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

State before:
α : Type u
r : α → α → Prop
as bs : List α
⊢ Ascending r (as ++ bs) → Ascending r bs
Tactic:
induction as
State after:
case nil
α : Type u
r : α → α → Prop
bs : List α
⊢ Ascending r ([] ++ bs) → Ascending r bs

case cons
α : Type u
r : α → α → Prop
bs : List α
head✝ : α
tail✝ : List α
tail_ih✝ : Ascending r (tail✝ ++ bs) → Ascending r bs
⊢ Ascending r (head✝ :: tail✝ ++ bs) → Ascending r bs

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

State before:
α : Type u
r : α → α → Prop
bs : List α
head✝ : α
tail✝ : List α
h_ind : Ascending r (tail✝ ++ bs) → Ascending r bs
⊢ Ascending r (head✝ :: tail✝ ++ bs) → Ascending r bs
Tactic:
case cons _ _ h_ind => exact h_ind ∘ Ascending.tail
State after:
no goals

State before:
α : Type u
r : α → α → Prop
bs : List α
⊢ Ascending r ([] ++ bs) → Ascending r bs
Tactic:
exact id
State after:
no goals

State before:
α : Type u
r : α → α → Prop
bs : List α
head✝ : α
tail✝ : List α
h_ind : Ascending r (tail✝ ++ bs) → Ascending r bs
⊢ Ascending r (head✝ :: tail✝ ++ bs) → Ascending r bs
Tactic:
exact h_ind ∘ Ascending.tail
State after:
no goals