induction arr, first, i, j, fi, ij using partitionImpl.induct with
| case1 arr first i j fi ij lt jl h prev ih =>
  unfold partitionImpl
  simp [*]
| @case2 arr first i j fi ij lt jl h swapped mid hm arr' eq ih =>
  unfold partitionImpl
  simp [*] at *
  have ⟨p₂⟩ := ih
  have p₁ : permuted n first j arr swapped := .step i j fi ij (Nat.le_refl _) .refl
  exact ⟨p₁.trans $ p₂.cast_last (Nat.sub_le ..)⟩
| case3 arr first i j fi ij jn =>
  simp [partitionImpl, *]
  exact ⟨.refl⟩
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
⊢ Nonempty (permuted n (↑first) (↑j) arr (partitionImpl arr first i j fi ij).snd)
no goals