. exact permuted_map_invertible p
case left
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ invertible p.to_map

case right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ ∀ (i : Fin n), arr[i] = (quickSort' arr)[p.to_map i]
case right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ ∀ (i : Fin n), arr[i] = (quickSort' arr)[p.to_map i]