-- 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
T : Type u_4
inst_9 : CommRing T
inst_10 : IsDomain T
inst_11 : IsIntegrallyClosed T
inst_12 : Algebra R T
inst_13 : Algebra T S
inst_14 : Module.Finite R T
inst_15 : Module.Finite T S
inst_16 : IsTorsionFree R T
inst_17 : IsTorsionFree T S
inst_18 : IsScalarTower R T S
inst_19 : IsDedekindDomain R
inst_20 : IsDedekindDomain T
inst_21 : IsDedekindDomain S
I : Ideal S
P : Ideal R
hP_1 : P.IsMaximal
hP : ¬P = ⊥
Rₚ : Type u_1 := Localization.AtPrime P
Tₚ : Type u_4 := Localization (M := T) (algebraMapSubmonoid T P.primeCompl)
Sₚ : Type u_3 := Localization (M := S) (algebraMapSubmonoid S P.primeCompl)
this : NeZero P
h : LE.le (α := Submonoid T) (algebraMapSubmonoid T P.primeCompl) T⁰
neg :
  Eq (α := Ideal (Localization.AtPrime P))
    (spanNorm (Localization.AtPrime P) (S := Tₚ) (map (F := T →+* Tₚ) (algebraMap T Tₚ) (spanNorm T I)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))
neg₁ :
  Eq (α := Ideal (Localization.AtPrime P))
    (spanNorm (Localization.AtPrime P) (spanNorm Tₚ (S := Sₚ) (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))
neg₂ :
  Eq (α := Ideal (Localization.AtPrime P))
    (spanNorm (Localization.AtPrime P) (spanNorm Tₚ (S := Sₚ) (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)))
    (spanNorm Rₚ (S := Sₚ) (map (F := S →+* Sₚ) (algebraMap S Sₚ) I))
neg₃ :
  Eq (α := Ideal (Localization.AtPrime P))
    (spanNorm (Localization.AtPrime P)
      (spanNorm Tₚ (S := Sₚ) (span {IsPrincipal.generator (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)})))
    (spanNorm Rₚ (S := Sₚ) (span {IsPrincipal.generator (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)}))
neg₄ :
  Eq (α := Ideal (Localization.AtPrime P))
    (spanNorm (Localization.AtPrime P) (S := Tₚ)
      (span
        (singleton (α := Tₚ)
          (((intNorm Tₚ Sₚ : Sₚ →* Tₚ) : (a : Sₚ) → Tₚ)
              (IsPrincipal.generator (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)) :
            Tₚ))))
    (spanNorm Rₚ (S := Sₚ) (span {IsPrincipal.generator (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)}))
neg₅ :
  Eq (α := Ideal (Localization.AtPrime P))
    (span
      (singleton (α := Localization.AtPrime P)
        ((intNorm (Localization.AtPrime P) Tₚ : (a : Tₚ) → Localization.AtPrime P)
            (((intNorm Tₚ Sₚ : Sₚ →* Tₚ) : (a : Sₚ) → Tₚ)
              (IsPrincipal.generator (map (F := S →+* Sₚ) (algebraMap S Sₚ) I))) :
          Localization.AtPrime P)))
    (spanNorm Rₚ (S := Sₚ) (span {IsPrincipal.generator (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)}))
⊢ Eq (α := Ideal (Localization.AtPrime P))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R (spanNorm T I)))
    (map (F := R →+* Localization.AtPrime P) (algebraMap R (Localization.AtPrime P)) (spanNorm R I))
have neg₆ : Eq (α := Ideal (Localization.AtPrime P))
  (span
    (singleton (α := Localization.AtPrime P)
      ((intNorm (Localization.AtPrime P) Sₚ : (a : Sₚ) → Localization.AtPrime P)
          (IsPrincipal.generator (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)) :
        Localization.AtPrime P)))
  (spanNorm Rₚ (S := Sₚ) (span {IsPrincipal.generator (map (F := S →+* Sₚ) (algebraMap S Sₚ) I)}))
Tactic: rw [← spanIntNorm_localization R (spanNorm T I) _ (primeCompl_le_nonZeroDivisors P) Tₚ,
    ← spanIntNorm_localization T (Rₘ := Tₚ) I _ h Sₚ, ← spanIntNorm_localization R (Rₘ := Rₚ) I _
    (primeCompl_le_nonZeroDivisors P) Sₚ, ← (I.map _).span_singleton_generator, spanNorm_singleton,
    spanNorm_singleton, intNorm_intNorm, spanNorm_singleton]