simp only [ofFn_succ f, get_push']
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
⊢ (ofFn f)[i] = f { val := i, isLt := (_ : i < Nat.succ n) }
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
⊢ (if h : i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) then
      (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })[i]
    else f { val := n, isLt := (_ : n < Nat.succ n) }) =
    f { val := i, isLt := (_ : i < Nat.succ n) }