cases Nat.eq_or_lt_of_le (Nat.le_of_succ_le_succ hij) with
| inl heq =>
  cases (Fin.eq_of_val_eq heq)
  simp only [get_set_eq ys]
  exact congrArg _ <| (IH j).2 .refl
| inr hlt =>
  have : j.1 ≠ k.1 := Ne.symm <| Nat.ne_of_lt hlt
  simp only [get_set_ne ys this]
  exact (IH k).1 hlt
case left
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k < ↑j + 1
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]
no goals