Theorem: Vec.get_set (QuickSortInLean/Vec.lean)

State before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
⊢ (a.set i v)[j] = if i = j then v else a[j]
Tactic:
if h : i = j then
  simp [h]
  exact Vec.get_set_eq a j v
else
  simp [h]
  exact Vec.get_set_ne a i j v h
State after:
no goals

State before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : i = j
⊢ (a.set i v)[j] = if i = j then v else a[j]
Tactic:
simp [h]
State after:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : i = j
⊢ (a.set j v)[j] = v

State before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : i = j
⊢ (a.set j v)[j] = v
Tactic:
exact Vec.get_set_eq a j v
State after:
no goals

State before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : ¬i = j
⊢ (a.set i v)[j] = if i = j then v else a[j]
Tactic:
simp [h]
State after:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : ¬i = j
⊢ (a.set i v)[j] = a[j]

State before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : ¬i = j
⊢ (a.set i v)[j] = a[j]
Tactic:
exact Vec.get_set_ne a i j v h
State after:
no goals