-- 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 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ₚ
this : Module.Finite Rₚ Sₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)

Tactic:
let L := FractionRing S

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ₚ
this : Module.Finite Rₚ Sₚ
L : Type u_3 := FractionRing 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
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)

Tactic:
let Sₚ := Localization P'

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'
⊢ 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'
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)

Tactic:
let _ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S

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
⊢ 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 inr
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
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)

Tactic:
by_cases hP0 : P = ⊥

Result:
case pos
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 = ⊥
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)

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 = ⊥
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)