rw [spanIntNorm, spanIntNorm, spanIntNorm, Ideal.span_mul_span', ← Set.image_mul]
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)
I J : Ideal S
⊢ spanIntNorm R I * spanIntNorm R J ≤ spanIntNorm R (I * J)
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)
I J : Ideal S
⊢ span (⇑(Algebra.intNorm R S) '' (↑I * ↑J)) ≤ span (⇑(Algebra.intNorm R S) '' ↑(I * J))