Theorem: sorted_of_adjacentSorted (QuickSortInLean/AdjacentSorted.lean)

State before:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k : Nat
kn : k < n
jk : j ≤ k
⊢ arr[j] ≤ arr[k]
Tactic:
induction jk with
| refl => exact Order.refl
| step h ih =>
  apply Order.trans
  . exact ih (Nat.lt_of_le_of_lt (Nat.le_succ ..) kn)
  . apply assms
State after:
no goals

State before:
case refl
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k : Nat
kn : j < n
⊢ arr[j] ≤ arr[j]
Tactic:
exact Order.refl
State after:
no goals

State before:
case step
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ arr[j] ≤ arr[m✝.succ]
Tactic:
apply Order.trans
State after:
case step.a
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ arr[j] ≤ ?step.y

case step.a
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ ?step.y ≤ arr[m✝.succ]

case step.y
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ α

State before:
case step.a
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ arr[j] ≤ ?step.y

case step.a
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ ?step.y ≤ arr[m✝.succ]

case step.y
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ α
Tactic:
. exact ih (Nat.lt_of_le_of_lt (Nat.le_succ ..) kn)
State after:
case step.a
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ arr[m✝] ≤ arr[m✝.succ]

State before:
case step.a
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ arr[m✝] ≤ arr[m✝.succ]
Tactic:
. apply assms
State after:
no goals

State before:
case step.a
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ arr[j] ≤ ?step.y
Tactic:
exact ih (Nat.lt_of_le_of_lt (Nat.le_succ ..) kn)
State after:
no goals

State before:
case step.a
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ arr[m✝] ≤ arr[m✝.succ]
Tactic:
apply assms
State after:
no goals