rw [Set.not_nonempty_iff_eq_empty.1 h]
case neg
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : ¬Set.Nonempty C
⊢ ∃ P ∈ Kaplansky.set S, ∀ J ∈ C, J ≤ P
case neg
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : ¬Set.Nonempty C
⊢ ∃ P ∈ Kaplansky.set S, ∀ J ∈ ∅, J ≤ P