refactor(*): define list.replicate and migrate to it (#18127)

This definition differs from `list.repeat` by the order of arguments. The new order is in sync with the Lean 4 version.

archive/100-theorems-list/30_ballot_problem.lean

@@ -68,18 +68,18 @@ def counted_sequence (p q : ℕ) : set (list ℤ) :=
 
 /-- An alternative definition of `counted_sequence` that uses `list.perm`. -/
 lemma mem_counted_sequence_iff_perm {p q l} :
-  l ∈ counted_sequence p q ↔ l ~ list.repeat (1 : ℤ) p ++ list.repeat (-1) q :=
+  l ∈ counted_sequence p q ↔ l ~ list.replicate p (1 : ℤ) ++ list.replicate q (-1) :=
 begin
-  rw [list.perm_repeat_append_repeat],
+  rw [list.perm_replicate_append_replicate],
   { simp only [counted_sequence, list.subset_def, mem_set_of_eq, list.mem_cons_iff,
       list.mem_singleton] },
   { norm_num1 }
 end
 
-@[simp] lemma counted_right_zero (p : ℕ) : counted_sequence p 0 = {list.repeat 1 p} :=
+@[simp] lemma counted_right_zero (p : ℕ) : counted_sequence p 0 = {list.replicate p 1} :=
 by { ext l, simp [mem_counted_sequence_iff_perm] }
 
-@[simp] lemma counted_left_zero (q : ℕ) : counted_sequence 0 q = {list.repeat (-1) q} :=
+@[simp] lemma counted_left_zero (q : ℕ) : counted_sequence 0 q = {list.replicate q (-1)} :=
 by { ext l, simp [mem_counted_sequence_iff_perm] }
 
 lemma mem_of_mem_counted_sequence {p q} {l} (hl : l ∈ counted_sequence p q) {x : ℤ} (hx : x ∈ l) :
@@ -286,7 +286,7 @@ begin
     rw mem_singleton_iff at hl,
     subst hl,
     refine λ l hl₁ hl₂, list.sum_pos _ (λ x hx, _) hl₁,
-    rw list.eq_of_mem_repeat (list.mem_of_mem_suffix hx hl₂),
+    rw list.eq_of_mem_replicate (list.mem_of_mem_suffix hx hl₂),
     norm_num },
 end
 

archive/100-theorems-list/45_partition.lean

