exact Nat.le_refl _
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i✝ : Nat
h✝ : i✝ < size (init (Nat.succ n) f)
h : i✝ < n
i : Fin n
⊢ n < Nat.succ n
no goals