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

State before:
α : Type
n : Nat
a : Vec α n
i j k : Fin n
ki : k ≠ i
kj : k ≠ j
⊢ (a.swap i j)[k] = a[k]
Tactic:
simp [Vec.swap_def]
State after:
α : Type
n : Nat
a : Vec α n
i j k : Fin n
ki : k ≠ i
kj : k ≠ j
⊢ ((a.set i (a.get j)).set j (a.get i))[k] = a[k]

State before:
α : Type
n : Nat
a : Vec α n
i j k : Fin n
ki : k ≠ i
kj : k ≠ j
⊢ ((a.set i (a.get j)).set j (a.get i))[k] = a[k]
Tactic:
rw [Vec.get_set_ne (h := kj.symm), Vec.get_set_ne (h := ki.symm)]
State after:
no goals