rw [Kaplansky.set, h, Set.mem_setOf, Set.eq_empty_iff_forall_not_mem] at hP
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : Set.Nonempty ↑S
P : Ideal R
hP : P ∈ Kaplansky.set S
h : P = ⊤
⊢ False
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : Set.Nonempty ↑S
P : Ideal R
hP : ∀ (x : R), x ∉ ↑⊤ ∩ ↑S
h : P = ⊤
⊢ False