-- Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
theorem spanNorm_mul (I J : Ideal S) : spanNorm R (I * J) = spanNorm R I * spanNorm R J

Proof state:
case he.h.a
R : Type u_1
inst✝¹² : CommRing R
inst✝¹¹ : IsDomain R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
inst✝⁸ : IsIntegrallyClosed R
inst✝⁷ : IsIntegrallyClosed S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Finite R S
inst✝⁴ : NoZeroSMulDivisors R S
inst✝³ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_3 := Localization P'
x✝¹ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝⁵ : IsDomain Sₚ
this✝⁴ : IsDedekindDomain Sₚ
this✝³ : IsPrincipalIdealRing Sₚ
this✝² : NoZeroSMulDivisors Rₚ Sₚ
this✝¹ : Module.Finite Rₚ Sₚ
L : Type u_3 := FractionRing S
g : Sₚ →+* L := IsLocalization.map L (RingHom.id S) h
algInst✝ : Algebra Sₚ L := g.toAlgebra
this✝ : IsScalarTower S Sₚ (FractionRing S)
this : IsFractionRing Sₚ (FractionRing S)
x✝ : R
⊢ (((algebraMap (FractionRing Rₚ) (FractionRing Sₚ)).comp
            ↑(FractionRing.algEquiv Rₚ (FractionRing R)).symm.toRingEquiv).comp
        (algebraMap R (FractionRing R)))
      x✝ =
    (((↑(FractionRing.algEquiv Sₚ (FractionRing S)).symm.toRingEquiv).comp
            (algebraMap (FractionRing R) (FractionRing S))).comp
        (algebraMap R (FractionRing R)))
      x✝

Tactic:
simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp,
  RingHom.coe_coe, Function.comp_apply, ← IsScalarTower.algebraMap_apply]

Result:
case he.h.a
R : Type u_1
inst✝¹² : CommRing R
inst✝¹¹ : IsDomain R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
inst✝⁸ : IsIntegrallyClosed R
inst✝⁷ : IsIntegrallyClosed S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Finite R S
inst✝⁴ : NoZeroSMulDivisors R S
inst✝³ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_3 := Localization P'
x✝¹ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝⁵ : IsDomain Sₚ
this✝⁴ : IsDedekindDomain Sₚ
this✝³ : IsPrincipalIdealRing Sₚ
this✝² : NoZeroSMulDivisors Rₚ Sₚ
this✝¹ : Module.Finite Rₚ Sₚ
L : Type u_3 := FractionRing S
g : Sₚ →+* L := IsLocalization.map L (RingHom.id S) h
algInst✝ : Algebra Sₚ L := g.toAlgebra
this✝ : IsScalarTower S Sₚ (FractionRing S)
this : IsFractionRing Sₚ (FractionRing S)
x✝ : R
⊢ (algebraMap (FractionRing Rₚ) (FractionRing Sₚ))
      (↑(FractionRing.algEquiv Rₚ (FractionRing R)).symm ((algebraMap R (FractionRing R)) x✝)) =
    ↑(FractionRing.algEquiv Sₚ (FractionRing S)).symm ((algebraMap R (FractionRing S)) x✝)

Proof state:
case neg
R : Type u_1
inst✝¹² : CommRing R
inst✝¹¹ : IsDomain R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
inst✝⁸ : IsIntegrallyClosed R
inst✝⁷ : IsIntegrallyClosed S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Finite R S
inst✝⁴ : NoZeroSMulDivisors R S
inst✝³ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_3 := Localization P'
x✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝² : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝¹ : IsDomain Sₚ
this✝ : IsDedekindDomain Sₚ
this : IsPrincipalIdealRing Sₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)

Tactic:
have := NoZeroSMulDivisors_of_isLocalization R S Rₚ Sₚ P.primeCompl_le_nonZeroDivisors

Result:
case neg
R : Type u_1
inst✝¹² : CommRing R
inst✝¹¹ : IsDomain R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
inst✝⁸ : IsIntegrallyClosed R
inst✝⁷ : IsIntegrallyClosed S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Finite R S
inst✝⁴ : NoZeroSMulDivisors R S
inst✝³ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_3 := Localization P'
x✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝³ : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : IsDedekindDomain Sₚ
this✝ : IsPrincipalIdealRing Sₚ
this : NoZeroSMulDivisors Rₚ Sₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)

Proof state:
case neg
R : Type u_1
inst✝¹² : CommRing R
inst✝¹¹ : IsDomain R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
inst✝⁸ : IsIntegrallyClosed R
inst✝⁷ : IsIntegrallyClosed S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Finite R S
inst✝⁴ : NoZeroSMulDivisors R S
inst✝³ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_3 := Localization P'
x✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝ : IsDomain Sₚ
this : IsDedekindDomain Sₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)

Tactic:
have : IsPrincipalIdealRing Sₚ :=
  IsDedekindDomain.isPrincipalIdealRing_localization_over_prime S P hP0

Result:
case neg
R : Type u_1
inst✝¹² : CommRing R
inst✝¹¹ : IsDomain R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
inst✝⁸ : IsIntegrallyClosed R
inst✝⁷ : IsIntegrallyClosed S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Finite R S
inst✝⁴ : NoZeroSMulDivisors R S
inst✝³ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_3 := Localization P'
x✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝² : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝¹ : IsDomain Sₚ
this✝ : IsDedekindDomain Sₚ
this : IsPrincipalIdealRing Sₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)