rw [lhs_rw]
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
lhs_rw :
  (a.set ⟨i, i_in_bounds⟩ (f (a.get ⟨i, i_in_bounds⟩))).get ⟨i, ⋯⟩ =
    if True then f (a.get ⟨i, i_in_bounds⟩) else a.get ⟨i, i_in_bounds⟩
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).get ⟨i, ⋯⟩ = f (a.get ⟨i, i_in_bounds⟩)
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
lhs_rw :
  (a.set ⟨i, i_in_bounds⟩ (f (a.get ⟨i, i_in_bounds⟩))).get ⟨i, ⋯⟩ =
    if True then f (a.get ⟨i, i_in_bounds⟩) else a.get ⟨i, i_in_bounds⟩
⊢ (if True then f (a.get ⟨i, i_in_bounds⟩) else a.get ⟨i, i_in_bounds⟩) = f (a.get ⟨i, i_in_bounds⟩)