no goals
α : Type u_1
β : Type u_2
γ : Type ?u.50772
inst✝¹ : Fintype α
inst✝ : Fintype β
h : Fintype.card α ≤ Fintype.card β
⊢ Nonempty (α ↪ β)
classical exact (truncOfCardLe h).nonempty
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.50772
inst✝¹ : Fintype α
inst✝ : Fintype β
h : Fintype.card α ≤ Fintype.card β
⊢ Nonempty (α ↪ β)
exact (truncOfCardLe h).nonempty