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

State before:
α : Type u_1
r : α → α → Prop
as bs : List α
⊢ HookedAscending r as bs → Ascending r (reverseAux as bs)
Tactic:
cases as <;> simp
State after:
case nil
α : Type u_1
r : α → α → Prop
bs : List α
⊢ HookedAscending r [] bs → Ascending r bs

case cons
α : Type u_1
r : α → α → Prop
bs : List α
head✝ : α
tail✝ : List α
⊢ HookedAscending r (head✝ :: tail✝) bs → Ascending r (reverseAux tail✝ (head✝ :: bs))

State before:
α : Type u_1
r : α → α → Prop
bs : List α
⊢ HookedAscending r [] bs → Ascending r bs
Tactic:
case nil => exact HookedAscending.snd_Ascending
State after:
no goals

State before:
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
⊢ HookedAscending r (a :: as) bs → Ascending r (reverseAux as (a :: bs))
Tactic:
case cons a as =>
  intro hhook
  apply Ascending.reverseAux_cons
  . exact hhook.fst_revAscending
  . apply Ascending.cons_of_forAll _ hhook.snd_Ascending
    have := hhook.fst_lt_snd
    rw [List.forAllRel_cons_left] at this
    exact this.left
State after:
no goals

State before:
α : Type u_1
r : α → α → Prop
bs : List α
⊢ HookedAscending r [] bs → Ascending r bs
Tactic:
exact HookedAscending.snd_Ascending
State after:
no goals

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

State before:
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r (reverseAux as (a :: bs))
Tactic:
apply Ascending.reverseAux_cons
State after:
case a
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending (flip r) (a :: as)

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

State before:
case a
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending (flip r) (a :: as)

case a
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r (a :: bs)
Tactic:
. exact hhook.fst_revAscending
State after:
case a
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r (a :: bs)

State before:
case a
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r (a :: bs)
Tactic:
. apply Ascending.cons_of_forAll _ hhook.snd_Ascending
  have := hhook.fst_lt_snd
  rw [List.forAllRel_cons_left] at this
  exact this.left
State after:
no goals

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

State before:
case a
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r (a :: bs)
Tactic:
apply Ascending.cons_of_forAll _ hhook.snd_Ascending
State after:
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ forAll (r a) bs

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

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

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