induction arr, first, i, j, fi, ij using partitionImpl.induct' with
| base => simp [*]
| step_lt => simp [*]
| step_ge arr first i j _ ij fi =>
  simp [*]
  have fj : first < j := Nat.lt_of_lt_of_le fi ij
  apply Vec.get_swap_neq
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_lt fi
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_lt fj
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
⊢ (partitionImpl arr first i j fi ij).snd[first] = arr[first]
no goals