@@ -335,29 +335,29 @@ begin
     { rwa [nat.nsmul_eq_mul, nat.nsmul_eq_mul, mul_left_inj' i.succ_ne_zero] at h } },
   { simp only [mem_filter, mem_cut, mem_univ, exists_prop, true_and, and_assoc],
     rintros f ⟨hf₁, hf₂, hf₃⟩,
-    refine ⟨⟨∑ i in s, multiset.repeat i (f i / i), _, _⟩, _, _, _⟩,
+    refine ⟨⟨∑ i in s, multiset.replicate (f i / i) i, _, _⟩, _, _, _⟩,
     { intros i hi,
       simp only [exists_prop, mem_sum, mem_map, function.embedding.coe_fn_mk] at hi,
       rcases hi with ⟨t, ht, z⟩,
       apply hs,
-      rwa multiset.eq_of_mem_repeat z },
-    { simp_rw [multiset.sum_sum, multiset.sum_repeat, nat.nsmul_eq_mul, ←hf₁],
+      rwa multiset.eq_of_mem_replicate z },
+    { simp_rw [multiset.sum_sum, multiset.sum_replicate, nat.nsmul_eq_mul, ←hf₁],
       refine sum_congr rfl (λ i hi, nat.div_mul_cancel _),
       rcases hf₃ i hi with ⟨w, hw, hw₂⟩,
       rw ← hw₂,
       exact dvd_mul_left _ _ },
     { intro i,
-      simp_rw [multiset.count_sum', multiset.count_repeat, sum_ite_eq],
+      simp_rw [multiset.count_sum', multiset.count_replicate, sum_ite_eq],
       split_ifs with h h,
       { rcases hf₃ i h with ⟨w, hw₁, hw₂⟩,
         rwa [← hw₂, nat.mul_div_cancel _ (hs i h)] },
       { exact hc _ h } },
     { intros i hi,
       rw mem_sum at hi,
       rcases hi with ⟨j, hj₁, hj₂⟩,
-      rwa multiset.eq_of_mem_repeat hj₂ },
+      rwa multiset.eq_of_mem_replicate hj₂ },
     { ext i,
-      simp_rw [multiset.count_sum', multiset.count_repeat, sum_ite_eq],
+      simp_rw [multiset.count_sum', multiset.count_replicate, sum_ite_eq],
       split_ifs,
       { apply nat.div_mul_cancel,
         rcases hf₃ i h with ⟨w, hw, hw₂⟩,

archive/miu_language/decision_suf.lean

@@ -52,11 +52,11 @@ open miu_atom list nat
 We start by showing that an `miustr` `M::w` can be derived, where `w` consists only of `I`s and
 where `count I w` is a power of 2.
 -/
-private lemma der_cons_repeat (n : ℕ) : derivable (M::(repeat I (2^n))) :=
+private lemma der_cons_replicate (n : ℕ) : derivable (M::(replicate (2^n) I)) :=
 begin
   induction n with k hk,
   { constructor, }, -- base case
-  { rw [succ_eq_add_one, pow_add, pow_one 2, mul_two,repeat_add], -- inductive step
+  { rw [succ_eq_add_one, pow_add, pow_one 2, mul_two,replicate_add], -- inductive step
     exact derivable.r2 hk, },
 end
 
@@ -81,16 +81,16 @@ an even number of `U`s and `z` is any `miustr`.
 Any number of successive occurrences of `"UU"` can be removed from the end of a `derivable` `miustr`
 to produce another `derivable` `miustr`.
 -/
-lemma der_of_der_append_repeat_U_even {z : miustr} {m : ℕ} (h : derivable (z ++ repeat U (m*2)))
-  : derivable z :=
+lemma der_of_der_append_replicate_U_even {z : miustr} {m : ℕ}
+  (h : derivable (z ++ replicate (m*2) U)) : derivable z :=
 begin
   induction m with k hk,
   { revert h,
-    simp only [list.repeat, zero_mul, append_nil, imp_self], },
+    simp only [list.replicate, zero_mul, append_nil, imp_self], },
   { apply hk,
-    simp only [succ_mul, repeat_add] at h,
-    change repeat U 2 with [U,U] at h,
-    rw ←(append_nil (z ++ repeat U (k*2) )),
+    simp only [succ_mul, replicate_add] at h,
+    change replicate 2 U with [U,U] at h,
+    rw ←(append_nil (z ++ replicate (k*2) U)),
     apply derivable.r4,
     simp only [append_nil, append_assoc,h], },
 end
@@ -106,24 +106,24 @@ In fine-tuning my application of `simp`, I issued the following commend to deter
 We may replace several consecutive occurrences of  `"III"` with the same number of `"U"`s.
 In application of the following lemma, `xs` will either be `[]` or `[U]`.
 -/
-lemma der_cons_repeat_I_repeat_U_append_of_der_cons_repeat_I_append (c k : ℕ)
-  (hc : c % 3 = 1 ∨ c % 3 = 2) (xs : miustr) (hder : derivable (M ::(repeat I (c+3*k)) ++ xs)) :
-    derivable (M::(repeat I c ++ repeat U k) ++ xs) :=
+lemma der_cons_replicate_I_replicate_U_append_of_der_cons_replicate_I_append (c k : ℕ)
+  (hc : c % 3 = 1 ∨ c % 3 = 2) (xs : miustr) (hder : derivable (M ::(replicate (c+3*k) I) ++ xs)) :
+    derivable (M::(replicate c I ++ replicate k U) ++ xs) :=
 begin
   revert xs,
   induction k with a ha,
-  { simp only [list.repeat, mul_zero, add_zero, append_nil, forall_true_iff, imp_self],},
+  { simp only [list.replicate, mul_zero, add_zero, append_nil, forall_true_iff, imp_self],},
   { intro xs,
     specialize ha (U::xs),
     intro h₂,
-    simp only [succ_eq_add_one, repeat_add], -- We massage the goal
+    simp only [succ_eq_add_one, replicate_add], -- We massage the goal
     rw [←append_assoc, ←cons_append],        -- into a form amenable
-    change repeat U 1 with [U],             -- to the application of
+    change replicate 1 U with [U],             -- to the application of
     rw [append_assoc, singleton_append],     -- ha.
     apply ha,
     apply derivable.r3,
-    change [I,I,I] with repeat I 3,
-    simp only [cons_append, ←repeat_add],
+    change [I,I,I] with replicate 3 I,
+    simp only [cons_append, ←replicate_add],
     convert h₂, },
 end
 
@@ -178,62 +178,67 @@ end
 
 end arithmetic
 
-lemma repeat_pow_minus_append  {m : ℕ} : M :: repeat I (2^m - 1) ++ [I] = M::(repeat I (2^m)) :=
+lemma replicate_pow_minus_append  {m : ℕ} :
+  M :: replicate (2^m - 1) I ++ [I] = M::(replicate (2^m) I) :=
 begin
-  change [I] with repeat I 1,
-  rw [cons_append, ←repeat_add, tsub_add_cancel_of_le (one_le_pow' m 1)],
+  change [I] with replicate 1 I,
+  rw [cons_append, ←replicate_add, tsub_add_cancel_of_le (one_le_pow' m 1)],
 end
 
 /--
-`der_repeat_I_of_mod3` states that `M::y` is `derivable` if `y` is any `miustr` consisiting just of
-`I`s, where `count I y` is 1 or 2 modulo 3.
+`der_replicate_I_of_mod3` states that `M::y` is `derivable` if `y` is any `miustr` consisiting just
+of `I`s, where `count I y` is 1 or 2 modulo 3.
 -/
-lemma der_repeat_I_of_mod3 (c : ℕ) (h : c % 3 = 1 ∨ c % 3 = 2):
-  derivable (M::(repeat I c)) :=
+lemma der_replicate_I_of_mod3 (c : ℕ) (h : c % 3 = 1 ∨ c % 3 = 2):
+  derivable (M::(replicate c I)) :=
 begin
-  -- From `der_cons_repeat`, we can derive the `miustr` `M::w` described in the introduction.
+  -- From `der_cons_replicate`, we can derive the `miustr` `M::w` described in the introduction.
   cases (le_pow2_and_pow2_eq_mod3 c h) with m hm, -- `2^m` will be  the number of `I`s in `M::w`
-  have hw₂ : derivable (M::(repeat I (2^m)) ++ repeat U ((2^m -c)/3 % 2)),
+  have hw₂ : derivable (M::(replicate (2^m) I) ++ replicate ((2^m -c)/3 % 2) U),
   { cases mod_two_eq_zero_or_one ((2^m -c)/3) with h_zero h_one,
-    { simp only [der_cons_repeat m, append_nil,list.repeat, h_zero], }, -- `(2^m - c)/3 ≡ 0 [MOD 2]`
-    { rw [h_one, ←repeat_pow_minus_append, append_assoc], -- case `(2^m - c)/3 ≡ 1 [MOD 2]`
+    { -- `(2^m - c)/3 ≡ 0 [MOD 2]`
+      simp only [der_cons_replicate m, append_nil,list.replicate, h_zero], },
+    { rw [h_one, ←replicate_pow_minus_append, append_assoc], -- case `(2^m - c)/3 ≡ 1 [MOD 2]`
       apply derivable.r1,
-      rw repeat_pow_minus_append,
-      exact (der_cons_repeat m), }, },
-  have hw₃ : derivable (M::(repeat I c) ++ repeat U ((2^m-c)/3) ++ repeat U ((2^m-c)/3 % 2)),
-  { apply der_cons_repeat_I_repeat_U_append_of_der_cons_repeat_I_append c ((2^m-c)/3) h,
+      rw replicate_pow_minus_append,
+      exact (der_cons_replicate m), }, },
+  have hw₃ :
+    derivable (M::(replicate c I) ++ replicate ((2^m-c)/3) U ++ replicate ((2^m-c)/3 % 2) U),
+  { apply der_cons_replicate_I_replicate_U_append_of_der_cons_replicate_I_append c ((2^m-c)/3) h,
     convert hw₂, -- now we must show `c + 3 * ((2 ^ m - c) / 3) = 2 ^ m`
     rw nat.mul_div_cancel',
     { exact add_tsub_cancel_of_le hm.1 },
     { exact (modeq_iff_dvd' hm.1).mp hm.2.symm } },
-  rw [append_assoc, ←repeat_add _ _] at hw₃,
+  rw [append_assoc, ←replicate_add _ _] at hw₃,
   cases add_mod2 ((2^m-c)/3) with t ht,
   rw ht at hw₃,
-  exact der_of_der_append_repeat_U_even hw₃,
+  exact der_of_der_append_replicate_U_even hw₃,
 end
 
 example (c : ℕ) (h : c % 3 = 1 ∨ c % 3 = 2):
-  derivable (M::(repeat I c)) :=
+  derivable (M::(replicate c I)) :=
 begin
-  -- From `der_cons_repeat`, we can derive the `miustr` `M::w` described in the introduction.
+  -- From `der_cons_replicate`, we can derive the `miustr` `M::w` described in the introduction.
   cases (le_pow2_and_pow2_eq_mod3 c h) with m hm, -- `2^m` will be  the number of `I`s in `M::w`
-  have hw₂ : derivable (M::(repeat I (2^m)) ++ repeat U ((2^m -c)/3 % 2)),
+  have hw₂ : derivable (M::(replicate (2^m) I) ++ replicate ((2^m -c)/3 % 2) U),
   { cases mod_two_eq_zero_or_one ((2^m -c)/3) with h_zero h_one,
-    { simp only [der_cons_repeat m, append_nil, list.repeat,h_zero], }, -- `(2^m - c)/3 ≡ 0 [MOD 2]`
-    { rw [h_one, ←repeat_pow_minus_append, append_assoc], -- case `(2^m - c)/3 ≡ 1 [MOD 2]`
+    { -- `(2^m - c)/3 ≡ 0 [MOD 2]`
+      simp only [der_cons_replicate m, append_nil, list.replicate, h_zero] },
+    { rw [h_one, ←replicate_pow_minus_append, append_assoc], -- case `(2^m - c)/3 ≡ 1 [MOD 2]`
       apply derivable.r1,
-      rw repeat_pow_minus_append,
-      exact (der_cons_repeat m), }, },
-  have hw₃ : derivable (M::(repeat I c) ++ repeat U ((2^m-c)/3) ++ repeat U ((2^m-c)/3 % 2)),
-  { apply der_cons_repeat_I_repeat_U_append_of_der_cons_repeat_I_append c ((2^m-c)/3) h,
+      rw replicate_pow_minus_append,
+      exact (der_cons_replicate m), }, },
+  have hw₃ :
+    derivable (M::(replicate c I) ++ replicate ((2^m-c)/3) U ++ replicate ((2^m-c)/3 % 2) U),
+  { apply der_cons_replicate_I_replicate_U_append_of_der_cons_replicate_I_append c ((2^m-c)/3) h,
     convert hw₂, -- now we must show `c + 3 * ((2 ^ m - c) / 3) = 2 ^ m`
     rw nat.mul_div_cancel',
     { exact add_tsub_cancel_of_le hm.1 },
     { exact (modeq_iff_dvd' hm.1).mp hm.2.symm } },
-  rw [append_assoc, ←repeat_add _ _] at hw₃,
+  rw [append_assoc, ←replicate_add _ _] at hw₃,
   cases add_mod2 ((2^m-c)/3) with t ht,
   rw ht at hw₃,
-  exact der_of_der_append_repeat_U_even hw₃,
+  exact der_of_der_append_replicate_U_even hw₃,
 end
 
 /-!
@@ -278,12 +283,12 @@ begin
   rcases (exists_cons_of_ne_nil this) with ⟨y,ys,rfl⟩,
   rw head at mhead,
   rw mhead at *,
-  rsuffices ⟨c, rfl, hc⟩ : ∃ c, repeat I c = ys ∧ (c % 3 = 1 ∨ c % 3 = 2),
-  { exact der_repeat_I_of_mod3 c hc, },
+  rsuffices ⟨c, rfl, hc⟩ : ∃ c, replicate c I = ys ∧ (c % 3 = 1 ∨ c % 3 = 2),
+  { exact der_replicate_I_of_mod3 c hc, },
   { simp only [count] at *,
     use (count I ys),
     refine and.intro _ hi,
-    apply repeat_count_eq_of_count_eq_length,
+    apply replicate_count_eq_of_count_eq_length,
     exact count_I_eq_length_of_count_U_zero_and_neg_mem hu nmtail, },
 end
 

src/algebra/big_operators/basic.lean

@@ -245,7 +245,7 @@ by rw [prod_insert (not_mem_singleton.2 h), prod_singleton]
 
 @[simp, priority 1100, to_additive]
 lemma prod_const_one : (∏ x in s, (1 : β)) = 1 :=
-by simp only [finset.prod, multiset.map_const, multiset.prod_repeat, one_pow]
+by simp only [finset.prod, multiset.map_const, multiset.prod_replicate, one_pow]
 
 @[simp, to_additive]
 lemma prod_image [decidable_eq α] {s : finset γ} {g : γ → α} :
@@ -1126,7 +1126,7 @@ begin
 end
 
 @[simp, to_additive] lemma prod_const (b : β) : (∏ x in s, b) = b ^ s.card :=
-(congr_arg _ $ s.val.map_const b).trans $ multiset.prod_repeat b s.card
+(congr_arg _ $ s.val.map_const b).trans $ multiset.prod_replicate b s.card
 
 @[to_additive]
 lemma pow_eq_prod_const (b : β) : ∀ n, b ^ n = ∏ k in range n, b := by simp
@@ -1382,7 +1382,7 @@ begin
   classical,
   apply finset.induction_on' S, { simp },
   intros a T haS _ haT IH,
-  repeat {rw finset.prod_insert haT},
+  repeat { rw finset.prod_insert haT },
   exact mul_dvd_mul (h a haS) IH,
 end
 

src/algebra/big_operators/multiset/basic.lean

@@ -86,8 +86,8 @@ lemma 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 n]
 
-@[simp, to_additive] lemma prod_repeat (a : α) (n : ℕ) : (repeat a n).prod = a ^ n :=
-by simp [repeat, list.prod_repeat]
+@[simp, to_additive] lemma prod_replicate (a : α) (n : ℕ) : (replicate n a).prod = a ^ n :=
+by simp [replicate, list.prod_replicate]
 
 @[to_additive]
 lemma prod_map_eq_pow_single [decidable_eq ι] (i : ι) (hf : ∀ i' ≠ i, i' ∈ m → f i' = 1) :
@@ -107,7 +107,7 @@ end
 
 @[to_additive]
 lemma pow_count [decidable_eq α] (a : α) : a ^ s.count a = (s.filter (eq a)).prod :=
-by rw [filter_eq, prod_repeat]
+by rw [filter_eq, prod_replicate]
 
 @[to_additive]
 lemma prod_hom [comm_monoid β] (s : multiset α) {F : Type*} [monoid_hom_class F α β] (f : F) :
@@ -134,7 +134,7 @@ quotient.induction_on s $ λ l,
   by simp only [l.prod_hom_rel h₁ h₂, quot_mk_to_coe, coe_map, coe_prod]
 
 @[to_additive]
-lemma prod_map_one : prod (m.map (λ i, (1 : α))) = 1 := by rw [map_const, prod_repeat, one_pow]
+lemma prod_map_one : prod (m.map (λ i, (1 : α))) = 1 := by rw [map_const, prod_replicate, one_pow]
 
 @[simp, to_additive]
 lemma prod_map_mul : (m.map $ λ i, f i * g i).prod = (m.map f).prod * (m.map g).prod :=
@@ -321,7 +321,7 @@ lemma prod_le_prod_map (f : α → α) (h : ∀ x, x ∈ s → x ≤ f x) : s.pr
 
 @[to_additive card_nsmul_le_sum]
 lemma pow_card_le_prod (h : ∀ x ∈ s, a ≤ x) : a ^ s.card ≤ s.prod :=
-by { rw [←multiset.prod_repeat, ←multiset.map_const], exact prod_map_le_prod _ h }
+by { rw [←multiset.prod_replicate, ←multiset.map_const], exact prod_map_le_prod _ h }
 
 end ordered_comm_monoid
 

src/algebra/gcd_monoid/multiset.lean

@@ -180,8 +180,8 @@ lemma extract_gcd (s : multiset α) (hs : s ≠ 0) :
 begin
   classical,
   by_cases h : ∀ x ∈ s, x = (0 : α),
-  { use repeat 1 s.card,
-    rw [map_repeat, eq_repeat, mul_one, s.gcd_eq_zero_iff.2 h, ←nsmul_singleton, ←gcd_dedup],
+  { use replicate s.card 1,
+    rw [map_replicate, eq_replicate, mul_one, s.gcd_eq_zero_iff.2 h, ←nsmul_singleton, ←gcd_dedup],
     rw [dedup_nsmul (card_pos.2 hs).ne', dedup_singleton, gcd_singleton],
     exact ⟨⟨rfl, h⟩, normalize_one⟩ },
   { choose f hf using @gcd_dvd _ _ _ s,

src/algebra/hom/freiman.lean

@@ -196,7 +196,7 @@ ext $ λ x, rfl
 def const (A : set α) (n : ℕ) (b : β) : A →*[n] β :=
 { to_fun := λ _, b,
   map_prod_eq_map_prod' := λ s t _ _ hs ht _,
-    by rw [multiset.map_const, multiset.map_const, prod_repeat, prod_repeat, hs, ht] }
+    by rw [multiset.map_const, multiset.map_const, prod_replicate, prod_replicate, hs, ht] }
 
 @[simp, to_additive] lemma const_apply (n : ℕ) (b : β) (x : α) : const A n b x = b := rfl
 
@@ -341,20 +341,20 @@ begin
     rw [hs, ht] },
   rw [←hs, card_pos_iff_exists_mem] at hm,
   obtain ⟨a, ha⟩ := hm,
-  suffices : ((s + repeat a (n - m)).map f).prod = ((t + repeat a (n - m)).map f).prod,
+  suffices : ((s + replicate (n - m) a).map f).prod = ((t + replicate (n - m) a).map f).prod,
   { simp_rw [multiset.map_add, prod_add] at this,
     exact mul_right_cancel this },
   replace ha := hsA _ ha,
   refine map_prod_eq_map_prod f (λ x hx, _) (λ x hx, _) _ _ _,
   rotate 2, assumption, -- Can't infer `A` and `n` from the context, so do it manually.
   { rw mem_add at hx,
     refine hx.elim (hsA _) (λ h, _),
-    rwa eq_of_mem_repeat h },
+    rwa eq_of_mem_replicate h },
   { rw mem_add at hx,
     refine hx.elim (htA _) (λ h, _),
-    rwa eq_of_mem_repeat h },
-  { rw [card_add, hs, card_repeat, add_tsub_cancel_of_le h] },
-  { rw [card_add, ht, card_repeat, add_tsub_cancel_of_le h] },
+    rwa eq_of_mem_replicate h },
+  { rw [card_add, hs, card_replicate, add_tsub_cancel_of_le h] },
+  { rw [card_add, ht, card_replicate, add_tsub_cancel_of_le h] },
   { rw [prod_add, prod_add, hst] }
 end
 

src/algebra/module/dedekind_domain.lean

@@ -48,7 +48,7 @@ begin
     { suffices : (normalized_factors _).count p = 0,
       { rw [this, zero_min, pow_zero, ideal.one_eq_top] },
       { rw [multiset.count_eq_zero, normalized_factors_of_irreducible_pow
-          (prime_of_mem q hq).irreducible, multiset.mem_repeat],
+          (prime_of_mem q hq).irreducible, multiset.mem_replicate],
         exact λ H, pq $ H.2.trans $ normalize_eq q } },
     { rw ← ideal.zero_eq_bot, apply pow_ne_zero, exact (prime_of_mem q hq).ne_zero },
     { exact (prime_of_mem p hp).irreducible } }

src/algebra/monoid_algebra/degree.lean

@@ -96,9 +96,9 @@ lemma sup_support_pow_le (degb0 : degb 0 ≤ 0) (degbm : ∀ a b, degb (a + b) 
   (n : ℕ) (f : add_monoid_algebra R A) :
   (f ^ n).support.sup degb ≤ n • (f.support.sup degb) :=
 begin
-  rw [← list.prod_repeat, ←list.sum_repeat],
+  rw [← list.prod_replicate, ←list.sum_replicate],
   refine (sup_support_list_prod_le degb0 degbm _).trans_eq _,
-  rw list.map_repeat,
+  rw list.map_replicate,
 end
 
 lemma le_inf_support_pow (degt0 : 0 ≤ degt 0) (degtm : ∀ a b, degt a + degt b ≤ degt (a + b))

src/algebra/polynomial/big_operators.lean

@@ -192,8 +192,8 @@ begin
   nontriviality R,
   apply nat_degree_multiset_prod',
   suffices : (t.map (λ f, leading_coeff f)).prod = 1, { rw this, simp },
-  convert prod_repeat (1 : R) t.card,
-  { simp only [eq_repeat, multiset.card_map, eq_self_iff_true, true_and],
+  convert prod_replicate (1 : R) t.card,
+  { simp only [eq_replicate, multiset.card_map, eq_self_iff_true, true_and],
     rintros i hi,
     obtain ⟨i, hi, rfl⟩ := multiset.mem_map.mp hi,
     apply h, assumption },