case nil
α : Type u
inst✝ : DecidableEq α
p : α → Bool
⊢ sum (map (fun x => count x []) (filter p (dedup []))) = countp p []

case cons
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
⊢ sum (map (fun x => count x (a :: as)) (filter p (dedup (a :: as)))) = countp p (a :: as)
α : Type u
inst✝ : DecidableEq α
p : α → Bool
l : List α
⊢ sum (map (fun x => count x l) (filter p (dedup l))) = countp p l
induction' l with a as h
no goals
case nil
α : Type u
inst✝ : DecidableEq α
p : α → Bool
⊢ sum (map (fun x => count x []) (filter p (dedup []))) = countp p []
simp
case cons
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
⊢ sum (map (fun i => count i as) (filter p (dedup (a :: as)))) +
      sum (map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))) =
    countp p as + if p a = true then 1 else 0
case cons
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
⊢ sum (map (fun x => count x (a :: as)) (filter p (dedup (a :: as)))) = countp p (a :: as)
simp_rw [List.countp_cons, List.count_cons', List.sum_map_add]
case cons.e_a
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
⊢ sum (map (fun i => count i as) (filter p (dedup (a :: as)))) = countp p as

case cons.e_a
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
⊢ sum (map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))) = if p a = true then 1 else 0
case cons
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
⊢ sum (map (fun i => count i as) (filter p (dedup (a :: as)))) +
      sum (map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))) =
    countp p as + if p a = true then 1 else 0
congr 1
case cons.e_a
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
⊢ sum (map (fun i => count i as) (filter p (dedup (a :: as)))) = sum (map (fun x => count x as) (filter p (dedup as)))
case cons.e_a
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
⊢ sum (map (fun i => count i as) (filter p (dedup (a :: as)))) = countp p as
refine' _root_.trans _ h
case pos
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
ha : a ∈ as
⊢ sum (map (fun i => count i as) (filter p (dedup (a :: as)))) = sum (map (fun x => count x as) (filter p (dedup as)))

case neg
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
ha : ¬a ∈ as
⊢ sum (map (fun i => count i as) (filter p (dedup (a :: as)))) = sum (map (fun x => count x as) (filter p (dedup as)))
case cons.e_a
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
⊢ sum (map (fun i => count i as) (filter p (dedup (a :: as)))) = sum (map (fun x => count x as) (filter p (dedup as)))
by_cases ha : a ∈ as
no goals
case pos
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
ha : a ∈ as
⊢ sum (map (fun i => count i as) (filter p (dedup (a :: as)))) = sum (map (fun x => count x as) (filter p (dedup as)))
simp [dedup_cons_of_mem ha]
case neg
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
ha : ¬a ∈ as
⊢ sum
      (map (fun i => count i as)
        (match p a with
        | true => a :: filter p (dedup as)
        | false => filter p (dedup as))) =
    sum (map (fun i => count i as) (filter p (dedup as)))
case neg
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
ha : ¬a ∈ as
⊢ sum (map (fun i => count i as) (filter p (dedup (a :: as)))) = sum (map (fun x => count x as) (filter p (dedup as)))
simp only [dedup_cons_of_not_mem ha, List.filter]
no goals
case neg
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
ha : ¬a ∈ as
⊢ sum
      (map (fun i => count i as)
        (match p a with
        | true => a :: filter p (dedup as)
        | false => filter p (dedup as))) =
    sum (map (fun i => count i as) (filter p (dedup as)))
match p a with
| true => simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
| false => simp only
no goals
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
ha : ¬a ∈ as
⊢ sum
      (map (fun i => count i as)
        (match true with
        | true => a :: filter p (dedup as)
        | false => filter p (dedup as))) =
    sum (map (fun i => count i as) (filter p (dedup as)))
simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
no goals
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
ha : ¬a ∈ as
⊢ sum
      (map (fun i => count i as)
        (match false with
        | true => a :: filter p (dedup as)
        | false => filter p (dedup as))) =
    sum (map (fun i => count i as) (filter p (dedup as)))
simp only
case pos
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : p a = true
⊢ sum (map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))) = if p a = true then 1 else 0

case neg
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : ¬p a = true
⊢ sum (map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))) = if p a = true then 1 else 0
case cons.e_a
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
⊢ sum (map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))) = if p a = true then 1 else 0
by_cases hp : p a
case pos
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : p a = true
⊢ (count a (filter p (dedup (a :: as))) • if a = a then 1 else 0) = if p a = true then 1 else 0
case pos
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : p a = true
⊢ sum (map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))) = if p a = true then 1 else 0
refine' _root_.trans (sum_map_eq_nsmul_single a _ fun _ h _ => by simp [h]) _
no goals
case pos
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : p a = true
⊢ (count a (filter p (dedup (a :: as))) • if a = a then 1 else 0) = if p a = true then 1 else 0
simp [hp, count_dedup]
no goals
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h✝ : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : p a = true
x✝¹ : α
h : x✝¹ ≠ a
x✝ : x✝¹ ∈ filter p (dedup (a :: as))
⊢ (if x✝¹ = a then 1 else 0) = 0
simp [h]
case neg
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))
⊢ n = 0
case neg
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : ¬p a = true
⊢ sum (map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))) = if p a = true then 1 else 0
refine' _root_.trans (List.sum_eq_zero fun n hn => _) (by simp [hp])
case neg.intro
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))
a' : α
ha' : a' ∈ filter p (dedup (a :: as)) ∧ (if a' = a then 1 else 0) = n
⊢ n = 0
case neg
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))
⊢ n = 0
obtain ⟨a', ha'⟩ := List.mem_map.1 hn
case neg.intro.inl
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))
a' : α
ha : a' = a
ha' : a' ∈ filter p (dedup (a :: as)) ∧ 1 = n
⊢ n = 0

case neg.intro.inr
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))
a' : α
ha : ¬a' = a
ha' : a' ∈ filter p (dedup (a :: as)) ∧ 0 = n
⊢ n = 0
case neg.intro
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))
a' : α
ha' : a' ∈ filter p (dedup (a :: as)) ∧ (if a' = a then 1 else 0) = n
⊢ n = 0
split_ifs at ha' with ha
no goals
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : ¬p a = true
⊢ 0 = if p a = true then 1 else 0
simp [hp]
no goals
case neg.intro.inl
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))
a' : α
ha : a' = a
ha' : a' ∈ filter p (dedup (a :: as)) ∧ 1 = n
⊢ n = 0
simp only [ha, mem_filter, mem_dedup, find?, mem_cons, true_or, hp,
  and_false, false_and] at ha'
no goals
case neg.intro.inr
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))
a' : α
ha : ¬a' = a
ha' : a' ∈ filter p (dedup (a :: as)) ∧ 0 = n
⊢ n = 0
exact ha'.2.symm