-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsDomain A
inst_14 : IsIntegrallyClosed A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Module.Finite A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Module.Finite Aₘ Bₘ
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
this_1 : IsIntegralClosure B A L
this_2 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
this_3 : IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_4 : Algebra Aₘ K := f.toAlgebra
this_5 : IsScalarTower A Aₘ K
this_6 : IsFractionRing Aₘ K := ⋯
g : Bₘ →+* L :=
  IsLocalization.map (M := algebraMapSubmonoid B M) (T := algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L (RingHom.id B)
    ⋯
this_7 : Algebra Bₘ L := g.toAlgebra
this_8 : IsScalarTower B Bₘ L
this_9 : Algebra Aₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
this_10 : IsScalarTower Aₘ K L
this_11 : IsScalarTower Aₘ Bₘ L
this_12 : IsFractionRing Bₘ L := ⋯
this_13 : FiniteDimensional K L
this : IsIntegralClosure Bₘ Aₘ L
neg :
  Eq (α := K) ((algebraMap A K : (a : A) → K) ((intTrace A B : (a : B) → A) x) : K)
    (((algebraMap Aₘ K : Aₘ →+* K) : (a : Aₘ) → K)
        ((intTrace Aₘ Bₘ : (a : Bₘ) → Aₘ) ((algebraMap B Bₘ : (a : B) → Bₘ) x : Bₘ)) :
      K)
neg₁ :
  Eq.{u_1 + 1} (α := K)
    ((trace (FractionRing A) (FractionRing B) : (a : FractionRing B) → FractionRing A)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
      FractionRing A)
    (((algebraMap Aₘ K : Aₘ →+* K) : (a : Aₘ) → K)
        ((intTrace Aₘ Bₘ : (a : Bₘ) → Aₘ) ((algebraMap B Bₘ : (a : B) → Bₘ) x : Bₘ)) :
      K)
neg₂ :
  Eq.{u_1 + 1} (α := K)
    ((trace (FractionRing A) (FractionRing B) : (a : FractionRing B) → FractionRing A)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
      FractionRing A)
    (((trace K L : L →ₗ[K] K) : (a : L) → K)
        (((algebraMap Bₘ L : Bₘ →+* L) : (a : Bₘ) → L) ((algebraMap B Bₘ : (a : B) → Bₘ) x)) :
      K)
⊢ Eq.{u_1 + 1} (α := K)
    (((algebraMap Aₘ K : Aₘ →+* K) : (a : Aₘ) → K)
        ((algebraMap A Aₘ : (a : A) → Aₘ) ((intTrace A B : (a : B) → A) x : A)) :
      K)
    (((algebraMap Aₘ K : Aₘ →+* K) : (a : Aₘ) → K)
        ((intTrace Aₘ Bₘ : (a : Bₘ) → Aₘ) ((algebraMap B Bₘ : (a : B) → Bₘ) x : Bₘ)) :
      K)
have neg₃ : Eq.{u_1 + 1} (α := K)
  ((trace (FractionRing A) (FractionRing B) : (a : FractionRing B) → FractionRing A)
      ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
    FractionRing A)
  (((trace K L : L →ₗ[K] K) : (a : L) → K) ((algebraMap B L : (a : B) → L) x) : K)
Tactic: rw [← IsScalarTower.algebraMap_apply, Algebra.algebraMap_intTrace_fractionRing,
    Algebra.algebraMap_intTrace (L := L), ← IsScalarTower.algebraMap_apply]