Theorem: List.count_cons (One.lean)

State before:
α : Type u_1
a : α
inst✝ : BEq α
head : α
tail : List α
⊢ count a (head :: tail) = (if (head == a) = true then 1 else 0) + count a tail
Tactic:
unfold count
State after:
α : Type u_1
a : α
inst✝ : BEq α
head : α
tail : List α
⊢ countp (fun x => x == a) (head :: tail) = (if (head == a) = true then 1 else 0) + countp (fun x => x == a) tail

State before:
α : Type u_1
a : α
inst✝ : BEq α
head : α
tail : List α
⊢ countp (fun x => x == a) (head :: tail) = (if (head == a) = true then 1 else 0) + countp (fun x => x == a) tail
Tactic:
apply countp_cons
State after:
no goals