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

State before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
⊢ HookedAscending r as (b :: bs) → HookedAscending r as bs
Tactic:
intro hhook
State after:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
⊢ HookedAscending r as bs

State before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
⊢ HookedAscending r as bs
Tactic:
have : Trans (flip r) (flip r) (flip r) :=
  Trans.mk (by simp [flip]; exact flip trans)
State after:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
this : Trans (flip r) (flip r) (flip r)
⊢ HookedAscending r as bs

State before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
this : Trans (flip r) (flip r) (flip r)
⊢ HookedAscending r as bs
Tactic:
exact hhook.flip.tailL.flip
State after:
no goals

State before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
⊢ ∀ {a b c : α}, flip r a b → flip r b c → flip r a c
Tactic:
simp [flip]
State after:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
⊢ ∀ {a b c : α}, r b a → r c b → r c a

State before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
⊢ ∀ {a b c : α}, r b a → r c b → r c a
Tactic:
exact flip trans
State after:
no goals