case h
α : Type u_1
β : Type u_2
γ : Type ?u.120186
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
x : β
⊢ x ∈ ↑(image f univ) ↔ x ∈ Set.range f
α : Type u_1
β : Type u_2
γ : Type ?u.120186
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
⊢ ↑(image f univ) = Set.range f
ext x
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.120186
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
x : β
⊢ x ∈ ↑(image f univ) ↔ x ∈ Set.range f
simp