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

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

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

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

State before:
α : Type u
r : α → α → Prop
bs : List α
a : α
as : List α
h_ind : Ascending r (as ++ bs) → Ascending r as
⊢ Ascending r (a :: as ++ bs) → Ascending r (a :: as)
Tactic:
case cons a as h_ind =>
  cases as
  case nil => exact λ _ => Ascending.singleton a
  case cons a₁ as =>
    simp [List.cons_append] at *
    intro has; cases has with | cons ha htail =>
    exact Ascending.cons ha (h_ind htail)
State after:
no goals

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

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

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

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

State before:
α : Type u
r : α → α → Prop
bs : List α
a a₁ : α
as : List α
h_ind : Ascending r (a₁ :: as ++ bs) → Ascending r (a₁ :: as)
⊢ Ascending r (a :: a₁ :: as ++ bs) → Ascending r (a :: a₁ :: as)
Tactic:
case cons a₁ as =>
  simp [List.cons_append] at *
  intro has; cases has with | cons ha htail =>
  exact Ascending.cons ha (h_ind htail)
State after:
no goals

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

State before:
α : Type u
r : α → α → Prop
bs : List α
a a₁ : α
as : List α
h_ind : Ascending r (a₁ :: as ++ bs) → Ascending r (a₁ :: as)
⊢ Ascending r (a :: a₁ :: as ++ bs) → Ascending r (a :: a₁ :: as)
Tactic:
simp [List.cons_append] at *
State after:
α : Type u
r : α → α → Prop
bs : List α
a a₁ : α
as : List α
h_ind : Ascending r (a₁ :: (as ++ bs)) → Ascending r (a₁ :: as)
⊢ Ascending r (a :: a₁ :: (as ++ bs)) → Ascending r (a :: a₁ :: as)

State before:
α : Type u
r : α → α → Prop
bs : List α
a a₁ : α
as : List α
h_ind : Ascending r (a₁ :: (as ++ bs)) → Ascending r (a₁ :: as)
⊢ Ascending r (a :: a₁ :: (as ++ bs)) → Ascending r (a :: a₁ :: as)
Tactic:
intro has
State after:
α : Type u
r : α → α → Prop
bs : List α
a a₁ : α
as : List α
h_ind : Ascending r (a₁ :: (as ++ bs)) → Ascending r (a₁ :: as)
has : Ascending r (a :: a₁ :: (as ++ bs))
⊢ Ascending r (a :: a₁ :: as)

State before:
α : Type u
r : α → α → Prop
bs : List α
a a₁ : α
as : List α
h_ind : Ascending r (a₁ :: (as ++ bs)) → Ascending r (a₁ :: as)
has : Ascending r (a :: a₁ :: (as ++ bs))
⊢ Ascending r (a :: a₁ :: as)
Tactic:
cases has with | cons ha htail =>
exact Ascending.cons ha (h_ind htail)
State after:
no goals

State before:
case cons
α : Type u
r : α → α → Prop
bs : List α
a a₁ : α
as : List α
h_ind : Ascending r (a₁ :: (as ++ bs)) → Ascending r (a₁ :: as)
ha : r a a₁
htail : Ascending r (a₁ :: (as ++ bs))
⊢ Ascending r (a :: a₁ :: as)
Tactic:
exact Ascending.cons ha (h_ind htail)
State after:
no goals