Theorem: List.count_append (One.lean)

State before:
α : Type u_1
inst✝ : BEq α
a : α
l₁ l₂ : List α
⊢ count a (l₁ ++ l₂) = count a l₁ + count a l₂
Tactic:
unfold count
State after:
α : Type u_1
inst✝ : BEq α
a : α
l₁ l₂ : List α
⊢ countp (fun x => x == a) (l₁ ++ l₂) = countp (fun x => x == a) l₁ + countp (fun x => x == a) l₂

State before:
α : Type u_1
inst✝ : BEq α
a : α
l₁ l₂ : List α
⊢ countp (fun x => x == a) (l₁ ++ l₂) = countp (fun x => x == a) l₁ + countp (fun x => x == a) l₂
Tactic:
apply List.countp_append
State after:
no goals