rintro _ ⟨x, hxI, y, hyJ, rfl⟩
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
⊢ ↑I * ↑J ≤ ↑(I * J)
case intro.intro.intro.intro
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
x : S
hxI : x ∈ ↑I
y : S
hyJ : y ∈ ↑J
⊢ (fun x x_1 => x * x_1) x y ∈ ↑(I * J)