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

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

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

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

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

State before:
α : Type u
r : α → α → Prop
a' : α
as : List α
h_ind :
  ∀ {a : α} {bs : List α}, Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux (a :: as) bs)
a : α
bs : List α
⊢ Ascending (flip r) (a :: a' :: as) → Ascending r (a :: bs) → Ascending r (reverseAux as (a' :: a :: bs))
Tactic:
case cons a' as h_ind =>
  intro haaas habs
  simp [reverseAux] at h_ind
  cases haaas with | cons haa haas =>
  apply h_ind haas (habs.cons haa)
State after:
no goals

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

State before:
α : Type u
r : α → α → Prop
a' : α
as : List α
h_ind :
  ∀ {a : α} {bs : List α}, Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux (a :: as) bs)
a : α
bs : List α
⊢ Ascending (flip r) (a :: a' :: as) → Ascending r (a :: bs) → Ascending r (reverseAux as (a' :: a :: bs))
Tactic:
intro haaas habs
State after:
α : Type u
r : α → α → Prop
a' : α
as : List α
h_ind :
  ∀ {a : α} {bs : List α}, Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux (a :: as) bs)
a : α
bs : List α
haaas : Ascending (flip r) (a :: a' :: as)
habs : Ascending r (a :: bs)
⊢ Ascending r (reverseAux as (a' :: a :: bs))

State before:
α : Type u
r : α → α → Prop
a' : α
as : List α
h_ind :
  ∀ {a : α} {bs : List α}, Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux (a :: as) bs)
a : α
bs : List α
haaas : Ascending (flip r) (a :: a' :: as)
habs : Ascending r (a :: bs)
⊢ Ascending r (reverseAux as (a' :: a :: bs))
Tactic:
simp [reverseAux] at h_ind
State after:
α : Type u
r : α → α → Prop
a' : α
as : List α
h_ind :
  ∀ {a : α} {bs : List α}, Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux as (a :: bs))
a : α
bs : List α
haaas : Ascending (flip r) (a :: a' :: as)
habs : Ascending r (a :: bs)
⊢ Ascending r (reverseAux as (a' :: a :: bs))

State before:
α : Type u
r : α → α → Prop
a' : α
as : List α
h_ind :
  ∀ {a : α} {bs : List α}, Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux as (a :: bs))
a : α
bs : List α
haaas : Ascending (flip r) (a :: a' :: as)
habs : Ascending r (a :: bs)
⊢ Ascending r (reverseAux as (a' :: a :: bs))
Tactic:
cases haaas with | cons haa haas =>
apply h_ind haas (habs.cons haa)
State after:
no goals

State before:
case cons
α : Type u
r : α → α → Prop
a' : α
as : List α
h_ind :
  ∀ {a : α} {bs : List α}, Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux as (a :: bs))
a : α
bs : List α
habs : Ascending r (a :: bs)
haa : flip r a a'
haas : Ascending (flip r) (a' :: as)
⊢ Ascending r (reverseAux as (a' :: a :: bs))
Tactic:
apply h_ind haas (habs.cons haa)
State after:
no goals