apply Fin.eq_of_val_eq
α : 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]
k : Fin n
eq : ↑mid.val = ↑k
mid' : Fin n := ⟨↑mid.val, mn⟩
⊢ k = mid'
case a
α : 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]
k : Fin n
eq : ↑mid.val = ↑k
mid' : Fin n := ⟨↑mid.val, mn⟩
⊢ ↑k = ↑mid'