intro hf
case succ.succ
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
this : ∀ (i : Fin n), f i ≠ a
i✝¹ i✝ : Fin n
⊢ f i✝¹ = f i✝ → i✝¹ = i✝
case succ.succ
n : ℕ
α : Type u
f : Fin n → α
h : Function.Injective f
a : α
ha : ∀ (i : Fin n), a ≠ f i
this : ∀ (i : Fin n), f i ≠ a
i✝¹ i✝ : Fin n
hf : f i✝¹ = f i✝
⊢ i✝¹ = i✝