Theorem: quickSortImpl_sortedRange
Proof state before:
case step.split
α : 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]
getLM : ∀ (k : Fin n), first ≤ ↑k → k ≤ mid.val → sorted[k] ≤ arr[first]
getMR : ∀ (k : Fin n), mid.val ≤ k → k ≤ last → ¬sorted[k] < arr[first]
im : ↑i ≤ ↑mid.val
mj : ↑mid.val ≤ ↑j
h₁ : sorted[i] ≤ 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 h₂ : arr[first] ≤o sorted[j] := Order.le_of_not_lt (getMR j mj jl)
Proof state after:
case step.split
α : 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]
getLM : ∀ (k : Fin n), first ≤ ↑k → k ≤ mid.val → sorted[k] ≤ arr[first]
getMR : ∀ (k : Fin n), mid.val ≤ k → k ≤ last → ¬sorted[k] < arr[first]
im : ↑i ≤ ↑mid.val
mj : ↑mid.val ≤ ↑j
h₁ : sorted[i] ≤ arr[first]
h₂ : arr[first] ≤ sorted[j]
⊢ (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