no goals
α✝ : Type ?u.16264
β✝ : Type ?u.16267
γ : Type ?u.16270
inst✝³ : Fintype α✝
inst✝² : Fintype β✝
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Fintype α
inst✝ : Fintype ↑(Set.range f)
a : α
⊢ f a ∈ Set.range f
simp
no goals
α✝ : Type ?u.16264
β✝ : Type ?u.16267
γ : Type ?u.16270
inst✝³ : Fintype α✝
inst✝² : Fintype β✝
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Fintype α
inst✝ : Fintype ↑(Set.range f)
x✝ : ↑(Set.range f)
val✝ : β
a : α
ha : f a = val✝
⊢ (fun a => { val := f a, property := (_ : f a ∈ Set.range f) }) a = { val := val✝, property := (_ : ∃ y, f y = val✝) }
simpa using ha