Theorem: quickSort'_sortedRange (QuickSortInLean/Sorted.lean)

State before:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
⊢ sortedRange (quickSort' arr) 0 (n - 1)
Tactic:
if h : n > 0 then
  simp [quickSort', h]
  apply quickSortImpl_sortedRange
else
  intro i
  have : n = 0 := Nat.eq_zero_of_not_pos h
  subst n
  exact (Nat.not_lt_zero i.val i.isLt).elim
State after:
no goals

State before:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : n > 0
⊢ sortedRange (quickSort' arr) 0 (n - 1)
Tactic:
simp [quickSort', h]
State after:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : n > 0
⊢ sortedRange (quickSortImpl arr 0 ⟨n - 1, ⋯⟩) 0 (n - 1)

State before:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : n > 0
⊢ sortedRange (quickSortImpl arr 0 ⟨n - 1, ⋯⟩) 0 (n - 1)
Tactic:
apply quickSortImpl_sortedRange
State after:
no goals

State before:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : ¬n > 0
⊢ sortedRange (quickSort' arr) 0 (n - 1)
Tactic:
intro i
State after:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : ¬n > 0
i : Fin n
⊢ ∀ (j : Fin n), 0 ≤ ↑i → i ≤ j → ↑j ≤ n - 1 → (compare (quickSort' arr)[i] (quickSort' arr)[j]).isLE = true

State before:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : ¬n > 0
i : Fin n
⊢ ∀ (j : Fin n), 0 ≤ ↑i → i ≤ j → ↑j ≤ n - 1 → (compare (quickSort' arr)[i] (quickSort' arr)[j]).isLE = true
Tactic:
have : n = 0 := Nat.eq_zero_of_not_pos h
State after:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : ¬n > 0
i : Fin n
this : n = 0
⊢ ∀ (j : Fin n), 0 ≤ ↑i → i ≤ j → ↑j ≤ n - 1 → (compare (quickSort' arr)[i] (quickSort' arr)[j]).isLE = true

State before:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : ¬n > 0
i : Fin n
this : n = 0
⊢ ∀ (j : Fin n), 0 ≤ ↑i → i ≤ j → ↑j ≤ n - 1 → (compare (quickSort' arr)[i] (quickSort' arr)[j]).isLE = true
Tactic:
subst n
State after:
α : Type
inst✝ : Order α
arr : Vec α 0
h : ¬0 > 0
i : Fin 0
⊢ ∀ (j : Fin 0), 0 ≤ ↑i → i ≤ j → ↑j ≤ 0 - 1 → (compare (quickSort' arr)[i] (quickSort' arr)[j]).isLE = true

State before:
α : Type
inst✝ : Order α
arr : Vec α 0
h : ¬0 > 0
i : Fin 0
⊢ ∀ (j : Fin 0), 0 ≤ ↑i → i ≤ j → ↑j ≤ 0 - 1 → (compare (quickSort' arr)[i] (quickSort' arr)[j]).isLE = true
Tactic:
exact (Nat.not_lt_zero i.val i.isLt).elim
State after:
no goals