. simp only [getElem]
  have lhs_rw := Array.get_set a ⟨i, i_size⟩ j j_size (f (Array.get a ⟨i, i_size⟩))
  simp only [getElem] at lhs_rw
  rw [lhs_rw]
  simp only [h, Array.get_eq_getElem, ite_false]
case isTrue
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[j] = a[j]

case isFalse
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
h✝ : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[j] = a[j]
case isFalse
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
h✝ : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[j] = a[j]