let inv₀ : partitionImpl.LoopInvariant arr first last last last := by
  apply partitionImpl.LoopInvariant.intro
  . intro k lk kl
    exact (Nat.lt_irrefl k (Nat.lt_trans kl lk)).elim
  . intro k lk kl
    exact (Nat.lt_irrefl k (Nat.lt_of_le_of_lt kl lk)).elim
  . intro ll
    exact (Nat.lt_irrefl last ll).elim
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
⊢ (∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]) ∧
    result.snd[result.fst.val] = arr[first] ∧
      ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]