cases i using Fin.cases <;> cases j using Fin.cases <;> simp[*]
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 j : Fin n.succ
⊢ (a :> f) i = (a :> f) j → i = j
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✝