Theorem: List.Ascending.predHead_tail (Algdata/Data/List/Ascending.lean)

State before:
α : Type u
r : α → α → Prop
a : α
as : List α
p : α → Prop
⊢ (∀ (a b : α), p a → r a b → p b) → Ascending r (a :: as) → predHead p (a :: as) → predHead p as
Tactic:
intro hup hchain hpa
State after:
α : Type u
r : α → α → Prop
a : α
as : List α
p : α → Prop
hup : ∀ (a b : α), p a → r a b → p b
hchain : Ascending r (a :: as)
hpa : predHead p (a :: as)
⊢ predHead p as

State before:
α : Type u
r : α → α → Prop
a : α
as : List α
p : α → Prop
hup : ∀ (a b : α), p a → r a b → p b
hchain : Ascending r (a :: as)
hpa : predHead p (a :: as)
⊢ predHead p as
Tactic:
cases as
State after:
case nil
α : Type u
r : α → α → Prop
a : α
p : α → Prop
hup : ∀ (a b : α), p a → r a b → p b
hchain : Ascending r [a]
hpa : predHead p [a]
⊢ predHead p []

case cons
α : Type u
r : α → α → Prop
a : α
p : α → Prop
hup : ∀ (a b : α), p a → r a b → p b
head✝ : α
tail✝ : List α
hchain : Ascending r (a :: head✝ :: tail✝)
hpa : predHead p (a :: head✝ :: tail✝)
⊢ predHead p (head✝ :: tail✝)

State before:
α : Type u
r : α → α → Prop
a : α
p : α → Prop
hup : ∀ (a b : α), p a → r a b → p b
hchain : Ascending r [a]
hpa : predHead p [a]
⊢ predHead p []
Tactic:
case nil => exact True.intro
State after:
no goals

State before:
α : Type u
r : α → α → Prop
a : α
p : α → Prop
hup : ∀ (a b : α), p a → r a b → p b
a₁ : α
as : List α
hchain : Ascending r (a :: a₁ :: as)
hpa : predHead p (a :: a₁ :: as)
⊢ predHead p (a₁ :: as)
Tactic:
case cons a₁ as => exact hup a a₁ hpa hchain.head
State after:
no goals

State before:
α : Type u
r : α → α → Prop
a : α
p : α → Prop
hup : ∀ (a b : α), p a → r a b → p b
hchain : Ascending r [a]
hpa : predHead p [a]
⊢ predHead p []
Tactic:
exact True.intro
State after:
no goals

State before:
α : Type u
r : α → α → Prop
a : α
p : α → Prop
hup : ∀ (a b : α), p a → r a b → p b
a₁ : α
as : List α
hchain : Ascending r (a :: a₁ :: as)
hpa : predHead p (a :: a₁ :: as)
⊢ predHead p (a₁ :: as)
Tactic:
exact hup a a₁ hpa hchain.head
State after:
no goals