Theorem: Ideal.spanIntNorm_mul
Proof state before:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R 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_2 := Localization P'
this✝⁹ : 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✝⁴ : IsIntegrallyClosed Rₚ
this✝³ : NoZeroSMulDivisors Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
L : Type u_2 := FractionRing S
g : Sₚ →+* L := IsLocalization.map L (RingHom.id S) h
this✝¹ : Algebra Sₚ L := g.toAlgebra
this✝ : IsScalarTower S Sₚ (FractionRing S)
this : IsFractionRing Sₚ (FractionRing S) :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization P' Sₚ (FractionRing S)
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
haveI : IsSeparable (FractionRing Rₚ) (FractionRing Sₚ) := by
  haveI : IsScalarTower R Rₚ (FractionRing R) := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.lift_comp])
  letI := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization
    P.primeCompl Rₚ (FractionRing R)
  apply IsSeparable.of_equiv_equiv (FractionRing.algEquiv Rₚ (FractionRing R)).symm.toRingEquiv
    (FractionRing.algEquiv Sₚ (FractionRing S)).symm.toRingEquiv
  apply IsLocalization.ringHom_ext R⁰
  ext
  simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp,
    RingHom.coe_coe, Function.comp_apply, ← IsScalarTower.algebraMap_apply]
  simp only [IsScalarTower.algebraMap_apply R Rₚ (FractionRing R), AlgEquiv.coe_ringEquiv,
    AlgEquiv.commutes, IsScalarTower.algebraMap_apply R S L,
    IsScalarTower.algebraMap_apply S Sₚ L]
  simp only [← IsScalarTower.algebraMap_apply]
  rw [IsScalarTower.algebraMap_apply R Rₚ (FractionRing Rₚ), ← IsScalarTower.algebraMap_apply Rₚ,
    ← IsScalarTower.algebraMap_apply]
Proof state after:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R 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_2 := Localization P'
this✝¹⁰ : 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✝⁵ : IsIntegrallyClosed Rₚ
this✝⁴ : NoZeroSMulDivisors Rₚ Sₚ
this✝³ : Module.Finite Rₚ Sₚ
L : Type u_2 := FractionRing S
g : Sₚ →+* L := IsLocalization.map L (RingHom.id S) h
this✝² : Algebra Sₚ L := g.toAlgebra
this✝¹ : IsScalarTower S Sₚ (FractionRing S)
this✝ : IsFractionRing Sₚ (FractionRing S) :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization P' Sₚ (FractionRing S)
this : IsSeparable (FractionRing Rₚ) (FractionRing Sₚ)
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)