no goals
α : Type u_1
β : Type ?u.187342
β₂ : Type ?u.187345
γ : Type ?u.187348
ι : Sort u_2
ι' : Sort ?u.187354
κ : ι → Sort ?u.187359
κ' : ι' → Sort ?u.187364
inst✝ : CompleteLinearOrder α
f : ι → α
⊢ iSup f = ⊤ ↔ ∀ (b : α), b < ⊤ → ∃ i, b < f i
simp only [← sSup_range, sSup_eq_top, Set.exists_range_iff]