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

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

State before:
α : Type u_1
r : α → α → Prop
as : List α
b : α
bs : List α
has : forAll (fun x => r x b) as
hbs : forAll (r b) bs
hhook : HookedAscending r as bs
⊢ HookedAscending r as (b :: bs)
Tactic:
have : ∀ a b, flip (flip r) a b → r a b := λ _ _ => id
State after:
α : Type u_1
r : α → α → Prop
as : List α
b : α
bs : List α
has : forAll (fun x => r x b) as
hbs : forAll (r b) bs
hhook : HookedAscending r as bs
this : ∀ (a b : α), flip (flip r) a b → r a b
⊢ HookedAscending r as (b :: bs)

State before:
α : Type u_1
r : α → α → Prop
as : List α
b : α
bs : List α
has : forAll (fun x => r x b) as
hbs : forAll (r b) bs
hhook : HookedAscending r as bs
this : ∀ (a b : α), flip (flip r) a b → r a b
⊢ HookedAscending r as (b :: bs)
Tactic:
exact (hhook.flip.consL hbs has).flip.of_implies this
State after:
no goals