case inl
x y : ℝ
hS : ∀ (x : ℝ), x ∈ ∅ → 0 ≤ x
⊢ 0 ≤ sSup ∅

case inr.intro
x y✝ : ℝ
S : Set ℝ
hS : ∀ (x : ℝ), x ∈ S → 0 ≤ x
y : ℝ
hy : y ∈ S
⊢ 0 ≤ sSup S
x y : ℝ
S : Set ℝ
hS : ∀ (x : ℝ), x ∈ S → 0 ≤ x
⊢ 0 ≤ sSup S
rcases S.eq_empty_or_nonempty with (rfl | ⟨y, hy⟩)
no goals
case inl
x y : ℝ
hS : ∀ (x : ℝ), x ∈ ∅ → 0 ≤ x
⊢ 0 ≤ sSup ∅
exact sSup_empty.ge
no goals
case inr.intro
x y✝ : ℝ
S : Set ℝ
hS : ∀ (x : ℝ), x ∈ S → 0 ≤ x
y : ℝ
hy : y ∈ S
⊢ 0 ≤ sSup S
apply dite _ (fun h => le_csSup_of_le h hy <| hS y hy) fun h => (sSup_of_not_bddAbove h).ge