[GOAL]
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ dedup l
⊢ ¬∀ (b : α), b ∈ pwFilter (fun x x_1 => x ≠ x_1) l → a ≠ b
[PROOFSTEP]
simpa only [forall_mem_ne, not_not] using h
[GOAL]
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ dedup l
⊢ ∀ (b : α), b ∈ pwFilter (fun x x_1 => x ≠ x_1) l → a ≠ b
[PROOFSTEP]
simpa only [forall_mem_ne] using h
[GOAL]
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
⊢ a ∈ dedup l ↔ a ∈ l
[PROOFSTEP]
have := not_congr (@forall_mem_pwFilter α (· ≠ ·) _ ?_ a l)
[GOAL]
case refine_2
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
this : (¬∀ (b : α), b ∈ pwFilter (fun x x_1 => x ≠ x_1) l → a ≠ b) ↔ ¬∀ (b : α), b ∈ l → a ≠ b
⊢ a ∈ dedup l ↔ a ∈ l
case refine_1
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
⊢ ∀ {x y z : α}, (fun x x_1 => x ≠ x_1) x z → (fun x x_1 => x ≠ x_1) x y ∨ (fun x x_1 => x ≠ x_1) y z
[PROOFSTEP]
simpa only [dedup, forall_mem_ne, not_not] using this
[GOAL]
case refine_1
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
⊢ ∀ {x y z : α}, (fun x x_1 => x ≠ x_1) x z → (fun x x_1 => x ≠ x_1) x y ∨ (fun x x_1 => x ≠ x_1) y z
[PROOFSTEP]
intros x y z xz
[GOAL]
case refine_1
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
x y z : α
xz : x ≠ z
⊢ (fun x x_1 => x ≠ x_1) x y ∨ (fun x x_1 => x ≠ x_1) y z
[PROOFSTEP]
exact not_and_or.1 <| mt (fun h ↦ h.1.trans h.2) xz
[GOAL]
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
⊢ headI (dedup (a :: l)) = if headI (a :: l) ∈ tail (a :: l) then headI (dedup (tail (a :: l))) else headI (a :: l)
[PROOFSTEP]
by_cases ha : a ∈ l
[GOAL]
case pos
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : a ∈ l
⊢ headI (dedup (a :: l)) = if headI (a :: l) ∈ tail (a :: l) then headI (dedup (tail (a :: l))) else headI (a :: l)
[PROOFSTEP]
simp [ha, List.dedup_cons_of_mem]
[GOAL]
case neg
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : ¬a ∈ l
⊢ headI (dedup (a :: l)) = if headI (a :: l) ∈ tail (a :: l) then headI (dedup (tail (a :: l))) else headI (a :: l)
[PROOFSTEP]
simp [ha, List.dedup_cons_of_mem]
[GOAL]
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
⊢ tail (dedup (a :: l)) = if headI (a :: l) ∈ tail (a :: l) then tail (dedup (tail (a :: l))) else dedup (tail (a :: l))
[PROOFSTEP]
by_cases ha : a ∈ l
[GOAL]
case pos
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : a ∈ l
⊢ tail (dedup (a :: l)) = if headI (a :: l) ∈ tail (a :: l) then tail (dedup (tail (a :: l))) else dedup (tail (a :: l))
[PROOFSTEP]
simp [ha, List.dedup_cons_of_mem]
[GOAL]
case neg
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : ¬a ∈ l
⊢ tail (dedup (a :: l)) = if headI (a :: l) ∈ tail (a :: l) then tail (dedup (tail (a :: l))) else dedup (tail (a :: l))
[PROOFSTEP]
simp [ha, List.dedup_cons_of_mem]
[GOAL]
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
⊢ dedup l = a :: l' ↔ a ∈ l ∧ ¬a ∈ l' ∧ tail (dedup l) = l'
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : dedup l = a :: l'
⊢ a ∈ l ∧ ¬a ∈ l' ∧ tail (dedup l) = l'
[PROOFSTEP]
refine' ⟨mem_dedup.1 (h.symm ▸ mem_cons_self _ _), fun ha => _, by rw [h, tail_cons]⟩
[GOAL]
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : dedup l = a :: l'
⊢ tail (dedup l) = l'
[PROOFSTEP]
rw [h, tail_cons]
[GOAL]
case refine'_1
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : dedup l = a :: l'
ha : a ∈ l'
⊢ False
[PROOFSTEP]
have : count a l.dedup ≤ 1 := nodup_iff_count_le_one.1 (nodup_dedup l) a
[GOAL]
case refine'_1
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : dedup l = a :: l'
ha : a ∈ l'
this : count a (dedup l) ≤ 1
⊢ False
[PROOFSTEP]
rw [h, count_cons_self, add_le_iff_nonpos_left] at this 
[GOAL]
case refine'_1
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : dedup l = a :: l'
ha : a ∈ l'
this : count a l' ≤ 0
⊢ False
[PROOFSTEP]
exact not_le_of_lt (count_pos.2 ha) this
[GOAL]
case refine'_2
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ tail (dedup l) = l'
⊢ dedup l = a :: l'
[PROOFSTEP]
have := @List.cons_head!_tail α ⟨a⟩ _ (ne_nil_of_mem (mem_dedup.2 h.1))
[GOAL]
case refine'_2
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ tail (dedup l) = l'
this : head! (dedup l) :: tail (dedup l) = dedup l
⊢ dedup l = a :: l'
[PROOFSTEP]
have hal : a ∈ l.dedup := mem_dedup.2 h.1
[GOAL]
case refine'_2
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ tail (dedup l) = l'
this : head! (dedup l) :: tail (dedup l) = dedup l
hal : a ∈ dedup l
⊢ dedup l = a :: l'
[PROOFSTEP]
rw [← this, mem_cons, or_iff_not_imp_right] at hal 
[GOAL]
case refine'_2
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ tail (dedup l) = l'
this : head! (dedup l) :: tail (dedup l) = dedup l
hal : ¬a ∈ tail (dedup l) → a = head! (dedup l)
⊢ dedup l = a :: l'
[PROOFSTEP]
exact this ▸ h.2.2.symm ▸ cons_eq_cons.2 ⟨(hal (h.2.2.symm ▸ h.2.1)).symm, rfl⟩
[GOAL]
α : Type u
inst✝ : DecidableEq α
l : List α
⊢ dedup l = [] ↔ l = []
[PROOFSTEP]
induction' l with a l hl
[GOAL]
case nil
α : Type u
inst✝ : DecidableEq α
⊢ dedup [] = [] ↔ [] = []
[PROOFSTEP]
exact Iff.rfl
[GOAL]
case cons
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
hl : dedup l = [] ↔ l = []
⊢ dedup (a :: l) = [] ↔ a :: l = []
[PROOFSTEP]
by_cases h : a ∈ l
[GOAL]
case pos
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
hl : dedup l = [] ↔ l = []
h : a ∈ l
⊢ dedup (a :: l) = [] ↔ a :: l = []
[PROOFSTEP]
simp only [List.dedup_cons_of_mem h, hl, List.ne_nil_of_mem h]
[GOAL]
case neg
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
hl : dedup l = [] ↔ l = []
h : ¬a ∈ l
⊢ dedup (a :: l) = [] ↔ a :: l = []
[PROOFSTEP]
simp only [List.dedup_cons_of_not_mem h, List.cons_ne_nil]
[GOAL]
α : Type u
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ dedup (l₁ ++ l₂) = l₁ ∪ dedup l₂
[PROOFSTEP]
induction' l₁ with a l₁ IH
[GOAL]
case nil
α : Type u
inst✝ : DecidableEq α
l₂ : List α
⊢ dedup ([] ++ l₂) = [] ∪ dedup l₂
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = l₁ ∪ dedup l₂
⊢ dedup (a :: l₁ ++ l₂) = a :: l₁ ∪ dedup l₂
[PROOFSTEP]
simp only [cons_union] at *
[GOAL]
case cons
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = l₁ ∪ dedup l₂
⊢ dedup (a :: l₁ ++ l₂) = List.insert a (l₁ ∪ dedup l₂)
[PROOFSTEP]
rw [← IH, cons_append]
[GOAL]
case cons
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = l₁ ∪ dedup l₂
⊢ dedup (a :: (l₁ ++ l₂)) = List.insert a (dedup (l₁ ++ l₂))
[PROOFSTEP]
by_cases h : a ∈ dedup (l₁ ++ l₂)
[GOAL]
case pos
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = l₁ ∪ dedup l₂
h : a ∈ dedup (l₁ ++ l₂)
⊢ dedup (a :: (l₁ ++ l₂)) = List.insert a (dedup (l₁ ++ l₂))
[PROOFSTEP]
rw [dedup_cons_of_mem' h, insert_of_mem h]
[GOAL]
case neg
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = l₁ ∪ dedup l₂
h : ¬a ∈ dedup (l₁ ++ l₂)
⊢ dedup (a :: (l₁ ++ l₂)) = List.insert a (dedup (l₁ ++ l₂))
[PROOFSTEP]
rw [dedup_cons_of_not_mem' h, insert_of_not_mem h]
[GOAL]
α : Type u
inst✝ : DecidableEq α
x : α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ dedup (replicate (n + 2) x) = [x]
[PROOFSTEP]
rw [replicate_succ, dedup_cons_of_mem (mem_replicate.2 ⟨n.succ_ne_zero, rfl⟩), replicate_dedup n.succ_ne_zero]
[GOAL]
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
⊢ count a (dedup l) = if a ∈ l then 1 else 0
[PROOFSTEP]
simp_rw [count_eq_of_nodup <| nodup_dedup l, mem_dedup]
[GOAL]
α : Type u
inst✝ : DecidableEq α
p : α → Bool
l : List α
⊢ sum (map (fun x => count x l) (filter p (dedup l))) = countp p l
[PROOFSTEP]
induction' l with a as h
[GOAL]
case nil
α : Type u
inst✝ : DecidableEq α
p : α → Bool
⊢ sum (map (fun x => count x []) (filter p (dedup []))) = countp p []
[PROOFSTEP]
simp
[GOAL]
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)
[PROOFSTEP]
simp_rw [List.countp_cons, List.count_cons', List.sum_map_add]
[GOAL]
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
[PROOFSTEP]
congr 1
[GOAL]
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
[PROOFSTEP]
refine' _root_.trans _ h
[GOAL]
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)))
[PROOFSTEP]
by_cases ha : a ∈ as
[GOAL]
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)))
[PROOFSTEP]
simp [dedup_cons_of_mem ha]
[GOAL]
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)))
[PROOFSTEP]
simp only [dedup_cons_of_not_mem ha, List.filter]
[GOAL]
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)))
[PROOFSTEP]
match p a with
| true => simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
| false => simp only
[GOAL]
α : 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)))
[PROOFSTEP]
simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
[GOAL]
α : 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)))
[PROOFSTEP]
simp only
[GOAL]
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
[PROOFSTEP]
by_cases hp : p a
[GOAL]
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
[PROOFSTEP]
refine' _root_.trans (sum_map_eq_nsmul_single a _ fun _ h _ => by simp [h]) _
[GOAL]
α : 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
[PROOFSTEP]
simp [h]
[GOAL]
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
[PROOFSTEP]
simp [hp, count_dedup]
[GOAL]
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
[PROOFSTEP]
refine' _root_.trans (List.sum_eq_zero fun n hn => _) (by simp [hp])
[GOAL]
α : 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
[PROOFSTEP]
simp [hp]
[GOAL]
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
[PROOFSTEP]
obtain ⟨a', ha'⟩ := List.mem_map.1 hn
[GOAL]
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
[PROOFSTEP]
split_ifs at ha'  with ha
[GOAL]
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
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
[PROOFSTEP]
simp only [ha, mem_filter, mem_dedup, find?, mem_cons, true_or, hp, and_false, false_and] at ha' 
[GOAL]
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)))
a' : α
ha : ¬a' = a
ha' : a' ∈ filter p (dedup (a :: as)) ∧ 0 = n
⊢ n = 0
[PROOFSTEP]
exact ha'.2.symm
[GOAL]
α : Type u
inst✝ : DecidableEq α
l : List α
⊢ sum (map (fun x => count x l) (dedup l)) = length l
[PROOFSTEP]
simpa using sum_map_count_dedup_filter_eq_countp (fun _ => True) l
