have ik : i.val ≤ k.val := by
  rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
  exact ik
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
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik : i.prev < k
kj : k < j.prev
⊢ swapped[k] < swapped[first]
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
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
k : Fin n
ik✝ : i.prev < k
kj : k < j.prev
ik : ↑i ≤ ↑k
⊢ swapped[k] < swapped[first]