case inl
x y : ℝ
h₁ : BddBelow ∅
h₂ : BddAbove ∅
⊢ sInf ∅ ≤ sSup ∅

case inr
x y : ℝ
s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
hne : Set.Nonempty s
⊢ sInf s ≤ sSup s
x y : ℝ
s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
⊢ sInf s ≤ sSup s
rcases s.eq_empty_or_nonempty with (rfl | hne)
no goals
case inl
x y : ℝ
h₁ : BddBelow ∅
h₂ : BddAbove ∅
⊢ sInf ∅ ≤ sSup ∅
rw [sInf_empty, sSup_empty]
no goals
case inr
x y : ℝ
s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
hne : Set.Nonempty s
⊢ sInf s ≤ sSup s
exact csInf_le_csSup h₁ h₂ hne