Theorem: Ideal.spanIntNorm_map
Proof state before:
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 : Ideal R
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
P : Ideal R
hPd : P.IsMaximal
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 Rₚ
this✝¹¹ : IsIntegrallyClosed Rₚ
this✝¹⁰ : NoZeroSMulDivisors Rₚ Sₚ
this✝⁹ : Module.Finite Rₚ Sₚ
K : Type u_1 := FractionRing R
f : Rₚ →+* K := IsLocalization.map K (RingHom.id R) ⋯
this✝⁸ : Algebra Rₚ K := f.toAlgebra
this✝⁷ : IsScalarTower R Rₚ K
this✝⁶ : IsFractionRing Rₚ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization P.primeCompl Rₚ K
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✝² : Algebra Rₚ L := ((algebraMap K L).comp f).toAlgebra
this✝¹ : IsScalarTower Rₚ K L
this✝ : IsScalarTower Rₚ Sₚ L
this : IsIntegralClosure Sₚ Rₚ L
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (map (algebraMap R S) I)) =
    map (algebraMap R (Localization.AtPrime P)) (I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S))
Tactic:
haveI : IsSeparable (FractionRing Rₚ) (FractionRing Sₚ) := by
  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:
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 : Ideal R
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
P : Ideal R
hPd : P.IsMaximal
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 Rₚ
this✝¹² : IsIntegrallyClosed Rₚ
this✝¹¹ : NoZeroSMulDivisors Rₚ Sₚ
this✝¹⁰ : Module.Finite Rₚ Sₚ
K : Type u_1 := FractionRing R
f : Rₚ →+* K := IsLocalization.map K (RingHom.id R) ⋯
this✝⁹ : Algebra Rₚ K := f.toAlgebra
this✝⁸ : IsScalarTower R Rₚ K
this✝⁷ : IsFractionRing Rₚ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization P.primeCompl Rₚ K
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✝³ : Algebra Rₚ L := ((algebraMap K L).comp f).toAlgebra
this✝² : IsScalarTower Rₚ K L
this✝¹ : IsScalarTower Rₚ Sₚ L
this✝ : IsIntegralClosure Sₚ Rₚ L
this : IsSeparable (FractionRing Rₚ) (FractionRing Sₚ)
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (map (algebraMap R S) I)) =
    map (algebraMap R (Localization.AtPrime P)) (I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S))