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

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

State before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ HookedAscending r as bs
Tactic:
constructor
State after:
case fst_lt_snd
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ List.forAllRel r as bs

case fst_revAscending
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending (flip r) as

case snd_Ascending
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r bs

State before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ List.forAllRel r as bs
Tactic:
case fst_lt_snd =>
  have := hhook.fst_lt_snd
  simp [List.forAllRel_cons_left] at this
  exact this.right
State after:
no goals

State before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending (flip r) as
Tactic:
case fst_revAscending => exact hhook.fst_revAscending.tail
State after:
no goals

State before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r bs
Tactic:
case snd_Ascending => exact hhook.snd_Ascending
State after:
no goals

State before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ List.forAllRel r as bs
Tactic:
have := hhook.fst_lt_snd
State after:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
this : List.forAllRel r (a :: as) bs
⊢ List.forAllRel r as bs

State before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
this : List.forAllRel r (a :: as) bs
⊢ List.forAllRel r as bs
Tactic:
simp [List.forAllRel_cons_left] at this
State after:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
this : forAll (r a) bs ∧ List.forAllRel r as bs
⊢ List.forAllRel r as bs

State before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
this : forAll (r a) bs ∧ List.forAllRel r as bs
⊢ List.forAllRel r as bs
Tactic:
exact this.right
State after:
no goals

State before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending (flip r) as
Tactic:
exact hhook.fst_revAscending.tail
State after:
no goals

State before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r bs
Tactic:
exact hhook.snd_Ascending
State after:
no goals