Theorem: quickSortImpl.get_lt (QuickSortInLean/Sorted.lean)

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last k : Fin n
lt : ↑k < first
⊢ (quickSortImpl arr first last)[k] = arr[k]
Tactic:
let p := quickSortImpl_permuted arr first last
State after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last k : Fin n
lt : ↑k < first
p : permuted n first (↑last) arr (quickSortImpl arr first last) := quickSortImpl_permuted arr first last
⊢ (quickSortImpl arr first last)[k] = arr[k]

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last k : Fin n
lt : ↑k < first
p : permuted n first (↑last) arr (quickSortImpl arr first last) := quickSortImpl_permuted arr first last
⊢ (quickSortImpl arr first last)[k] = arr[k]
Tactic:
exact p.get_lt lt
State after:
no goals