rw [Set.nonempty_def] at hS
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
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : ∃ x, x ∈ ↑S
P : Ideal R
hP : ∀ (x : R), x ∉ ↑⊤ ∩ ↑S
h : P = ⊤
⊢ False