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

Tactic:
rw [← (I.map _).span_singleton_generator, ← (J.map _).span_singleton_generator,
  span_singleton_mul_span_singleton, spanNorm_singleton, spanNorm_singleton,
  spanNorm_singleton, span_singleton_mul_span_singleton, _root_.map_mul]

Result:
no goals

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
⊢ spanNorm R (I * J) = spanNorm R I * spanNorm R J

Tactic:
cases subsingleton_or_nontrivial S

Result:
case inl
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✝ : Subsingleton S
⊢ spanNorm R (I * J) = spanNorm R I * spanNorm R J

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

Tactic:
rw [IsScalarTower.algebraMap_apply R Rₚ (FractionRing R), AlgEquiv.coe_ringEquiv,
  AlgEquiv.commutes, IsScalarTower.algebraMap_apply R S L,
  IsScalarTower.algebraMap_apply S Sₚ L, AlgEquiv.coe_ringEquiv, AlgEquiv.commutes]

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ₚ)) ((algebraMap Rₚ (FractionRing Rₚ)) ((algebraMap R Rₚ) x✝)) =
    (algebraMap Sₚ (FractionRing Sₚ)) ((algebraMap S Sₚ) ((algebraMap R S) x✝))