Theorem: quickSort_sorted (QuickSortInLean/Sorted.lean)

State before:
α : Type
inst✝ : Order α
arr : Array α
⊢ sorted (quickSort arr)
Tactic:
let sr := quickSort'_sortedRange (arr : Vec α arr.size)
State after:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
⊢ sorted (quickSort arr)

State before:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
⊢ sorted (quickSort arr)
Tactic:
intro i j ij
State after:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
i j : Fin (quickSort arr).size
ij : i ≤ j
⊢ (compare (quickSort arr)[i] (quickSort arr)[j]).isLE = true

State before:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
i j : Fin (quickSort arr).size
ij : i ≤ j
⊢ (compare (quickSort arr)[i] (quickSort arr)[j]).isLE = true
Tactic:
have hi : 0 ≤ i.val := Nat.zero_le i.val
State after:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
i j : Fin (quickSort arr).size
ij : i ≤ j
hi : 0 ≤ ↑i
⊢ (compare (quickSort arr)[i] (quickSort arr)[j]).isLE = true

State before:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
i j : Fin (quickSort arr).size
ij : i ≤ j
hi : 0 ≤ ↑i
⊢ (compare (quickSort arr)[i] (quickSort arr)[j]).isLE = true
Tactic:
have s : (quickSort arr).size = arr.size := quickSort_size arr
State after:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
i j : Fin (quickSort arr).size
ij : i ≤ j
hi : 0 ≤ ↑i
s : (quickSort arr).size = arr.size
⊢ (compare (quickSort arr)[i] (quickSort arr)[j]).isLE = true

State before:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
i j : Fin (quickSort arr).size
ij : i ≤ j
hi : 0 ≤ ↑i
s : (quickSort arr).size = arr.size
⊢ (compare (quickSort arr)[i] (quickSort arr)[j]).isLE = true
Tactic:
have hj : j.val ≤ arr.size - 1 := Nat.le_sub_one_of_lt (s ▸ j.isLt)
State after:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
i j : Fin (quickSort arr).size
ij : i ≤ j
hi : 0 ≤ ↑i
s : (quickSort arr).size = arr.size
hj : ↑j ≤ arr.size - 1
⊢ (compare (quickSort arr)[i] (quickSort arr)[j]).isLE = true

State before:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
i j : Fin (quickSort arr).size
ij : i ≤ j
hi : 0 ≤ ↑i
s : (quickSort arr).size = arr.size
hj : ↑j ≤ arr.size - 1
⊢ (compare (quickSort arr)[i] (quickSort arr)[j]).isLE = true
Tactic:
exact sr (i.cast s) (j.cast s) hi ij hj
State after:
no goals