have h₁ : ∃ x : R, x ∈ (I : Set R) ∩ S := by
  refine' exists_mem_inter hmax (lt_of_le_of_ne' le_sup_left _)
  intro hI
  rw [← hI, ← I.span_singleton_le_iff_mem] at h'
  exact h' le_sup_right
case intro
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}
⊢ False
case intro
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
⊢ False