α : Type u_2
β : Type u_1
γ : Type ?u.74585
ι : Sort ?u.74588
ι' : Sort ?u.74591
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set β
h : f '' (f ⁻¹' s) = s
⊢ s ⊆ range f
α : Type u_2
β : Type u_1
γ : Type ?u.74585
ι : Sort ?u.74588
ι' : Sort ?u.74591
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set β
⊢ f '' (f ⁻¹' s) = s → s ⊆ range f
intro h
α : Type u_2
β : Type u_1
γ : Type ?u.74585
ι : Sort ?u.74588
ι' : Sort ?u.74591
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set β
h : f '' (f ⁻¹' s) = s
⊢ f '' (f ⁻¹' s) ⊆ range f
α : Type u_2
β : Type u_1
γ : Type ?u.74585
ι : Sort ?u.74588
ι' : Sort ?u.74591
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set β
h : f '' (f ⁻¹' s) = s
⊢ s ⊆ range f
rw [← h]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.74585
ι : Sort ?u.74588
ι' : Sort ?u.74591
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set β
h : f '' (f ⁻¹' s) = s
⊢ f '' (f ⁻¹' s) ⊆ range f
apply image_subset_range