no goals
α : Type u_2
β : Type u_1
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → f a₁ = f a₂ → a₁ = a₂
⊢ card s ≤ card t
classical calc
    s.card = (s.image f).card := (card_image_of_injOn f_inj).symm
    _ ≤ t.card := card_le_of_subset <| image_subset_iff.2 hf
no goals
α : Type u_2
β : Type u_1
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → f a₁ = f a₂ → a₁ = a₂
⊢ card s ≤ card t
calc
s.card = (s.image f).card := (card_image_of_injOn f_inj).symm
_ ≤ t.card := card_le_of_subset <| image_subset_iff.2 hf