unfold ofFn.go
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 → (ofFn.go cont f j x)[i] = f { val := i, isLt := hi }) ∧ (i < j → (ofFn.go cont f j x)[i] = x[i])
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])