Refactor: drop List.repeat (#1579)

Mathlib 3 migrated to `list.replicate` in leanprover-community/mathlib#18127 (merged) and leanprover-community/mathlib#18181 (awaiting review).

Mathlib/Algebra/BigOperators/Multiset/Basic.lean

@@ -116,11 +116,10 @@ theorem prod_nsmul (m : Multiset α) : ∀ n : ℕ, (n • m).prod = m.prod ^ n
   | n + 1 => by rw [add_nsmul, one_nsmul, pow_add, pow_one, prod_add, prod_nsmul m n]
 #align multiset.prod_nsmul Multiset.prod_nsmul
 
-set_option linter.deprecated false in
 @[to_additive (attr := simp)]
-theorem prod_repeat (a : α) (n : ℕ) : («repeat» a n).prod = a ^ n := by
-  simp [«repeat», replicate, List.prod_replicate]
-#align multiset.prod_repeat Multiset.prod_repeat
+theorem prod_replicate (n : ℕ) (a : α) : (replicate n a).prod = a ^ n := by
+  simp [replicate, List.prod_replicate]
+#align multiset.prod_replicate Multiset.prod_replicate
 
 @[to_additive]
 theorem prod_map_eq_pow_single [DecidableEq ι] (i : ι)
@@ -140,7 +139,7 @@ theorem prod_eq_pow_single [DecidableEq α] (a : α) (h : ∀ (a') (_ : a' ≠ a
 
 @[to_additive]
 theorem pow_count [DecidableEq α] (a : α) : a ^ s.count a = (s.filter (Eq a)).prod := by
-  rw [filter_eq, prod_repeat]
+  rw [filter_eq, prod_replicate]
 #align multiset.pow_count Multiset.pow_count
 
 @[to_additive]
@@ -174,7 +173,8 @@ theorem prod_hom_rel [CommMonoid β] (s : Multiset ι) {r : α → β → Prop}
 #align multiset.prod_hom_rel Multiset.prod_hom_rel
 
 @[to_additive]
-theorem prod_map_one : prod (m.map fun _ => (1 : α)) = 1 := by rw [map_const', prod_repeat, one_pow]
+theorem prod_map_one : prod (m.map fun _ => (1 : α)) = 1 := by
+  rw [map_const', prod_replicate, one_pow]
 #align multiset.prod_map_one Multiset.prod_map_one
 
 @[to_additive (attr := simp)]
@@ -395,7 +395,7 @@ theorem prod_le_prod_map (f : α → α) (h : ∀ x, x ∈ s → x ≤ f x) : s.
 @[to_additive card_nsmul_le_sum]
 theorem pow_card_le_prod (h : ∀ x ∈ s, a ≤ x) : a ^ card s ≤ s.prod :=
   by
-  rw [← Multiset.prod_repeat, ← Multiset.map_const]
+  rw [← Multiset.prod_replicate, ← Multiset.map_const]
   exact prod_map_le_prod _ h
 #align multiset.pow_card_le_prod Multiset.pow_card_le_prod
 

Mathlib/Data/List/BigOperators/Basic.lean

@@ -71,17 +71,12 @@ theorem prod_eq_foldr : ∀ {l : List M}, l.prod = foldr (· * ·) 1 l
 #align list.prod_eq_foldr List.prod_eq_foldr
 
 @[to_additive (attr := simp)]
-theorem prod_replicate (a : M) (n : ℕ) : (List.replicate n a).prod = a ^ n := by
+theorem prod_replicate (n : ℕ) (a : M) : (replicate n a).prod = a ^ n := by
   induction' n with n ih
   · rw [pow_zero]
     rfl
-  · rw [List.replicate_succ, List.prod_cons, ih, pow_succ]
-
-set_option linter.deprecated false in
-/-- Deprecated: use `List.prod_replicate` instead. -/
-@[to_additive (attr := deprecated) "Deprecated: use `List.sum_replicate` instead."]
-theorem prod_repeat (a : M) (n : ℕ) : (List.repeat a n).prod = a ^ n := by simp
-#align list.prod_repeat List.prod_repeat
+  · rw [replicate_succ, prod_cons, ih, pow_succ]
+#align list.prod_replicate List.prod_replicate
 
 @[to_additive sum_eq_card_nsmul]
 theorem prod_eq_pow_card (l : List M) (m : M) (h : ∀ x ∈ l, x = m) : l.prod = m ^ l.length := by
@@ -125,23 +120,9 @@ theorem prod_map_mul {α : Type _} [CommMonoid α] {l : List ι} {f g : ι → 
 
 @[simp]
 theorem prod_map_neg {α} [CommMonoid α] [HasDistribNeg α] (l : List α) :
-    (l.map Neg.neg).prod = (-1) ^ l.length * l.prod :=
-  by
-  convert @prod_map_mul α α _ l (fun _ => -1) id
-  · ext
-    rw [neg_one_mul]
-    rfl
-  · -- Porting note: proof used to be
-    -- convert (prod_repeat _ _).symm
-    -- rw [eq_repeat]
-    -- use l.length_map _
-    -- intro
-    -- rw [mem_map]
-    -- rintro ⟨_, _, rfl⟩
-    -- rfl
-    rw [prod_eq_pow_card _ (-1:α) _, length_map]
-    simp
-  · rw [map_id]
+    (l.map Neg.neg).prod = (-1) ^ l.length * l.prod := by
+  simpa only [id_eq, neg_mul, one_mul, map_const', prod_replicate, map_id]
+    using @prod_map_mul α α _ l (fun _ => -1) id
 #align list.prod_map_neg List.prod_map_neg
 
 @[to_additive]
@@ -326,16 +307,11 @@ theorem prod_lt_prod_of_ne_nil [Preorder M] [CovariantClass M M (· * ·) (· <
     (exists_mem_of_ne_nil l hl).imp fun i hi => ⟨hi, hlt i hi⟩
 #align list.prod_lt_prod_of_ne_nil List.prod_lt_prod_of_ne_nil
 
-set_option linter.deprecated false in
 @[to_additive sum_le_card_nsmul]
 theorem prod_le_pow_card [Preorder M] [CovariantClass M M (Function.swap (· * ·)) (· ≤ ·)]
     [CovariantClass M M (· * ·) (· ≤ ·)] (l : List M) (n : M) (h : ∀ x ∈ l, x ≤ n) :
     l.prod ≤ n ^ l.length := by
-      -- Porting note: proof used to be
-      -- simpa only [map_id'', map_const, prod_repeat] using prod_le_prod' h
-      have := prod_le_prod' h
-      erw [map_id'', map_const', prod_repeat] at this
-      exact this
+      simpa only [map_id'', map_const', prod_replicate] using prod_le_prod' h
 #align list.prod_le_pow_card List.prod_le_pow_card
 
 @[to_additive exists_lt_of_sum_lt]
@@ -560,10 +536,8 @@ theorem prod_map_erase [DecidableEq ι] [CommMonoid M] (f : ι → M) {a} :
         mul_left_comm (f a) (f b)]
 #align list.prod_map_erase List.prod_map_erase
 
--- Porting note: Should this not be `to_additive` of a multiplicative statement?
--- @[simp] -- Porting note: simp can prove this up to commutativity
-theorem sum_const_nat (m n : ℕ) : sum (List.replicate n m) = m * n := by
-  simp only [sum_replicate, smul_eq_mul, mul_comm]
+theorem sum_const_nat (m n : ℕ) : sum (replicate m n) = m * n :=
+  sum_replicate m n
 #align list.sum_const_nat List.sum_const_nat
 
 /-- The product of a list of positive natural numbers is positive,
@@ -584,8 +558,7 @@ If desired, we could add a class stating that `default = 0`.
 
 
 /-- This relies on `default ℕ = 0`. -/
-theorem headI_add_tail_sum (L : List ℕ) : L.headI + L.tail.sum = L.sum :=
-  by
+theorem headI_add_tail_sum (L : List ℕ) : L.headI + L.tail.sum = L.sum := by
   cases L
   · simp
   · simp

Mathlib/Data/List/Count.lean

@@ -167,7 +167,6 @@ end Countp
 
 /-! ### count -/
 
-
 section Count
 
 variable [DecidableEq α]
@@ -268,66 +267,46 @@ theorem count_eq_zero : count a l = 0 ↔ a ∉ l :=
 
 @[simp]
 theorem count_eq_length : count a l = l.length ↔ ∀ b ∈ l, a = b := by
-  rw [count, countp_eq_length]
-  refine ⟨fun h b hb => ?h₁, fun h b hb => ?h₂⟩
-  · refine' Eq.symm _
-    simpa using h b hb
-  · rw [h b hb, beq_self_eq_true]
+  simp_rw [count, countp_eq_length, beq_iff_eq, eq_comm]
 #align list.count_eq_length List.count_eq_length
 
 @[simp]
 theorem count_replicate_self (a : α) (n : ℕ) : count a (replicate n a) = n :=
   (count_eq_length.2 <| fun _ h => (eq_of_mem_replicate h).symm).trans (length_replicate _ _)
+#align list.count_replicate_self List.count_replicate_self
 
 theorem count_replicate (a b : α) (n : ℕ) : count a (replicate n b) = if a = b then n else 0 := by
   split
   exacts [‹a = b› ▸ count_replicate_self _ _, count_eq_zero.2 <| mt eq_of_mem_replicate ‹a ≠ b›]
+#align list.count_replicate List.count_replicate
+
+-- porting note: new lemma
+theorem filter_beq' (l : List α) (a : α) : l.filter (· == a) = replicate (count a l) a := by
+  simp only [count, countp_eq_length_filter, eq_replicate, mem_filter, beq_iff_eq]
+  exact ⟨trivial, fun _ h => h.2⟩
+
+theorem filter_eq' (l : List α) (a : α) : l.filter (· = a) = replicate (count a l) a :=
+  filter_beq' l a
+#align list.filter_eq' List.filter_eq'
+
+theorem filter_eq (l : List α) (a : α) : l.filter (a = ·) = replicate (count a l) a := by
+  simpa only [eq_comm] using filter_eq' l a
+#align list.filter_eq List.filter_eq
+
+-- porting note: new lemma
+theorem filter_beq (l : List α) (a : α) : l.filter (a == ·) = replicate (count a l) a :=
+  filter_eq l a
 
 theorem le_count_iff_replicate_sublist : n ≤ count a l ↔ replicate n a <+ l :=
-  ⟨fun h =>
-    ((replicate_sublist_replicate a).2 h).trans <| by
-      have : filter (Eq a) l = replicate (count a l) a := eq_replicate.2 ⟨?h₁, ?h₂⟩
-      rw [← this]
-      apply filter_sublist
-      · simp [count, countp_eq_length_filter, ← Bool.beq_eq_decide_eq, Bool.beq_comm]
-      · intro b hb
-        simpa [decide_eq_true_eq, eq_comm] using of_mem_filter hb,
+  ⟨fun h => ((replicate_sublist_replicate a).2 h).trans <| filter_eq l a ▸ filter_sublist _,
     fun h => by simpa only [count_replicate_self] using h.count_le a⟩
+#align list.le_count_iff_replicate_sublist List.le_count_iff_replicate_sublist
 
 theorem replicate_count_eq_of_count_eq_length (h : count a l = length l) :
     replicate (count a l) a = l :=
   (le_count_iff_replicate_sublist.mp le_rfl).eq_of_length <|
     (length_replicate (count a l) a).trans h
-
-section deprecated
-
-set_option linter.deprecated false
-
---Porting note: removed `simp`, `simp` can prove it using corresponding lemma about replicate
-@[deprecated count_replicate_self]
-theorem count_repeat_self (a : α) (n : ℕ) : count a (List.repeat a n) = n :=
-  count_replicate_self _ _
-#align list.count_repeat_self List.count_repeat_self
-
---Porting note: removed `simp`, `simp` can prove it using corresponding lemma about replicate
-@[deprecated count_replicate]
-theorem count_repeat (a b : α) (n : ℕ) : count a (List.repeat b n) = if a = b then n else 0 :=
-  count_replicate _ _ _
-#align list.count_repeat List.count_repeat
-
-@[deprecated le_count_iff_replicate_sublist]
-theorem le_count_iff_repeat_sublist {a : α} {l : List α} {n : ℕ} :
-    n ≤ count a l ↔ List.repeat a n <+ l :=
-  le_count_iff_replicate_sublist
-#align list.le_count_iff_repeat_sublist List.le_count_iff_repeat_sublist
-
-@[deprecated replicate_count_eq_of_count_eq_length]
-theorem repeat_count_eq_of_count_eq_length {a : α} {l : List α} (h : count a l = length l) :
-    List.repeat a (count a l) = l :=
-  replicate_count_eq_of_count_eq_length h
-#align list.repeat_count_eq_of_count_eq_length List.repeat_count_eq_of_count_eq_length
-
-end deprecated
+#align list.replicate_count_eq_of_count_eq_length List.replicate_count_eq_of_count_eq_length
 
 @[simp]
 theorem count_filter (h : p a) : count a (filter p l) = count a l := by

Mathlib/Data/List/Dedup.lean

@@ -106,12 +106,7 @@ theorem replicate_dedup {x : α} : ∀ {k}, k ≠ 0 → (replicate k x).dedup =
   | n + 2, _ => by
     rw [replicate_succ, dedup_cons_of_mem (mem_replicate.2 ⟨n.succ_ne_zero, rfl⟩),
       replicate_dedup n.succ_ne_zero]
-
-set_option linter.deprecated false in
-@[deprecated replicate_dedup]
-theorem repeat_dedup {x : α} : ∀ {k}, k ≠ 0 → (List.repeat x k).dedup = [x] :=
-  replicate_dedup
-#align list.repeat_dedup List.repeat_dedup
+#align list.replicate_dedup List.replicate_dedup
 
 theorem count_dedup (l : List α) (a : α) : l.dedup.count a = if a ∈ l then 1 else 0 := by
   simp_rw [count_eq_of_nodup <| nodup_dedup l, mem_dedup]

Mathlib/Data/List/Nodup.lean

@@ -193,11 +193,7 @@ theorem nodup_replicate (a : α) : ∀ {n : ℕ}, Nodup (replicate n a) ↔ n 
     iff_of_false
       (fun H => nodup_iff_sublist.1 H a ((replicate_sublist_replicate _).2 (Nat.le_add_left 2 n)))
       (not_le_of_lt <| Nat.le_add_left 2 n)
-
-set_option linter.deprecated false in
-theorem nodup_repeat (a : α) : ∀ {n : ℕ}, Nodup (List.repeat a n) ↔ n ≤ 1 :=
-  nodup_replicate a
-#align list.nodup_repeat List.nodup_repeat
+#align list.nodup_replicate List.nodup_replicate
 
 @[simp]
 theorem count_eq_one_of_mem [DecidableEq α] {a : α} {l : List α} (d : Nodup l) (h : a ∈ l) :

Mathlib/Data/List/Pairwise.lean

@@ -350,13 +350,7 @@ theorem pairwise_replicate {α : Type _} {r : α → α → Prop} {x : α} (hx :
   | 0 => by simp
   | n + 1 => by simp only [replicate, add_eq, add_zero, pairwise_cons, mem_replicate, ne_eq,
     and_imp, forall_eq_apply_imp_iff', hx, implies_true, pairwise_replicate hx n, and_self]
-
-set_option linter.deprecated false in
-@[deprecated pairwise_replicate]
-theorem pairwise_repeat {α : Type _} {r : α → α → Prop} {x : α} (hx : r x x) :
-    ∀ n : ℕ, Pairwise r (List.repeat x n) :=
-  List.pairwise_replicate hx
-#align list.pairwise_repeat List.pairwise_repeat
+#align list.pairwise_replicate List.pairwise_replicate
 
 /-! ### Pairwise filtering -/
 

Mathlib/Data/List/Perm.lean

@@ -196,37 +196,27 @@ theorem perm_cons_append_cons {l l₁ l₂ : List α} (a : α) (p : l ~ l₁ ++
 #align list.perm_cons_append_cons List.perm_cons_append_cons
 
 @[simp]
-theorem perm_replicate {a : α} {n : ℕ} {l : List α} :
-    l ~ List.replicate n a ↔ l = List.replicate n a :=
+theorem perm_replicate {n : ℕ} {a : α} {l : List α} :
+    l ~ replicate n a ↔ l = replicate n a :=
   ⟨fun p => eq_replicate.2
     ⟨p.length_eq.trans <| length_replicate _ _, fun _b m => eq_of_mem_replicate <| p.subset m⟩,
     fun h => h ▸ Perm.refl _⟩
-
-set_option linter.deprecated false in
-@[deprecated perm_replicate]
-theorem perm_repeat {a : α} {n : ℕ} {l : List α} : l ~ List.repeat a n ↔ l = List.repeat a n :=
-  perm_replicate
-#align list.perm_repeat List.perm_repeat
+#align list.perm_replicate List.perm_replicate
 
 @[simp]
-theorem replicate_perm {a : α} {n : ℕ} {l : List α} :
-    List.replicate n a ~ l ↔ List.replicate n a = l :=
+theorem replicate_perm {n : ℕ} {a : α} {l : List α} :
+    replicate n a ~ l ↔ replicate n a = l :=
   (perm_comm.trans perm_replicate).trans eq_comm
-
-set_option linter.deprecated false in
-@[deprecated replicate_perm]
-theorem repeat_perm {a : α} {n : ℕ} {l : List α} : List.repeat a n ~ l ↔ List.repeat a n = l :=
-  replicate_perm
-#align list.repeat_perm List.repeat_perm
+#align list.replicate_perm List.replicate_perm
 
 @[simp]
 theorem perm_singleton {a : α} {l : List α} : l ~ [a] ↔ l = [a] :=
-  @perm_replicate α a 1 l
+  @perm_replicate α 1 a l
 #align list.perm_singleton List.perm_singleton
 
 @[simp]
 theorem singleton_perm {a : α} {l : List α} : [a] ~ l ↔ [a] = l :=
-  @replicate_perm α a 1 l
+  @replicate_perm α 1 a l
 #align list.singleton_perm List.singleton_perm
 
 theorem Perm.eq_singleton {a : α} {l : List α} (p : l ~ [a]) : l = [a] :=