-- 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 (α := ℝ)
    (((Basis.det (latticeBasis K) : mixedSpace K [⋀^ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℝ] ℝ) :
          (a : ChooseBasisIndex ℤ (𝓞 K) → mixedSpace 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)))) :
      ℝ)
    ((algebraMap ℚ ℝ : (a : ℚ) → ℝ)
        (((Basis.det.{0, u_1, u_1} (R := ℚ) (M := K) (ι := ChooseBasisIndex ℤ (𝓞 K)) (integralBasis K) :
                K [⋀^ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℚ] ℚ) :
              (a : 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))) :
          ℚ) :
      ℝ)
have rw : Matrix.det (n := 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)) ℝ) =
  Matrix.det.{0, u_1} (n := 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)) ℚ))
Tactic: rw [Basis.det_apply, Basis.det_apply, RingHom.map_det]