Theorem: SizedArray.get_set_ite (Algdata/Data/Array/Sized.lean)

State before:
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
v : α
j : Nat
hj : j < n
⊢ (set x i v)[j] = if ↑i = j then v else x[j]
Tactic:
if hij : i.1 = j then
  cases hij; rw [if_pos rfl, get_set_eq]
else
  rw [get_set_ne (h:=hij), if_neg hij]
State after:
no goals

State before:
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
v : α
j : Nat
hj : j < n
hij : ↑i = j
⊢ (set x i v)[j] = if ↑i = j then v else x[j]
Tactic:
cases hij
State after:
case refl
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
v : α
hj : ↑i < n
⊢ (set x i v)[↑i] = if ↑i = ↑i then v else x[↑i]

State before:
case refl
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
v : α
hj : ↑i < n
⊢ (set x i v)[↑i] = if ↑i = ↑i then v else x[↑i]
Tactic:
rw [if_pos rfl, get_set_eq]
State after:
no goals

State before:
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
v : α
j : Nat
hj : j < n
hij : ¬↑i = j
⊢ (set x i v)[j] = if ↑i = j then v else x[j]
Tactic:
rw [get_set_ne (h:=hij), if_neg hij]
State after:
no goals