no goals
ι : Sort ?u.234525
α : Type u_1
β : Type u_2
f✝ : α → β
f : Set α → Set β
hf : Injective f
h2 : f ∅ = ∅
s : Set α
⊢ Set.Nonempty (f s) ↔ Set.Nonempty s
rw [nonempty_iff_ne_empty, ← h2, nonempty_iff_ne_empty, hf.ne_iff]