Theorem: List.all_append (LeanSAT/Reflect/CNF/ForStd.lean)

State before:
α : Type u_1
f : α → Bool
x y : List α
⊢ (x ++ y).all f = (x.all f && y.all f)
Tactic:
induction x with
| nil => rfl
| cons h t ih => simp_all [Bool.and_assoc]
State after:
no goals

State before:
case nil
α : Type u_1
f : α → Bool
y : List α
⊢ ([] ++ y).all f = ([].all f && y.all f)
Tactic:
rfl
State after:
no goals

State before:
case cons
α : Type u_1
f : α → Bool
y : List α
h : α
t : List α
ih : (t ++ y).all f = (t.all f && y.all f)
⊢ (h :: t ++ y).all f = ((h :: t).all f && y.all f)
Tactic:
simp_all [Bool.and_assoc]
State after:
no goals