Theorem: quickSortImpl_sortedRange
Proof state before:
case step
α : 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]
⊢ (compare (quickSortImpl (quickSortImpl parted.snd first parted.fst.val.prev) (↑parted.fst.val + 1) last)[i]
        (quickSortImpl (quickSortImpl parted.snd first parted.fst.val.prev) (↑parted.fst.val + 1) last)[j]).isLE =
    true
Tactic:
have getR (k : Fin n) (mk : mid.val < k) (kl : k ≤ last) : ¬sorted[k] <o arr[first] := by
  let p := quickSortImpl_permuted (quickSortImpl parted.snd first mid.val.prev) (mid.val + 1) last
  let ⟨k', ⟨index, mk', kl'⟩⟩ := permuted_map_index_in_range_inv p k mk kl
  let inv := index ▸ permuted_map_index p k'
  rw [←inv]
  have : mid.val.prev.val ≤ mid.val := by
    simp
    exact (Nat.sub_le ..)
  rw [quickSortImpl.get_gt (gt := Nat.lt_of_le_of_lt this mk')]
  apply r k' mk' kl'
Proof state after:
case step
α : 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]
⊢ (compare (quickSortImpl (quickSortImpl parted.snd first parted.fst.val.prev) (↑parted.fst.val + 1) last)[i]
        (quickSortImpl (quickSortImpl parted.snd first parted.fst.val.prev) (↑parted.fst.val + 1) last)[j]).isLE =
    true