case h
α : Type u_2
β : Type u_1
γ : Type ?u.67325
ι : Sort ?u.67328
ι' : Sort ?u.67331
f✝ : ι → α
s t : Set α
f : α → β
x✝ : β
⊢ x✝ ∈ f '' univ ↔ x✝ ∈ range f
α : Type u_2
β : Type u_1
γ : Type ?u.67325
ι : Sort ?u.67328
ι' : Sort ?u.67331
f✝ : ι → α
s t : Set α
f : α → β
⊢ f '' univ = range f
ext
no goals
case h
α : Type u_2
β : Type u_1
γ : Type ?u.67325
ι : Sort ?u.67328
ι' : Sort ?u.67331
f✝ : ι → α
s t : Set α
f : α → β
x✝ : β
⊢ x✝ ∈ f '' univ ↔ x✝ ∈ range f
simp [image, range]