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

State before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ (a.swap i j)[i] = a[j]
Tactic:
simp [Vec.swap_def, Vec.get_set, Vec.get_set_eq]
State after:
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ (if j = i then a.get i else a.get j) = a[j]

State before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ (if j = i then a.get i else a.get j) = a[j]
Tactic:
cases decEq j i <;> simp [*] <;> rfl
State after:
no goals