-- Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
theorem sum_map_count_dedup_filter_eq_countP (p : α → Bool) (l : List α) :
    ((l.dedup.filter p).map fun x => l.count x).sum = l.countP p

Proof state:
case cons.e_a
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x => count x as) (filter p as.dedup)).sum = countP p as
⊢ (map (fun i => count i as) (filter p (a :: as).dedup)).sum = (map (fun x => count x as) (filter p as.dedup)).sum

Tactic:
by_cases ha : a ∈ as

Result:
case pos
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x => count x as) (filter p as.dedup)).sum = countP p as
ha : a ∈ as
⊢ (map (fun i => count i as) (filter p (a :: as).dedup)).sum = (map (fun x => count x as) (filter p as.dedup)).sum

case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x => count x as) (filter p as.dedup)).sum = countP p as
ha : a ∉ as
⊢ (map (fun i => count i as) (filter p (a :: as).dedup)).sum = (map (fun x => count x as) (filter p as.dedup)).sum

Proof state:
case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x => count x as) (filter p as.dedup)).sum = countP p as
ha : a ∉ as
⊢ (map (fun i => count i as) (filter p (a :: as).dedup)).sum = (map (fun x => count x as) (filter p as.dedup)).sum

Tactic:
simp only [dedup_cons_of_not_mem ha, List.filter]

Result:
case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x => count x as) (filter p as.dedup)).sum = countP p as
ha : a ∉ as
⊢ (map (fun i => count i as)
        (match p a with
        | true => a :: filter p as.dedup
        | false => filter p as.dedup)).sum =
    (map (fun i => count i as) (filter p as.dedup)).sum

Proof state:
case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x => count x as) (filter p as.dedup)).sum = countP p as
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i => if a = i then 1 else 0) (filter p (a :: as).dedup)
a' : α
ha : ¬a = a'
ha' : a' ∈ filter p (a :: as).dedup ∧ 0 = n
⊢ n = 0

Tactic:
exact ha'.2.symm

Result:
no goals

Proof state:
case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x => count x as) (filter p as.dedup)).sum = countP p as
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i => if a = i then 1 else 0) (filter p (a :: as).dedup)
⊢ n = 0

Tactic:
obtain ⟨a', ha'⟩ := List.mem_map.1 hn

Result:
case neg.intro
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x => count x as) (filter p as.dedup)).sum = countP p as
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i => if a = i then 1 else 0) (filter p (a :: as).dedup)
a' : α
ha' : a' ∈ filter p (a :: as).dedup ∧ (if a = a' then 1 else 0) = n
⊢ n = 0

Proof state:
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x => count x as) (filter p as.dedup)).sum = countP p as
ha : a ∉ as
⊢ (map (fun i => count i as)
        (match false with
        | true => a :: filter p as.dedup
        | false => filter p as.dedup)).sum =
    (map (fun i => count i as) (filter p as.dedup)).sum

Tactic:
simp only

Result:
no goals

Proof state:
case neg.intro
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x => count x as) (filter p as.dedup)).sum = countP p as
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i => if a = i then 1 else 0) (filter p (a :: as).dedup)
a' : α
ha' : a' ∈ filter p (a :: as).dedup ∧ (if a = a' then 1 else 0) = n
⊢ n = 0

Tactic:
split_ifs at ha' with ha

Result:
case pos
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x => count x as) (filter p as.dedup)).sum = countP p as
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i => if a = i then 1 else 0) (filter p (a :: as).dedup)
a' : α
ha : a = a'
ha' : a' ∈ filter p (a :: as).dedup ∧ 1 = n
⊢ n = 0

case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x => count x as) (filter p as.dedup)).sum = countP p as
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i => if a = i then 1 else 0) (filter p (a :: as).dedup)
a' : α
ha : ¬a = a'
ha' : a' ∈ filter p (a :: as).dedup ∧ 0 = n
⊢ n = 0