-- 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 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

Tactic:
match p a with
| true => simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
| false => simp only

Result:
no goals

Proof state:
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

Tactic:
simp only [ha.symm, mem_filter, mem_dedup, find?, mem_cons, true_or, hp,
  and_false, false_and, reduceCtorEq] at ha'

Result:
no goals

Proof state:
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

Tactic:
simp [dedup_cons_of_mem ha]

Result:
no goals

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 => if (a == i) = true then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

Tactic:
simp only [beq_iff_eq]

Result:
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 => if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 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 true 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 [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]

Result:
no goals

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
hp : ¬p a = true
⊢ 0 = if p a = true then 1 else 0

Tactic:
simp [hp]

Result:
no goals

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 = countP p as

Tactic:
refine _root_.trans ?_ h

Result:
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

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
hp : p a = true
x✝¹ : α
h : x✝¹ ≠ a
x✝ : x✝¹ ∈ filter p (a :: as).dedup
⊢ (if a = x✝¹ then 1 else 0) = 0

Tactic:
simp [h.symm]

Result:
no goals

Proof state:
case cons
α : 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 i => if (a == i) = true then 1 else 0) (filter p (a :: as).dedup)).sum =
    countP p as + if p a = true then 1 else 0

Tactic:
congr 1

Result:
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 = countP p as

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 => if (a == i) = true then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

Proof state:
case nil
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
⊢ (map (fun x => count x []) (filter p [].dedup)).sum = countP p []

Tactic:
simp

Result:
no goals

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 => if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

Tactic:
by_cases hp : p a

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
⊢ (map (fun i => if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 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
⊢ (map (fun i => if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

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
⊢ (map (fun i => if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

Tactic:
refine _root_.trans (List.sum_eq_zero fun n hn => ?_) (by simp [hp])

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
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i => if a = i then 1 else 0) (filter p (a :: as).dedup)
⊢ n = 0

Proof state:
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
⊢ (map (fun i => if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

Tactic:
refine _root_.trans (sum_map_eq_nsmul_single a _ fun _ h _ => by simp [h.symm]) ?_

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
⊢ (count a (filter p (a :: as).dedup) • if a = a then 1 else 0) = if p a = true then 1 else 0

Proof state:
case cons
α : 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 x => count x (a :: as)) (filter p (a :: as).dedup)).sum = countP p (a :: as)

Tactic:
simp_rw [List.countP_cons, List.count_cons, List.sum_map_add]

Result:
case cons
α : 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 i => if (a == i) = true then 1 else 0) (filter p (a :: as).dedup)).sum =
    countP p as + if p a = true then 1 else 0

Proof state:
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
⊢ (count a (filter p (a :: as).dedup) • if a = a then 1 else 0) = if p a = true then 1 else 0

Tactic:
simp [hp, count_dedup]

Result:
no goals