Theorem: List.countp_append (One.lean)

State before:
α✝ : Type u_1
p : α✝ → Bool
l₁ l₂ : List α✝
⊢ countp p (l₁ ++ l₂) = countp p l₁ + countp p l₂
Tactic:
induction l₁ with
| nil => simp only [nil_append, countp_nil, zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_add]
| cons head tail ih => simp only [cons_append, countp_cons, ih, zero_le, ge_iff_le, nonpos_iff_eq_zero, add_assoc]
State after:
no goals

State before:
case nil
α✝ : Type u_1
p : α✝ → Bool
l₂ : List α✝
⊢ countp p ([] ++ l₂) = countp p [] + countp p l₂
Tactic:
simp only [nil_append, countp_nil, zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_add]
State after:
no goals

State before:
case cons
α✝ : Type u_1
p : α✝ → Bool
l₂ : List α✝
head : α✝
tail : List α✝
ih : countp p (tail ++ l₂) = countp p tail + countp p l₂
⊢ countp p (head :: tail ++ l₂) = countp p (head :: tail) + countp p l₂
Tactic:
simp only [cons_append, countp_cons, ih, zero_le, ge_iff_le, nonpos_iff_eq_zero, add_assoc]
State after:
no goals