Theorem: quickSortImpl_sortedRange
Proof state before:
α : 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]
k : Fin n
mk : mid.val < k
kl : k ≤ last
p : permuted n (↑mid.val + 1) (↑last) (quickSortImpl parted.snd first mid.val.prev)
  (quickSortImpl (quickSortImpl parted.snd first mid.val.prev) (↑mid.val + 1) last) :=
  quickSortImpl_permuted (quickSortImpl parted.snd first mid.val.prev) (↑mid.val + 1) last
k' : Fin n
index : p.to_map k' = k
mk' : ↑mid.val + 1 ≤ ↑k'
kl' : ↑k' ≤ ↑last
inv : (quickSortImpl parted.snd first mid.val.prev)[k'] =
  (quickSortImpl (quickSortImpl parted.snd first mid.val.prev) (↑mid.val + 1) last)[k] :=
  index ▸ permuted_map_index p k'
⊢ ¬(quickSortImpl parted.snd first mid.val.prev)[k'] < arr[first]
Tactic:
have : mid.val.prev.val ≤ mid.val := by
  simp
  exact (Nat.sub_le ..)
Proof state after:
α : 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]
k : Fin n
mk : mid.val < k
kl : k ≤ last
p : permuted n (↑mid.val + 1) (↑last) (quickSortImpl parted.snd first mid.val.prev)
  (quickSortImpl (quickSortImpl parted.snd first mid.val.prev) (↑mid.val + 1) last) :=
  quickSortImpl_permuted (quickSortImpl parted.snd first mid.val.prev) (↑mid.val + 1) last
k' : Fin n
index : p.to_map k' = k
mk' : ↑mid.val + 1 ≤ ↑k'
kl' : ↑k' ≤ ↑last
inv : (quickSortImpl parted.snd first mid.val.prev)[k'] =
  (quickSortImpl (quickSortImpl parted.snd first mid.val.prev) (↑mid.val + 1) last)[k] :=
  index ▸ permuted_map_index p k'
this : ↑mid.val.prev ≤ ↑mid.val
⊢ ¬(quickSortImpl parted.snd first mid.val.prev)[k'] < arr[first]