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

State before:
α : Type u_1
r : α → α → Prop
as bs : List α
hhook : HookedAscending r as bs
⊢ List.forAllRel (flip r) bs as
Tactic:
simp
State after:
α : Type u_1
r : α → α → Prop
as bs : List α
hhook : HookedAscending r as bs
⊢ List.forAllRel r as bs

State before:
α : Type u_1
r : α → α → Prop
as bs : List α
hhook : HookedAscending r as bs
⊢ List.forAllRel r as bs
Tactic:
exact hhook.fst_lt_snd
State after:
no goals

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

State before:
α : Type u_1
r : α → α → Prop
as bs : List α
hhook : HookedAscending r as bs
this : ∀ (a b : α), r a b → flip (flip r) a b
⊢ Ascending (flip (flip r)) bs
Tactic:
apply Ascending.of_implies this
State after:
α : Type u_1
r : α → α → Prop
as bs : List α
hhook : HookedAscending r as bs
this : ∀ (a b : α), r a b → flip (flip r) a b
⊢ Ascending (fun a b => r a b) bs

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