-- 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)
i j : ChooseBasisIndex ℤ (𝓞 K)
e_M :
  Eq (α := ℝ)
    (((((Basis.repr (latticeBasis K) : mixedSpace K ≃ₗ[ℝ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℝ) :
                (a : mixedSpace K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℝ)
              ((mixedEmbedding K : (a : K) → mixedSpace 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))
                        j :
                      ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))) :
                mixedSpace K) :
            ChooseBasisIndex ℤ (𝓞 K) →₀ ℝ) :
          (a : ChooseBasisIndex ℤ (𝓞 K)) → ℝ)
        i :
      ℝ)
    ((algebraMap ℚ ℝ : (a : ℚ) → ℝ)
        (((((Basis.repr (integralBasis K) : K ≃ₗ[ℚ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
                    (a : K) → ChooseBasisIndex ℤ (𝓞 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))
                          j :
                        ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) :
                    K) :
                ChooseBasisIndex ℤ (𝓞 K) →₀ ℚ) :
              (a : ChooseBasisIndex ℤ (𝓞 K)) → ℚ)
            i :
          ℚ) :
      ℝ)
⊢ 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:
simp_rw [RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply, Function.comp_apply]

Premises used: RingHom.mapMatrix_apply, Matrix.map_apply, Module.Basis.toMatrix_apply, Function.comp_apply