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

State before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a : α
as : List α
⊢ Ascending r (a :: as) → forAll (r a) as
Tactic:
revert a
State after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
as : List α
⊢ ∀ {a : α}, Ascending r (a :: as) → forAll (r a) as

State before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
as : List α
⊢ ∀ {a : α}, Ascending r (a :: as) → forAll (r a) as
Tactic:
induction as <;> intro a h
State after:
case nil
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a : α
h : Ascending r [a]
⊢ forAll (r a) []

case cons
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {a : α}, Ascending r (a :: tail✝) → forAll (r a) tail✝
a : α
h : Ascending r (a :: head✝ :: tail✝)
⊢ forAll (r a) (head✝ :: tail✝)

State before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a : α
h : Ascending r [a]
⊢ forAll (r a) []
Tactic:
case nil => exact True.intro
State after:
no goals

State before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a₁ : α
as : List α
h_ind : ∀ {a : α}, Ascending r (a :: as) → forAll (r a) as
a : α
h : Ascending r (a :: a₁ :: as)
⊢ forAll (r a) (a₁ :: as)
Tactic:
case cons a₁ as h_ind =>
  cases h with | cons ha htail =>
  have : as.forAll (r a) :=
    forAll_of_forAll (λ x => trans ha) $ h_ind htail
  exact And.intro ha this
State after:
no goals

State before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a : α
h : Ascending r [a]
⊢ forAll (r a) []
Tactic:
exact True.intro
State after:
no goals

State before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a₁ : α
as : List α
h_ind : ∀ {a : α}, Ascending r (a :: as) → forAll (r a) as
a : α
h : Ascending r (a :: a₁ :: as)
⊢ forAll (r a) (a₁ :: as)
Tactic:
cases h with | cons ha htail =>
have : as.forAll (r a) :=
  forAll_of_forAll (λ x => trans ha) $ h_ind htail
exact And.intro ha this
State after:
no goals

State before:
case cons
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a₁ : α
as : List α
h_ind : ∀ {a : α}, Ascending r (a :: as) → forAll (r a) as
a : α
ha : r a a₁
htail : Ascending r (a₁ :: as)
⊢ forAll (r a) (a₁ :: as)
Tactic:
have : as.forAll (r a) :=
  forAll_of_forAll (λ x => trans ha) $ h_ind htail
State after:
case cons
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a₁ : α
as : List α
h_ind : ∀ {a : α}, Ascending r (a :: as) → forAll (r a) as
a : α
ha : r a a₁
htail : Ascending r (a₁ :: as)
this : forAll (r a) as
⊢ forAll (r a) (a₁ :: as)

State before:
case cons
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a₁ : α
as : List α
h_ind : ∀ {a : α}, Ascending r (a :: as) → forAll (r a) as
a : α
ha : r a a₁
htail : Ascending r (a₁ :: as)
this : forAll (r a) as
⊢ forAll (r a) (a₁ :: as)
Tactic:
exact And.intro ha this
State after:
no goals