. intro ij
  have ij : i.val ≤ j.val := by
    rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
    exact ij
  cases Nat.eq_or_lt_of_le ij with
  | inl ij =>
    simp [Fin.eq_of_val_eq ij.symm]
    assumption
  | inr ij => exact inv.3 ij
case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
⊢ i.prev < j → arr[j] < arr[first]
no goals