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

State before:
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
a b : α
j : Nat
hj : j < n
⊢ (set (set x i a) i b)[j] = (set x i b)[j]
Tactic:
if hij : i.1 = j then
  cases hij; simp only [get_set_eq]
else
  simp only [get_set_ne (h:=hij)]
State after:
no goals

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

State before:
case refl
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
a b : α
hj : ↑i < n
⊢ (set (set x i a) i b)[↑i] = (set x i b)[↑i]
Tactic:
simp only [get_set_eq]
State after:
no goals

State before:
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
a b : α
j : Nat
hj : j < n
hij : ¬↑i = j
⊢ (set (set x i a) i b)[j] = (set x i b)[j]
Tactic:
simp only [get_set_ne (h:=hij)]
State after:
no goals