rw [Ideal.mul_sup, Ideal.sup_mul, Ideal.sup_mul, Ideal.span_singleton_mul_span_singleton]
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
s : R
hs : s ∈ ↑I
hs' : s ∈ ↑S
t : R
ht : t ∈ ↑J
ht' : t ∈ ↑S
⊢ I * J ≤ P
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
s : R
hs : s ∈ ↑I
hs' : s ∈ ↑S
t : R
ht : t ∈ ↑J
ht' : t ∈ ↑S
⊢ P * P ⊔ Ideal.span {x} * P ⊔ (P * Ideal.span {y} ⊔ Ideal.span {x * y}) ≤ P