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

State before:
α : Type u
r : α → α → Prop
a : α
as : List α
⊢ Ascending r (a :: as) → predHead (r a) as
Tactic:
intro hchain
State after:
α : Type u
r : α → α → Prop
a : α
as : List α
hchain : Ascending r (a :: as)
⊢ predHead (r a) as

State before:
α : Type u
r : α → α → Prop
a : α
as : List α
hchain : Ascending r (a :: as)
⊢ predHead (r a) as
Tactic:
cases hchain
State after:
case singleton
α : Type u
r : α → α → Prop
a : α
⊢ predHead (r a) []

case cons
α : Type u
r : α → α → Prop
a b✝ : α
bs✝ : List α
a✝¹ : Ascending r (b✝ :: bs✝)
a✝ : r a b✝
⊢ predHead (r a) (b✝ :: bs✝)

State before:
α : Type u
r : α → α → Prop
a : α
⊢ predHead (r a) []
Tactic:
case singleton => exact True.intro
State after:
no goals

State before:
α : Type u
r : α → α → Prop
a b✝ : α
bs✝ : List α
a✝¹ : Ascending r (b✝ :: bs✝)
a✝ : r a b✝
⊢ predHead (r a) (b✝ :: bs✝)
Tactic:
case cons => exact ‹r a _›
State after:
no goals

State before:
α : Type u
r : α → α → Prop
a : α
⊢ predHead (r a) []
Tactic:
exact True.intro
State after:
no goals

State before:
α : Type u
r : α → α → Prop
a b✝ : α
bs✝ : List α
a✝¹ : Ascending r (b✝ :: bs✝)
a✝ : r a b✝
⊢ predHead (r a) (b✝ :: bs✝)
Tactic:
exact ‹r a _›
State after:
no goals