-- 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
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)
⊢ (algebraMap (FractionRing Rₚ) (FractionRing Sₚ)).comp ↑(FractionRing.algEquiv Rₚ (FractionRing R)).symm.toRingEquiv =
    (↑(FractionRing.algEquiv Sₚ (FractionRing S)).symm.toRingEquiv).comp (algebraMap (FractionRing R) (FractionRing S))

Tactic:
apply IsLocalization.ringHom_ext R⁰

Result:
case he.h
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)
⊢ ((algebraMap (FractionRing Rₚ) (FractionRing Sₚ)).comp
          ↑(FractionRing.algEquiv Rₚ (FractionRing R)).symm.toRingEquiv).comp
      (algebraMap R (FractionRing R)) =
    ((↑(FractionRing.algEquiv Sₚ (FractionRing S)).symm.toRingEquiv).comp
          (algebraMap (FractionRing R) (FractionRing S))).comp
      (algebraMap R (FractionRing R))

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

Tactic:
let P' := Algebra.algebraMapSubmonoid S P.primeCompl

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

Proof state:
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
⊢ algebraMap S (FractionRing S) = (algebraMap Sₚ (FractionRing S)).comp (algebraMap S Sₚ)

Tactic:
rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHom.comp_id]

Result:
no goals

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ₚ
L : Type u_3 := FractionRing S
g : Sₚ →+* L := IsLocalization.map L (RingHom.id S) h
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)

Tactic:
algebraize [g]

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
g : Sₚ →+* L := IsLocalization.map L (RingHom.id S) h
algInst✝ : Algebra Sₚ L := g.toAlgebra
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)