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

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

case cons
α : Type u
r : α → α → Prop
a head✝ : α
tail✝ : List α
⊢ forAll (r a) (head✝ :: tail✝) → Ascending r (head✝ :: tail✝) → Ascending r (a :: head✝ :: tail✝)

State before:
α : Type u
r : α → α → Prop
a : α
⊢ forAll (r a) [] → Ascending r [] → Ascending r [a]
Tactic:
case nil => intros; exact Ascending.singleton a
State after:
no goals

State before:
α : Type u
r : α → α → Prop
a a₁ : α
as : List α
⊢ forAll (r a) (a₁ :: as) → Ascending r (a₁ :: as) → Ascending r (a :: a₁ :: as)
Tactic:
case cons a₁ as =>
  intro h
  exact Ascending.cons h.left
State after:
no goals

State before:
α : Type u
r : α → α → Prop
a : α
⊢ forAll (r a) [] → Ascending r [] → Ascending r [a]
Tactic:
intros
State after:
α : Type u
r : α → α → Prop
a : α
a✝¹ : forAll (r a) []
a✝ : Ascending r []
⊢ Ascending r [a]

State before:
α : Type u
r : α → α → Prop
a : α
a✝¹ : forAll (r a) []
a✝ : Ascending r []
⊢ Ascending r [a]
Tactic:
exact Ascending.singleton a
State after:
no goals

State before:
α : Type u
r : α → α → Prop
a a₁ : α
as : List α
⊢ forAll (r a) (a₁ :: as) → Ascending r (a₁ :: as) → Ascending r (a :: a₁ :: as)
Tactic:
intro h
State after:
α : Type u
r : α → α → Prop
a a₁ : α
as : List α
h : forAll (r a) (a₁ :: as)
⊢ Ascending r (a₁ :: as) → Ascending r (a :: a₁ :: as)

State before:
α : Type u
r : α → α → Prop
a a₁ : α
as : List α
h : forAll (r a) (a₁ :: as)
⊢ Ascending r (a₁ :: as) → Ascending r (a :: a₁ :: as)
Tactic:
exact Ascending.cons h.left
State after:
no goals