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