apply Order.refl
case inl
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
lt : first < ↑last
parted : { mid // first ≤ ↑mid ∧ mid ≤ last } × Vec α n
eq : partition arr ⟨first, ⋯⟩ last ⋯ = parted
ih₁ : sortedRange (quickSortImpl parted.snd first parted.fst.val.prev) first ↑parted.fst.val.prev
ih₂ :
  sortedRange (quickSortImpl (quickSortImpl parted.snd first parted.fst.val.prev) (↑parted.fst.val + 1) last)
    (↑parted.fst.val + 1) ↑last
this : first < n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ ↑last
mid : { mid // first ≤ ↑mid ∧ mid ≤ last } := parted.fst
mn : ↑mid.val < n
sorted : Vec α n := quickSortImpl (quickSortImpl parted.snd first mid.val.prev) (↑mid.val + 1) last
l : ∀ (k : Fin n), ⟨first, this⟩ ≤ k → ↑k < ↑parted.fst.val → parted.snd[k] < arr[⟨first, this⟩]
m : parted.snd[parted.fst.val] = arr[⟨first, this⟩]
r : ∀ (k : Fin n), ↑parted.fst.val < ↑k → k ≤ last → ¬parted.snd[k] < arr[⟨first, this⟩]
getL : ∀ (k : Fin n), first ≤ ↑k → k < mid.val → sorted[k] < arr[first]
getM : ∀ (k : Fin n), ↑mid.val = ↑k → sorted[k] = arr[first]
getR : ∀ (k : Fin n), mid.val < k → k ≤ last → ¬sorted[k] < arr[first]
k : Fin n
fk : first ≤ ↑k
km✝ : k ≤ mid.val
km : ↑k = ↑mid.val
⊢ arr[first] ≤ arr[first]
no goals