cases Nat.eq_or_lt_of_le hij with
| inl heq =>
  cases heq
  apply Eq.trans ((IH _).2 i.lt_succ_self)
  exact ArrayLike.get_set_eq x i (f ⟨i,hi⟩)
| inr hgt => exact Eq.trans ((IH _).1 hgt) rfl
case left
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
IH :
  ∀ (x : cont),
    (i ≥ j + 1 → (ofFn.go cont f (j + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < j + 1 → (ofFn.go cont f (j + 1) x)[i] = x[i])
hij : i ≥ j
⊢ (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = f { val := i, isLt := hi }
no goals