no goals
α : Type u_2
β : Type u_1
γ : Type ?u.74448
ι : Sort ?u.74451
ι' : Sort ?u.74454
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set β
hs : s ⊆ range f
⊢ f '' (f ⁻¹' s) = s
rw [image_preimage_eq_inter_range, inter_eq_self_of_subset_left hs]