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

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

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

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

State before:
α : Type u
r : α → α → Prop
p : α → Prop
a : α
as : List α
h_ind : (∀ (a b : α), p a → r a b → p b) → predHead p as → Ascending r as → forAll p as
⊢ (∀ (a b : α), p a → r a b → p b) → predHead p (a :: as) → Ascending r (a :: as) → forAll p (a :: as)
Tactic:
case cons a as h_ind =>
  intro hup hpa hchain
  exact ⟨hpa, h_ind hup (hchain.predHead_tail hup hpa) hchain.tail⟩
State after:
no goals

State before:
α : Type u
r : α → α → Prop
p : α → Prop
⊢ (∀ (a b : α), p a → r a b → p b) → predHead p [] → Ascending r [] → forAll p []
Tactic:
intros
State after:
α : Type u
r : α → α → Prop
p : α → Prop
a✝² : ∀ (a b : α), p a → r a b → p b
a✝¹ : predHead p []
a✝ : Ascending r []
⊢ forAll p []

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

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

State before:
α : Type u
r : α → α → Prop
p : α → Prop
a : α
as : List α
h_ind : (∀ (a b : α), p a → r a b → p b) → predHead p as → Ascending r as → forAll p as
hup : ∀ (a b : α), p a → r a b → p b
hpa : predHead p (a :: as)
hchain : Ascending r (a :: as)
⊢ forAll p (a :: as)
Tactic:
exact ⟨hpa, h_ind hup (hchain.predHead_tail hup hpa) hchain.tail⟩
State after:
no goals