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

State before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
as bs : List α
⊢ Ascending r (as ++ bs) → List.forAllRel r as bs
Tactic:
induction as <;> simp
State after:
case cons
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
head✝ : α
tail✝ : List α
tail_ih✝ : Ascending r (tail✝ ++ bs) → List.forAllRel r tail✝ bs
⊢ Ascending r (head✝ :: (tail✝ ++ bs)) → forAll (r head✝) bs ∧ List.forAllRel r tail✝ bs

State before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : Ascending r (as ++ bs) → List.forAllRel r as bs
⊢ Ascending r (a :: (as ++ bs)) → forAll (r a) bs ∧ List.forAllRel r as bs
Tactic:
case cons a as h_ind =>
  intro hass
  have := hass.forAll_of_tail; simp at this
  exact And.intro this.right (h_ind hass.tail)
State after:
no goals

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

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

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

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