-- 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)
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
have 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 :
        ℚ) :
    ℝ)
Tactic: simp_rw [RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply, Function.comp_apply]