α : Type u_2
β : Type u_1
γ : Type ?u.29339
inst✝³ : Fintype α
s t : Finset α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y => y ∈ Set.range f
inst✝ : DecidableEq β
this : DecidablePred fun y => ∃ x, f x = y := inst✝¹
⊢ filter (fun y => y ∈ Set.range f) univ = image f univ
α : Type u_2
β : Type u_1
γ : Type ?u.29339
inst✝³ : Fintype α
s t : Finset α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y => y ∈ Set.range f
inst✝ : DecidableEq β
⊢ filter (fun y => y ∈ Set.range f) univ = image f univ
letI : DecidablePred (fun y => ∃ x, f x = y) := by simpa using ‹_›
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.29339
inst✝³ : Fintype α
s t : Finset α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y => y ∈ Set.range f
inst✝ : DecidableEq β
this : DecidablePred fun y => ∃ x, f x = y := inst✝¹
⊢ filter (fun y => y ∈ Set.range f) univ = image f univ
exact univ_filter_exists f
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.29339
inst✝³ : Fintype α
s t : Finset α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y => y ∈ Set.range f
inst✝ : DecidableEq β
⊢ DecidablePred fun y => ∃ x, f x = y
simpa using ‹_›