Theorem: List.forAll_append (Algdata/Data/List/Prop.lean)

State before:
α : Type u_1
p : α → Prop
as bs : List α
⊢ forAll p (as ++ bs) = (forAll p as ∧ forAll p bs)
Tactic:
induction as
State after:
case nil
α : Type u_1
p : α → Prop
bs : List α
⊢ forAll p ([] ++ bs) = (forAll p [] ∧ forAll p bs)

case cons
α : Type u_1
p : α → Prop
bs : List α
head✝ : α
tail✝ : List α
tail_ih✝ : forAll p (tail✝ ++ bs) = (forAll p tail✝ ∧ forAll p bs)
⊢ forAll p (head✝ :: tail✝ ++ bs) = (forAll p (head✝ :: tail✝) ∧ forAll p bs)

State before:
α : Type u_1
p : α → Prop
bs : List α
⊢ forAll p ([] ++ bs) = (forAll p [] ∧ forAll p bs)
Tactic:
case nil => dsimp [forAll]; rw [true_and]
State after:
no goals

State before:
α : Type u_1
p : α → Prop
bs : List α
head✝ : α
tail✝ : List α
h_ind : forAll p (tail✝ ++ bs) = (forAll p tail✝ ∧ forAll p bs)
⊢ forAll p (head✝ :: tail✝ ++ bs) = (forAll p (head✝ :: tail✝) ∧ forAll p bs)
Tactic:
case cons _ _ h_ind => dsimp [forAll]; rw [h_ind, and_assoc]
State after:
no goals

State before:
α : Type u_1
p : α → Prop
bs : List α
⊢ forAll p ([] ++ bs) = (forAll p [] ∧ forAll p bs)
Tactic:
dsimp [forAll]
State after:
α : Type u_1
p : α → Prop
bs : List α
⊢ forAll p bs = (True ∧ forAll p bs)

State before:
α : Type u_1
p : α → Prop
bs : List α
⊢ forAll p bs = (True ∧ forAll p bs)
Tactic:
rw [true_and]
State after:
no goals

State before:
α : Type u_1
p : α → Prop
bs : List α
head✝ : α
tail✝ : List α
h_ind : forAll p (tail✝ ++ bs) = (forAll p tail✝ ∧ forAll p bs)
⊢ forAll p (head✝ :: tail✝ ++ bs) = (forAll p (head✝ :: tail✝) ∧ forAll p bs)
Tactic:
dsimp [forAll]
State after:
α : Type u_1
p : α → Prop
bs : List α
head✝ : α
tail✝ : List α
h_ind : forAll p (tail✝ ++ bs) = (forAll p tail✝ ∧ forAll p bs)
⊢ (p head✝ ∧ forAll p (tail✝ ++ bs)) = ((p head✝ ∧ forAll p tail✝) ∧ forAll p bs)

State before:
α : Type u_1
p : α → Prop
bs : List α
head✝ : α
tail✝ : List α
h_ind : forAll p (tail✝ ++ bs) = (forAll p tail✝ ∧ forAll p bs)
⊢ (p head✝ ∧ forAll p (tail✝ ++ bs)) = ((p head✝ ∧ forAll p tail✝) ∧ forAll p bs)
Tactic:
rw [h_ind, and_assoc]
State after:
no goals