have : i = n := Nat.le_antisymm
  (Nat.le_of_succ_le_succ (by rw [size_init] at h; exact h))
  h'
α✝ : 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' : n ≤ i
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }
α✝ : 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' : n ≤ i
this : i = n
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }