Theorem: quickSort_size (QuickSortInLean/Sorted.lean)

State before:
α : Type
inst✝ : Order α
arr : Array α
⊢ (quickSort arr).size = arr.size
Tactic:
let sorted := quickSort' ⟨arr, rfl⟩
State after:
α : Type
inst✝ : Order α
arr : Array α
sorted : Vec α arr.size := quickSort' ⟨arr, ⋯⟩
⊢ (quickSort arr).size = arr.size

State before:
α : Type
inst✝ : Order α
arr : Array α
sorted : Vec α arr.size := quickSort' ⟨arr, ⋯⟩
⊢ (quickSort arr).size = arr.size
Tactic:
show sorted.val.size = arr.size
State after:
α : Type
inst✝ : Order α
arr : Array α
sorted : Vec α arr.size := quickSort' ⟨arr, ⋯⟩
⊢ sorted.val.size = arr.size

State before:
α : Type
inst✝ : Order α
arr : Array α
sorted : Vec α arr.size := quickSort' ⟨arr, ⋯⟩
⊢ sorted.val.size = arr.size
Tactic:
simp [sorted.property]
State after:
no goals