no goals
α : Type u_1
β : Type ?u.27403
β₂ : Type ?u.27406
γ : Type ?u.27409
ι : Sort u_2
ι' : Sort ?u.27415
κ : ι → Sort ?u.27420
κ' : ι' → Sort ?u.27425
inst✝ : CompleteSemilatticeSup α
s✝ t : Set α
a b : α
s : ι → α
⊢ a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b
simp [iSup, le_sSup_iff, upperBounds]