have h : P' ≤ S⁰ :=
  map_le_nonZeroDivisors_of_injective _ (NoZeroSMulDivisors.algebraMap_injective _ _)
    P.primeCompl_le_nonZeroDivisors
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ₚ
⊢ 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))
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⁰
⊢ 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))