simp [init_succ]
α✝ : Type u_1
n✝ : Nat
ih : ∀ {f : Fin n✝ → α✝}, size (init n✝ f) = n✝
f : Fin (Nat.succ n✝) → α✝
⊢ size (init (Nat.succ n✝) f) = Nat.succ n✝
α✝ : Type u_1
n✝ : Nat
ih : ∀ {f : Fin n✝ → α✝}, size (init n✝ f) = n✝
f : Fin (Nat.succ n✝) → α✝
⊢ size (init n✝ fun i => f { val := ↑i, isLt := ⋯ }) = n✝