Theorem: Ideal.spanIntNorm_mul
Proof state before:
case he.h
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✝ : IsScalarTower R Rₚ (FractionRing R)
this : IsFractionRing Rₚ (FractionRing R) :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization P.primeCompl Rₚ (FractionRing R)
⊢ ((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))
Tactic:
ext
Proof state after:
case he.h.a
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✝ : IsScalarTower R Rₚ (FractionRing R)
this : IsFractionRing Rₚ (FractionRing R) :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization P.primeCompl Rₚ (FractionRing R)
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✝