rw [← hJ, ← J.span_singleton_le_iff_mem] at h''
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}
h₁ : ∃ x, x ∈ ↑I ∩ ↑S
hJ : J = P
⊢ False
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
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
h'' : ¬Ideal.span {y} ≤ J
h₁ : ∃ x, x ∈ ↑I ∩ ↑S
hJ : J = P
⊢ False