-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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)
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
⊢ 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)) ℝ)

Tactic:
ext i j