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

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