-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)
⊢ Eq (α := Matrix (ChooseBasisIndex ℤ (𝓞 K)) (ChooseBasisIndex ℤ (𝓞 K)) ℝ)
    (Basis.toMatrix (latticeBasis K)
        (Function.comp (β := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
          (Function.comp (β := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (⇑(basisOfFractionalIdeal K I :
                  Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
              (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
            (⇑e :
              (a : ChooseBasisIndex ℤ (𝓞 K)) →
                ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))) :
      Matrix (ChooseBasisIndex ℤ (𝓞 K)) (ChooseBasisIndex ℤ (𝓞 K)) ℝ)
    ((RingHom.mapMatrix (algebraMap ℚ ℝ) :
          (a : Matrix (ChooseBasisIndex ℤ (𝓞 K)) (ChooseBasisIndex ℤ (𝓞 K)) ℚ) →
            Matrix (ChooseBasisIndex ℤ (𝓞 K)) (ChooseBasisIndex ℤ (𝓞 K)) ℝ)
        (Basis.toMatrix (integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K)
            (Function.comp (β := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
              (⇑(basisOfFractionalIdeal K I :
                    Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
                (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
              (⇑e :
                (a : ChooseBasisIndex ℤ (𝓞 K)) →
                  ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))) :
          Matrix (ChooseBasisIndex ℤ (𝓞 K)) (ChooseBasisIndex ℤ (𝓞 K)) ℚ) :
      Matrix (ChooseBasisIndex ℤ (𝓞 K)) (ChooseBasisIndex ℤ (𝓞 K)) ℝ)
have e_M : ∀ (i j : ChooseBasisIndex ℤ (𝓞 K)),
  Basis.toMatrix (latticeBasis K)
      (Function.comp (β := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
        (Function.comp (β := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(basisOfFractionalIdeal K I :
                Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
            (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
          (⇑e :
            (a : ChooseBasisIndex ℤ (𝓞 K)) →
              ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))))
      i j =
    (RingHom.mapMatrix (algebraMap ℚ ℝ) :
        (a : Matrix (ChooseBasisIndex ℤ (𝓞 K)) (ChooseBasisIndex ℤ (𝓞 K)) ℚ) →
          Matrix (ChooseBasisIndex ℤ (𝓞 K)) (ChooseBasisIndex ℤ (𝓞 K)) ℝ)
      (Basis.toMatrix (integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K)
          (Function.comp (β := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (⇑(basisOfFractionalIdeal K I :
                  Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
              (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
            (⇑e :
              (a : ChooseBasisIndex ℤ (𝓞 K)) →
                ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))) :
        Matrix (ChooseBasisIndex ℤ (𝓞 K)) (ChooseBasisIndex ℤ (𝓞 K)) ℚ)
      i j
Tactic: ext i j