no goals
α : Type u_1
β : Type ?u.188056
β₂ : Type ?u.188059
γ : Type ?u.188062
ι : Sort u_2
ι' : Sort ?u.188068
κ : ι → Sort ?u.188073
κ' : ι' → Sort ?u.188078
inst✝ : CompleteLinearOrder α
f : ι → α
⊢ iInf f = ⊥ ↔ ∀ (b : α), b > ⊥ → ∃ i, f i < b
simp only [← sInf_range, sInf_eq_bot, Set.exists_range_iff]