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

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

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

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

State before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
⊢ List.forAllRel r (a :: as) bs → Ascending r (a :: as) → Ascending r bs → Ascending r (a :: as ++ bs)
Tactic:
case cons a as h_ind =>
  dsimp [forAllRel_cons_left]
  rw [List.forAllRel_cons_left]
  intro h hass hbs
  have htail := h_ind h.right hass.tail hbs
  have hhead : bs.forAll (r a) := h.left
  apply cons_of_forAll _ htail
  rw [forAll_append]
  exact And.intro hass.forAll_of_tail hhead
State after:
no goals

State before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
⊢ List.forAllRel r [] bs → Ascending r [] → Ascending r bs → Ascending r ([] ++ bs)
Tactic:
dsimp
State after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
⊢ True → Ascending r [] → Ascending r bs → Ascending r bs

State before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
⊢ True → Ascending r [] → Ascending r bs → Ascending r bs
Tactic:
exact λ _ _ => id
State after:
no goals

State before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
⊢ List.forAllRel r (a :: as) bs → Ascending r (a :: as) → Ascending r bs → Ascending r (a :: as ++ bs)
Tactic:
dsimp [forAllRel_cons_left]
State after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
⊢ List.forAllRel r (a :: as) bs → Ascending r (a :: as) → Ascending r bs → Ascending r (a :: (as ++ bs))

State before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
⊢ List.forAllRel r (a :: as) bs → Ascending r (a :: as) → Ascending r bs → Ascending r (a :: (as ++ bs))
Tactic:
rw [List.forAllRel_cons_left]
State after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
⊢ forAll (r a) bs ∧ List.forAllRel r as bs → Ascending r (a :: as) → Ascending r bs → Ascending r (a :: (as ++ bs))

State before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
⊢ forAll (r a) bs ∧ List.forAllRel r as bs → Ascending r (a :: as) → Ascending r bs → Ascending r (a :: (as ++ bs))
Tactic:
intro h hass hbs
State after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
⊢ Ascending r (a :: (as ++ bs))

State before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
⊢ Ascending r (a :: (as ++ bs))
Tactic:
have htail := h_ind h.right hass.tail hbs
State after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
htail : Ascending r (as ++ bs)
⊢ Ascending r (a :: (as ++ bs))

State before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
htail : Ascending r (as ++ bs)
⊢ Ascending r (a :: (as ++ bs))
Tactic:
have hhead : bs.forAll (r a) := h.left
State after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
htail : Ascending r (as ++ bs)
hhead : forAll (r a) bs
⊢ Ascending r (a :: (as ++ bs))

State before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
htail : Ascending r (as ++ bs)
hhead : forAll (r a) bs
⊢ Ascending r (a :: (as ++ bs))
Tactic:
apply cons_of_forAll _ htail
State after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
htail : Ascending r (as ++ bs)
hhead : forAll (r a) bs
⊢ forAll (r a) (as ++ bs)

State before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
htail : Ascending r (as ++ bs)
hhead : forAll (r a) bs
⊢ forAll (r a) (as ++ bs)
Tactic:
rw [forAll_append]
State after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
htail : Ascending r (as ++ bs)
hhead : forAll (r a) bs
⊢ forAll (r a) as ∧ forAll (r a) bs

State before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
htail : Ascending r (as ++ bs)
hhead : forAll (r a) bs
⊢ forAll (r a) as ∧ forAll (r a) bs
Tactic:
exact And.intro hass.forAll_of_tail hhead
State after:
no goals