if hj : j < len then
  simp only [dif_pos hj]
  have IH := get_ofFn_go f i (j+1) hi
  apply And.intro
  . show i ≥ j → _
    intro hij
    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
  . show i < j → _
    intro hij
    apply Eq.trans ((IH _).2 (Nat.lt_succ_of_lt hij))
    exact ArrayLike.get_set_ne x (Nat.ne_of_gt hij) (f ⟨j,hj⟩) hi
else
  simp only [dif_neg hj]
  refine And.intro ?_ (fun _ => True.intro)
  intro hij
  have : len ≤ i := trans (r:=LE.le) (s:=LE.le) (Nat.ge_of_not_lt hj) hij
  exact False.elim <| Nat.le_lt_antisymm this hi
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
⊢ (i ≥ j →
      (if h : j < len then ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := h }) h) else x)[i] =
        f { val := i, isLt := hi }) ∧
    (i < j →
      (if h : j < len then ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := h }) h) else x)[i] = x[i])
no goals