Theorem: List.Ascending.reverseAux (Algdata/Data/List/Ascending.lean)

State before:
α : Type u
r : α → α → Prop
as bs : List α
⊢ relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
Tactic:
revert bs
State after:
α : Type u
r : α → α → Prop
as : List α
⊢ ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)

State before:
α : Type u
r : α → α → Prop
as : List α
⊢ ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
Tactic:
induction as <;> intro bs
State after:
case nil
α : Type u
r : α → α → Prop
bs : List α
⊢ relHead r [] bs → Ascending (flip r) [] → Ascending r bs → Ascending r (List.reverseAux [] bs)

case cons
α : Type u
r : α → α → Prop
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ {bs : List α},
    relHead r tail✝ bs → Ascending (flip r) tail✝ → Ascending r bs → Ascending r (List.reverseAux tail✝ bs)
bs : List α
⊢ relHead r (head✝ :: tail✝) bs →
    Ascending (flip r) (head✝ :: tail✝) → Ascending r bs → Ascending r (List.reverseAux (head✝ :: tail✝) bs)

State before:
α : Type u
r : α → α → Prop
bs : List α
⊢ relHead r [] bs → Ascending (flip r) [] → Ascending r bs → Ascending r (List.reverseAux [] bs)
Tactic:
case nil => exact λ _ _ => id
State after:
no goals

State before:
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
⊢ relHead r (a :: as) bs → Ascending (flip r) (a :: as) → Ascending r bs → Ascending r (List.reverseAux (a :: as) bs)
Tactic:
case cons a as h_ind =>
  intro hhead has hbs
  unfold List.reverseAux
  apply h_ind
  . exact relHead_cons_right ▸ has.head
  . exact has.tail
  . exact hbs.cons_of_head_tail (relHead_cons_left ▸ hhead)
State after:
no goals

State before:
α : Type u
r : α → α → Prop
bs : List α
⊢ relHead r [] bs → Ascending (flip r) [] → Ascending r bs → Ascending r (List.reverseAux [] bs)
Tactic:
exact λ _ _ => id
State after:
no goals

State before:
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
⊢ relHead r (a :: as) bs → Ascending (flip r) (a :: as) → Ascending r bs → Ascending r (List.reverseAux (a :: as) bs)
Tactic:
intro hhead has hbs
State after:
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (List.reverseAux (a :: as) bs)

State before:
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (List.reverseAux (a :: as) bs)
Tactic:
unfold List.reverseAux
State after:
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (List.reverseAux as (a :: bs))

State before:
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (List.reverseAux as (a :: bs))
Tactic:
apply h_ind
State after:
case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ relHead r as (a :: bs)

case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending (flip r) as

case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (a :: bs)

State before:
case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ relHead r as (a :: bs)

case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending (flip r) as

case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (a :: bs)
Tactic:
. exact relHead_cons_right ▸ has.head
State after:
case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending (flip r) as

case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (a :: bs)

State before:
case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending (flip r) as

case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (a :: bs)
Tactic:
. exact has.tail
State after:
case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (a :: bs)

State before:
case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (a :: bs)
Tactic:
. exact hbs.cons_of_head_tail (relHead_cons_left ▸ hhead)
State after:
no goals

State before:
case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ relHead r as (a :: bs)
Tactic:
exact relHead_cons_right ▸ has.head
State after:
no goals

State before:
case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending (flip r) as
Tactic:
exact has.tail
State after:
no goals

State before:
case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (a :: bs)
Tactic:
exact hbs.cons_of_head_tail (relHead_cons_left ▸ hhead)
State after:
no goals