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

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last k : Fin n
gt : k > last
⊢ (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
gt : k > last
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
gt : k > last
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_gt gt
State after:
no goals