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

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

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

State before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : i ≠ j
⊢ (a.val.set ⟨↑i, ⋯⟩ v)[↑j] = a.val[↑j]
Tactic:
exact Array.get_set_ne (j := j.val) a.val ⟨i, by simp [a.property, i.isLt]⟩ v
  (by simp [a.property, j.isLt]) (Fin.val_ne_of_ne h)
State after:
no goals

State before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : i ≠ j
⊢ ↑i < a.val.size
Tactic:
simp [a.property, i.isLt]
State after:
no goals

State before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : i ≠ j
⊢ ↑j < a.val.size
Tactic:
simp [a.property, j.isLt]
State after:
no goals