induction n generalizing i with
| zero => simp at h; exact False.elim <| Nat.not_lt_zero _ h
| succ n ih =>
  simp [init_succ, get_push]
  split
  next h =>
    have := @ih (fun i => f ⟨i,Nat.lt_trans i.isLt (by exact Nat.le_refl _)⟩) i (by simp; assumption)
    simp at this ⊢
    rw [this]
  next h' =>
    simp at h'
    have : i = n := Nat.le_antisymm
      (Nat.le_of_succ_le_succ (by rw [size_init] at h; exact h))
      h'
    cases this
    congr
n : Nat
α✝ : Type u_1
f : Fin n → α✝
i : Nat
h : i < size (init n f)
⊢ (init n f)[i] = f { val := i, isLt := ⋯ }
no goals