feat(data/list/count): partially sync with multiset (#18125)

urkud · urkud · commit 7c523cb78f41 · 2023-01-11T18:25:14.000Z
* rename `list.count_repeat` to `list.count_repeat_self`;
* prove `list.count_repeat` with `if .. then .. else` in the RHS.
diff --git a/archive/100-theorems-list/30_ballot_problem.lean b/archive/100-theorems-list/30_ballot_problem.lean
@@ -82,7 +82,7 @@ begin
     { rwa ← list.count_eq_length.2 this },
     { exact λ x hx, (this x hx).symm } },
   { rintro rfl,
-    simp only [mem_set_of_eq, list.count_repeat, eq_self_iff_true, true_and],
+    simp only [mem_set_of_eq, list.count_repeat_self, eq_self_iff_true, true_and],
     refine ⟨list.count_eq_zero_of_not_mem _, λ x, _⟩; rw list.mem_repeat,
     { norm_num },
     { rintro ⟨-, rfl⟩,
@@ -105,7 +105,7 @@ begin
     { rwa ← list.count_eq_length.2 this },
     { exact λ x hx, (this x hx).symm } },
   { rintro rfl,
-    simp only [mem_set_of_eq, list.count_repeat, eq_self_iff_true, true_and],
+    simp only [mem_set_of_eq, list.count_repeat_self, eq_self_iff_true, true_and],
     refine ⟨list.count_eq_zero_of_not_mem _, λ x, _⟩; rw list.mem_repeat,
     { norm_num },
     { rintro ⟨-, rfl⟩,
diff --git a/src/data/list/count.lean b/src/data/list/count.lean
@@ -164,17 +164,23 @@ lemma not_mem_of_count_eq_zero {a : α} {l : list α} (h : count a l = 0) : a 
 @[simp] lemma count_eq_length {a : α} {l} : count a l = l.length ↔ ∀ b ∈ l, a = b :=
 countp_eq_length _
 
-@[simp] lemma count_repeat (a : α) (n : ℕ) : count a (repeat a n) = n :=
+@[simp] lemma count_repeat_self (a : α) (n : ℕ) : count a (repeat a n) = n :=
 by rw [count, countp_eq_length_filter, filter_eq_self.2, length_repeat];
    exact λ b m, (eq_of_mem_repeat m).symm
 
+lemma count_repeat (a b : α) (n : ℕ) : count a (repeat b n) = if a = b then n else 0 :=
+begin
+  split_ifs with h,
+  exacts [h ▸ count_repeat_self _ _, count_eq_zero_of_not_mem (mt eq_of_mem_repeat h)]
+end
+
 lemma le_count_iff_repeat_sublist {a : α} {l : list α} {n : ℕ} :
   n ≤ count a l ↔ repeat a n <+ l :=
 ⟨λ h, ((repeat_sublist_repeat a).2 h).trans $
   have filter (eq a) l = repeat a (count a l), from eq_repeat.2
     ⟨by simp only [count, countp_eq_length_filter], λ b m, (of_mem_filter m).symm⟩,
   by rw ← this; apply filter_sublist,
- λ h, by simpa only [count_repeat] using h.count_le a⟩
+ λ h, by simpa only [count_repeat_self] using h.count_le a⟩
 
 lemma repeat_count_eq_of_count_eq_length  {a : α} {l : list α} (h : count a l = length l)  :
   repeat a (count a l) = l :=
diff --git a/src/data/multiset/basic.lean b/src/data/multiset/basic.lean
@@ -1790,12 +1790,7 @@ by simp [repeat]
 
 theorem count_repeat (a b : α) (n : ℕ)  :
   count a (repeat b n) = if (a = b) then n else 0 :=
-begin
-  split_ifs with h₁,
-  { rw [h₁, count_repeat_self] },
-  { rw [count_eq_zero],
-    apply mt eq_of_mem_repeat h₁ },
-end
+count_repeat a b n
 
 @[simp] theorem count_erase_self (a : α) (s : multiset α) :
   count a (erase s a) = pred (count a s) :=
