α : Type u_1
β : Type u_2
γ : Type ?u.2785
inst✝ : Finite α
f : α → β
hf : Function.Surjective f
this : Fintype α
⊢ Nat.card β ≤ Nat.card α
α : Type u_1
β : Type u_2
γ : Type ?u.2785
inst✝ : Finite α
f : α → β
hf : Function.Surjective f
⊢ Nat.card β ≤ Nat.card α
haveI := Fintype.ofFinite α
α : Type u_1
β : Type u_2
γ : Type ?u.2785
inst✝ : Finite α
f : α → β
hf : Function.Surjective f
this✝ : Fintype α
this : Fintype β
⊢ Nat.card β ≤ Nat.card α
α : Type u_1
β : Type u_2
γ : Type ?u.2785
inst✝ : Finite α
f : α → β
hf : Function.Surjective f
this : Fintype α
⊢ Nat.card β ≤ Nat.card α
haveI := Fintype.ofSurjective f hf
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.2785
inst✝ : Finite α
f : α → β
hf : Function.Surjective f
this✝ : Fintype α
this : Fintype β
⊢ Nat.card β ≤ Nat.card α
simpa only [Nat.card_eq_fintype_card, ge_iff_le] using Fintype.card_le_of_surjective f hf