no goals
α : Type u_1
β : Type ?u.75010
γ : Type ?u.75013
ι : Sort u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : ι → α
a : α
h : BddAbove (range s)
⊢ a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b
simp [iSup, h, le_csSup_iff', upperBounds]