-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  Basis.indexEquiv (canonicalEmbedding.latticeBasis K) (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Equiv.trans (indexEquiv K) f.symm
M : Matrix (index K) (index K) ℝ :=
  Basis.toMatrix (mixedEmbedding.stdBasis K) (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ
    (Function.comp (β := Free.ChooseBasisIndex ℤ (𝓞 K))
      (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
      (⇑f.symm : (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)))
    RingHom.equivRatAlgHom
this :
  M.map (⇑ofRealHom : (a : ℝ) → ℂ) =
    HMul.hMul (α := Matrix (index K) (index K) ℂ) (matrixToStdBasis K)
      ((reindex (Equiv.symm (indexEquiv K)) (Equiv.symm (indexEquiv K)) :
            (a : Matrix (K →+* ℂ) (K →+* ℂ) ℂ) → Matrix (index K) (index K) ℂ)
          N)ᵀ
rw :
  (↑‖(↑(det (n := index K)
                (Basis.toMatrix (mixedEmbedding.stdBasis K)
                  (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))) :
            ℂ)‖₊ :
      ℝ≥0∞) =
    (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
rw₁ :
  (↑(nnnorm (E := ℂ)
          ((ofRealHom : (a : ℝ) → ℂ)
              (det (n := index K)
                (Basis.toMatrix (mixedEmbedding.stdBasis K)
                  (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))) :
            ℂ)) :
      ℝ≥0∞) =
    (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
rw₂ :
  (↑(nnnorm (E := ℂ)
          (det.{0, u_1} (n := index K)
            ((ofRealHom.mapMatrix : (a : Matrix (index K) (index K) ℝ) → Matrix (index K) (index K) ℂ)
              (Basis.toMatrix (mixedEmbedding.stdBasis K)
                (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))))) :
      ℝ≥0∞) =
    (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
rw₃ :
  (↑(nnnorm (E := ℂ)
          (det (n := index K)
            (Matrix.map
              (Basis.toMatrix (mixedEmbedding.stdBasis K)
                (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))
              (⇑ofRealHom : (a : ℝ) → ℂ)))) :
      ℝ≥0∞) =
    (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
rw₄ :
  (↑‖(HMul.hMul (α := Matrix (index K) (index K) ℂ) (matrixToStdBasis K)
              ((reindex (Equiv.symm (indexEquiv K)) (Equiv.symm (indexEquiv K)) :
                    (a : Matrix (K →+* ℂ) (K →+* ℂ) ℂ) → Matrix (index K) (index K) ℂ)
                  N)ᵀ).det‖₊ :
      ℝ≥0∞) =
    (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
⊢ (↑‖det (n := index K)
            (Basis.toMatrix (mixedEmbedding.stdBasis K)
              (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))‖₊ :
      ℝ≥0∞) =
    (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
have rw₅ : (↑‖det (n := index K) (matrixToStdBasis K) *
          det.{0, u_1} (n := index K)
            ((reindex (Equiv.symm (indexEquiv K)) (Equiv.symm (indexEquiv K)) :
                  (a : Matrix (K →+* ℂ) (K →+* ℂ) ℂ) → Matrix (index K) (index K) ℂ)
                N)ᵀ‖₊ :
    ℝ≥0∞) =
  (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
Tactic: rw [← nnnorm_real, ← ofRealHom_eq_coe, RingHom.map_det, RingHom.mapMatrix_apply, this,
          det_mul, det_transpose, det_reindex_self]