-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst_9 : CommRing Rₘ
inst_10 : Algebra R Rₘ
inst_11 : CommRing Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : Algebra R Sₘ
inst_15 : IsScalarTower R Rₘ Sₘ
inst_16 : IsScalarTower R S Sₘ
inst_17 : IsLocalization M Rₘ
inst_18 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_19 : IsIntegrallyClosed Rₘ
inst_20 : IsDomain Rₘ
inst_21 : IsDomain Sₘ
inst_22 : IsTorsionFree Rₘ Sₘ
inst_23 : Module.Finite Rₘ Sₘ
inst_24 : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) ⋯
algInst : Algebra Rₘ K := f.toAlgebra
algInst_1 : Algebra Sₘ L := g.toAlgebra
algInst_2 : Algebra Rₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
scalarTowerInst : IsScalarTower Rₘ K L := ⋯
this_1 : IsScalarTower R Rₘ K
h_1 : IsFractionRing Rₘ K := ⋯
this : IsScalarTower S Sₘ L
h :
  Eq (α := R →+* L) (RingHom.comp (RingHom.comp (algebraMap K L) f) (algebraMap R Rₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₘ L) (algebraMap Rₘ Sₘ)) (algebraMap R Rₘ))
h₁ :
  Eq (α := R →+* L) (RingHom.comp (RingHom.comp (algebraMap K L) f) (algebraMap R Rₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (g.comp (algebraMap Rₘ Sₘ)) (algebraMap R Rₘ))
h₂ :
  Eq (α := R →+* L) (RingHom.comp (algebraMap K L) (f.comp (algebraMap R Rₘ)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (g.comp (algebraMap Rₘ Sₘ)) (algebraMap R Rₘ))
h₃ :
  Eq (α := R →+* L) (RingHom.comp (algebraMap K L) (f.comp (algebraMap R Rₘ)))
    (g.comp (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ Sₘ) (algebraMap R Rₘ)))
h₄ : Eq (α := R →+* L) (RingHom.comp (algebraMap K L) (f.comp (algebraMap R Rₘ))) (g.comp (algebraMap R Sₘ))
h₅ :
  Eq (α := R →+* L) (RingHom.comp (algebraMap K L) (f.comp (algebraMap R Rₘ)))
    (g.comp (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₘ) (algebraMap R S)))
h₆ :
  Eq (α := R →+* L) (RingHom.comp (algebraMap K L) (RingHom.comp (algebraMap R K) (RingHom.id R)))
    (g.comp (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₘ) (algebraMap R S)))
h₇ :
  Eq (α := R →+* L) (RingHom.comp (algebraMap K L) (algebraMap R K))
    (g.comp (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₘ) (algebraMap R S)))
h₈ :
  Eq (α := R →+* L) (RingHom.comp (algebraMap K L) (algebraMap R K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (g.comp (algebraMap S Sₘ)) (algebraMap R S))
⊢ Eq (α := R →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ L) (algebraMap R Rₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₘ L) (algebraMap Rₘ Sₘ)) (algebraMap R Rₘ))
have h₉ : Eq (α := R →+* L) (RingHom.comp (algebraMap K L) (algebraMap R K))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (RingHom.comp (algebraMap S L) (RingHom.id S)) (algebraMap R S))
Tactic: rw [RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra (R := Sₘ), RingHom.comp_assoc,
      RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R S Sₘ,
      IsLocalization.map_comp, RingHom.comp_id, ← RingHom.comp_assoc, IsLocalization.map_comp,
      RingHom.comp_id, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]