simp [afterLoop, dbgTraceIfShared]
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝⟩
this : result.fst = mid
⊢ (let result := partitionImpl arr first last last fl ⋯;
      let mid := result.fst;
      let arr_1 := result.snd;
      (mid, (dbgTraceIfShared "swap2" arr_1).swap first ⟨↑mid.val, ⋯⟩)).snd =
    swapped
no goals