Theorem: List.HookedAscending.reelL (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 (b :: 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 (b :: 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 (b :: as) bs
Tactic:
have hlt := hhook.fst_lt_snd
State after:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : List.forAllRel r as (b :: bs)
⊢ HookedAscending r (b :: 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)
hlt : List.forAllRel r as (b :: bs)
⊢ HookedAscending r (b :: as) bs
Tactic:
rw [List.forAllRel_cons_right] at hlt
State after:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ HookedAscending r (b :: 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)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ HookedAscending r (b :: as) bs
Tactic:
constructor
State after:
case fst_lt_snd
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ List.forAllRel r (b :: as) bs

case fst_revAscending
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending (flip r) (b :: as)

case snd_Ascending
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending r bs

State before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ List.forAllRel r (b :: as) bs
Tactic:
case fst_lt_snd =>
  constructor
  case left => exact hhook.snd_Ascending.forAll_of_tail
  case right => exact hlt.right
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)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending (flip r) (b :: as)
Tactic:
case fst_revAscending =>
  exact List.Ascending.cons_of_forAll hlt.left hhook.fst_revAscending
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)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending r bs
Tactic:
case snd_Ascending => exact hhook.snd_Ascending.tail
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)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ List.forAllRel r (b :: as) bs
Tactic:
constructor
State after:
case left
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ (fun a => forAll (r a) bs) b

case right
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ forAll (fun a => forAll (r a) bs) as

State before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ (fun a => forAll (r a) bs) b
Tactic:
case left => exact hhook.snd_Ascending.forAll_of_tail
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)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ forAll (fun a => forAll (r a) bs) as
Tactic:
case right => exact hlt.right
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)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ (fun a => forAll (r a) bs) b
Tactic:
exact hhook.snd_Ascending.forAll_of_tail
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)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ forAll (fun a => forAll (r a) bs) as
Tactic:
exact hlt.right
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)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending (flip r) (b :: as)
Tactic:
exact List.Ascending.cons_of_forAll hlt.left hhook.fst_revAscending
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)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending r bs
Tactic:
exact hhook.snd_Ascending.tail
State after:
no goals