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

State before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ a.swap i j = (a.set i (a.get j)).set j (a.get i)
Tactic:
simp [Vec.swap]
State after:
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ ⟨a.val.swap (Fin.cast ⋯ i) (Fin.cast ⋯ j), ⋯⟩ = (a.set i (a.get j)).set j (a.get i)

State before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ ⟨a.val.swap (Fin.cast ⋯ i) (Fin.cast ⋯ j), ⋯⟩ = (a.set i (a.get j)).set j (a.get i)
Tactic:
apply Subtype.eq
State after:
case a
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ ⟨a.val.swap (Fin.cast ⋯ i) (Fin.cast ⋯ j), ⋯⟩.val = ((a.set i (a.get j)).set j (a.get i)).val

State before:
case a
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ ⟨a.val.swap (Fin.cast ⋯ i) (Fin.cast ⋯ j), ⋯⟩.val = ((a.set i (a.get j)).set j (a.get i)).val
Tactic:
simp [Vec.get, Vec.set, Array.swap_def]
State after:
case a
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ (a.val.set (Fin.cast ⋯ i) a.val[↑j]).set ⟨↑j, ⋯⟩ a.val[↑i] = (a.val.set ⟨↑i, ⋯⟩ a.val[↑j]).set ⟨↑j, ⋯⟩ a.val[↑i]

State before:
case a
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ (a.val.set (Fin.cast ⋯ i) a.val[↑j]).set ⟨↑j, ⋯⟩ a.val[↑i] = (a.val.set ⟨↑i, ⋯⟩ a.val[↑j]).set ⟨↑j, ⋯⟩ a.val[↑i]
Tactic:
rfl
State after:
no goals