no goals
α : Type u_1
β : Type u_2
γ : Type ?u.15344
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → β
h : Injective f
b : β
w : ¬b ∈ Set.range f
⊢ ¬?m.15633 f h w ∈ map { toFun := f, inj' := h } univ
rwa [← mem_coe, coe_map, coe_univ, Set.image_univ]