case a
α : Type u_1
β : Type u_2
γ : Type ?u.95007
s t : Set α
inst✝² : DecidableEq α
inst✝¹ : Fintype β
f : β → α
inst✝ : Fintype ↑(range f)
a✝ : α
⊢ a✝ ∈ toFinset (range f) ↔ a✝ ∈ Finset.image f Finset.univ
α : Type u_1
β : Type u_2
γ : Type ?u.95007
s t : Set α
inst✝² : DecidableEq α
inst✝¹ : Fintype β
f : β → α
inst✝ : Fintype ↑(range f)
⊢ toFinset (range f) = Finset.image f Finset.univ
ext
no goals
case a
α : Type u_1
β : Type u_2
γ : Type ?u.95007
s t : Set α
inst✝² : DecidableEq α
inst✝¹ : Fintype β
f : β → α
inst✝ : Fintype ↑(range f)
a✝ : α
⊢ a✝ ∈ toFinset (range f) ↔ a✝ ∈ Finset.image f Finset.univ
simp