no goals
α : Type u_1
β : Type ?u.72544
γ : Type ?u.72547
ι : Sort u_2
ι' : Sort ?u.72553
f✝ : ι → α
s t : Set α
f : ι → α
⊢ range f = ∅ ↔ IsEmpty ι
rw [← not_nonempty_iff, ← range_nonempty_iff_nonempty, not_nonempty_iff_eq_empty]