Theorem: List.HookedAscending.consL (Algdata/Data/List/Ascending.lean)

State before:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
⊢ forAll (fun x => r x a) as → forAll (r a) bs → HookedAscending r as bs → HookedAscending r (a :: as) bs
Tactic:
intro has hbs hhook
State after:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ HookedAscending r (a :: as) bs

State before:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ HookedAscending r (a :: as) bs
Tactic:
constructor
State after:
case fst_lt_snd
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ List.forAllRel r (a :: as) bs

case fst_revAscending
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ Ascending (flip r) (a :: as)

case snd_Ascending
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ Ascending r bs

State before:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ List.forAllRel r (a :: as) bs
Tactic:
case fst_lt_snd =>
  simp [List.forAllRel_cons_left]
  exact And.intro hbs hhook.fst_lt_snd
State after:
no goals

State before:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ Ascending (flip r) (a :: as)
Tactic:
case fst_revAscending =>
  exact List.Ascending.cons_of_forAll has hhook.fst_revAscending
State after:
no goals

State before:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ Ascending r bs
Tactic:
case snd_Ascending => exact hhook.snd_Ascending
State after:
no goals

State before:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ List.forAllRel r (a :: as) bs
Tactic:
simp [List.forAllRel_cons_left]
State after:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ forAll (r a) bs ∧ List.forAllRel r as bs

State before:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ forAll (r a) bs ∧ List.forAllRel r as bs
Tactic:
exact And.intro hbs hhook.fst_lt_snd
State after:
no goals

State before:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ Ascending (flip r) (a :: as)
Tactic:
exact List.Ascending.cons_of_forAll has hhook.fst_revAscending
State after:
no goals

State before:
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ Ascending r bs
Tactic:
exact hhook.snd_Ascending
State after:
no goals