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

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

case inr
x y : ℝ
S : Set ℝ
a : ℝ
hS : ∀ (x : ℝ), x ∈ S → x ≤ a
ha : 0 ≤ a
hS₂ : Set.Nonempty S
⊢ sSup S ≤ a
exacts [sSup_empty.trans_le ha, csSup_le hS₂ hS]