Formalizing a proof in lean using GitHub Copilot and canonical