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

case inr
x y : ℝ
S : Set ℝ
hS : ∀ (x : ℝ), x ∈ S → 0 ≤ x
hS₂ : Set.Nonempty S
⊢ 0 ≤ sInf S
x y : ℝ
S : Set ℝ
hS : ∀ (x : ℝ), x ∈ S → 0 ≤ x
⊢ 0 ≤ sInf S
rcases S.eq_empty_or_nonempty with (rfl | hS₂)
no goals
case inl
x y : ℝ
hS : ∀ (x : ℝ), x ∈ ∅ → 0 ≤ x
⊢ 0 ≤ sInf ∅

case inr
x y : ℝ
S : Set ℝ
hS : ∀ (x : ℝ), x ∈ S → 0 ≤ x
hS₂ : Set.Nonempty S
⊢ 0 ≤ sInf S
exacts [sInf_empty.ge, le_csInf hS₂ hS]