no goals
α : Type u_1
β : Type ?u.26322
s t : Finset α
f✝ : α → β
n : ℕ
f : ℕ → α
hf : ∀ (i : ℕ), i < n → f i ∈ s
f_inj : ∀ (i : ℕ), i < n → ∀ (j : ℕ), j < n → f i = f j → i = j
⊢ ∀ (a : ℕ), a ∈ range n → f a ∈ s
simpa only [mem_range]
no goals
α : Type u_1
β : Type ?u.26322
s t : Finset α
f✝ : α → β
n : ℕ
f : ℕ → α
hf : ∀ (i : ℕ), i < n → f i ∈ s
f_inj : ∀ (i : ℕ), i < n → ∀ (j : ℕ), j < n → f i = f j → i = j
⊢ ∀ (a₁ : ℕ), a₁ ∈ range n → ∀ (a₂ : ℕ), a₂ ∈ range n → f a₁ = f a₂ → a₁ = a₂
simpa only [mem_range]