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

State before:
α : Type
n : Nat
a : Vec α n
i : Fin n
v : α
⊢ (a.set i v)[i] = v
Tactic:
show (a.set i v).get i = v
State after:
α : Type
n : Nat
a : Vec α n
i : Fin n
v : α
⊢ (a.set i v).get i = v

State before:
α : Type
n : Nat
a : Vec α n
i : Fin n
v : α
⊢ (a.set i v).get i = v
Tactic:
simp [Vec.get, Vec.set]
State after:
no goals