refine' ⟨sSup C, _, fun z hz => le_sSup hz⟩
case pos.intro
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
I : Ideal R
hI : I ∈ C
⊢ ∃ P ∈ Kaplansky.set S, ∀ J ∈ C, J ≤ P
case pos.intro
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
I : Ideal R
hI : I ∈ C
⊢ sSup C ∈ Kaplansky.set S