-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
inst_5 : CommRing Sₘ
inst_6 : Algebra S Sₘ
M : Submonoid R
inst_7 : IsLocalization M Rₘ
inst_8 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra Rₘ Sₘ
inst_10 : Algebra R Sₘ
inst_11 : IsScalarTower R Rₘ Sₘ
inst_12 : IsScalarTower R S Sₘ
inst_13 : Free R S
inst_14 : Module.Finite R S
a : S
h : Nontrivial R
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
this : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
inr :
  Eq.{u_3 + 1} (α := Rₘ)
    (Matrix.det.{u_3, u_2} (n := Free.ChooseBasisIndex R S)
        ((leftMulMatrix (Basis.localizationLocalization Rₘ M (A := S) Sₘ b) :
            (a : Sₘ) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) Rₘ)
          ((algebraMap S Sₘ : (a : S) → Sₘ) a)) :
      Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) ((norm R : (a : S) → R) a : R) : Rₘ)
inr₁ :
  Eq.{u_3 + 1} (α := Rₘ)
    (Matrix.det.{u_3, u_2} (n := Free.ChooseBasisIndex R S)
        ((leftMulMatrix (Basis.localizationLocalization Rₘ M (A := S) Sₘ b) :
            (a : Sₘ) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) Rₘ)
          ((algebraMap S Sₘ : (a : S) → Sₘ) a)) :
      Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ)
        (Matrix.det.{u_1, u_2} (n := Free.ChooseBasisIndex R S)
          ((leftMulMatrix b : (a : S) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) a)) :
      Rₘ)
inr₂ :
  Eq.{u_3 + 1} (α := Rₘ)
    (Matrix.det.{u_3, u_2} (n := Free.ChooseBasisIndex R S)
      ((leftMulMatrix (Basis.localizationLocalization Rₘ M (A := S) Sₘ b) :
          (a : Sₘ) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) Rₘ)
        ((algebraMap S Sₘ : (a : S) → Sₘ) a)))
    (Matrix.det.{u_3, u_2} (n := Free.ChooseBasisIndex R S)
      ((RingHom.mapMatrix (algebraMap R Rₘ) :
          (a : Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) →
            Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) Rₘ)
        ((leftMulMatrix b : (a : S) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) a)))
⊢ Eq.{u_3 + 1} (α := Rₘ) ((norm Rₘ : (a : Sₘ) → Rₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) a : Sₘ) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) ((norm R : (a : S) → R) a : R) : Rₘ)
have inr₃ : Eq.{u_3 + 1} (α := Rₘ)
  (Matrix.det.{u_3, u_2} (n := Free.ChooseBasisIndex R S)
    ((RingHom.mapMatrix (algebraMap R Rₘ) :
        (a : Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) →
          Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) Rₘ)
      ((leftMulMatrix b : (a : S) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) a)))
  (Matrix.det.{u_3, u_2} (n := Free.ChooseBasisIndex R S)
    ((RingHom.mapMatrix (algebraMap R Rₘ) :
        (a : Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) →
          Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) Rₘ)
      ((leftMulMatrix b : (a : S) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) a)))
Tactic: rw [Algebra.norm_eq_matrix_det (b.localizationLocalization Rₘ M Sₘ),
    Algebra.norm_eq_matrix_det b, RingHom.map_det, ← Algebra.map_leftMulMatrix_localization]