intro h
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : Set.Nonempty ↑S
P : Ideal R
hP : P ∈ Kaplansky.set S
⊢ P ≠ ⊤
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