no goals
α✝ : Type ?u.81981
β✝ : Type ?u.81984
γ : Type ?u.81987
α : Sort u_1
β : Sort u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
⊢ ∃ x y, x ≠ y ∧ f x = f y
simpa only [Injective, not_forall, not_imp, and_comm] using not_injective_infinite_finite f