no goals
α✝ : Type ?u.2629
β : Type ?u.2632
γ : Type ?u.2635
ι : Sort u_2
α : Type u_1
inst✝¹ : IsEmpty ι
inst✝ : InfSet α
f : ι → WithTop α
⊢ (⨅ (i : ι), f i) = ⊤
rw [iInf, range_eq_empty, WithTop.sInf_empty]