by_cases hP0 : P = ⊥
case inr
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
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
case pos
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 = ⊥
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)

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 = ⊥
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)