α : Type u_1
β : Type ?u.90617
s t : Set α
a b x y : α
f✝ : α → β
n : ℕ
f : ℕ → α
hf : ∀ (i : ℕ), i < n → f i ∈ s
f_inj : ∀ (i : ℕ), i < n → ∀ (j : ℕ), j < n → f i = f j → i = j
hs : autoParam (Set.Finite s) _auto✝
⊢ n ≤ Finset.card (Finite.toFinset hs)
α : Type u_1
β : Type ?u.90617
s t : Set α
a b x y : α
f✝ : α → β
n : ℕ
f : ℕ → α
hf : ∀ (i : ℕ), i < n → f i ∈ s
f_inj : ∀ (i : ℕ), i < n → ∀ (j : ℕ), j < n → f i = f j → i = j
hs : autoParam (Set.Finite s) _auto✝
⊢ n ≤ ncard s
rw [ncard_eq_toFinset_card _ hs]
no goals
α : Type u_1
β : Type ?u.90617
s t : Set α
a b x y : α
f✝ : α → β
n : ℕ
f : ℕ → α
hf : ∀ (i : ℕ), i < n → f i ∈ s
f_inj : ∀ (i : ℕ), i < n → ∀ (j : ℕ), j < n → f i = f j → i = j
hs : autoParam (Set.Finite s) _auto✝
⊢ n ≤ Finset.card (Finite.toFinset hs)
apply Finset.le_card_of_inj_on_range <;> simpa