chore(*): sync list.replicate with Mathlib 4 (#18181)

urkud · urkud · commit 47adfab39a11 · 2023-01-16T07:12:55.000Z
Sync arguments order and golfs with leanprover-community/mathlib4#1579
diff --git a/src/algebra/big_operators/basic.lean b/src/algebra/big_operators/basic.lean
@@ -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_replicate b s.card
+(congr_arg _ $ s.val.map_const b).trans $ multiset.prod_replicate s.card b
 
 @[to_additive]
 lemma pow_eq_prod_const (b : β) : ∀ n, b ^ n = ∏ k in range n, b := by simp
diff --git a/src/algebra/big_operators/multiset/basic.lean b/src/algebra/big_operators/multiset/basic.lean
@@ -86,7 +86,7 @@ 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_replicate (a : α) (n : ℕ) : (replicate n a).prod = a ^ n :=
+@[simp, to_additive] lemma prod_replicate (n : ℕ) (a : α) : (replicate n a).prod = a ^ n :=
 by simp [replicate, list.prod_replicate]
 
 @[to_additive]
diff --git a/src/algebra/polynomial/big_operators.lean b/src/algebra/polynomial/big_operators.lean
@@ -192,7 +192,7 @@ begin
   nontriviality R,
   apply nat_degree_multiset_prod',
   suffices : (t.map (λ f, leading_coeff f)).prod = 1, { rw this, simp },
-  convert prod_replicate (1 : R) t.card,
+  convert prod_replicate t.card (1 : R),
   { 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,
diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean
@@ -450,13 +450,13 @@ append_inj_right h rfl
 theorem append_right_cancel {s₁ s₂ t : list α} (h : s₁ ++ t = s₂ ++ t) : s₁ = s₂ :=
 append_inj_left' h rfl
 
-theorem append_right_injective (s : list α) : function.injective (λ t, s ++ t) :=
+theorem append_right_injective (s : list α) : injective (λ t, s ++ t) :=
 λ t₁ t₂, append_left_cancel
 
 theorem append_right_inj {t₁ t₂ : list α} (s) : s ++ t₁ = s ++ t₂ ↔ t₁ = t₂ :=
 (append_right_injective s).eq_iff
 
-theorem append_left_injective (t : list α) : function.injective (λ s, s ++ t) :=
+theorem append_left_injective (t : list α) : injective (λ s, s ++ t) :=
 λ s₁ s₂, append_right_cancel
 
 theorem append_left_inj {s₁ s₂ : list α} (t) : s₁ ++ t = s₂ ++ t ↔ s₁ = s₂ :=
@@ -475,7 +475,9 @@ end
 
 /-! ### replicate -/
 
+@[simp] theorem replicate_zero (a : α) : replicate 0 a = [] := rfl
 @[simp] theorem replicate_succ (a : α) (n) : replicate (n + 1) a = a :: replicate n a := rfl
+theorem replicate_one (a : α) : replicate 1 a = [a] := rfl
 
 @[simp] theorem length_replicate : ∀ n (a : α), length (replicate n a) = n
 | 0 a := rfl
@@ -498,16 +500,19 @@ theorem eq_replicate {a : α} {n} {l : list α} : l = replicate n a ↔ length l
 ⟨λ h, h.symm ▸ ⟨length_replicate _ _, λ b, eq_of_mem_replicate⟩,
  λ ⟨e, al⟩, e ▸ eq_replicate_of_mem al⟩
 
-theorem replicate_add (a : α) (m n) : replicate (m + n) a = replicate m a ++ replicate n a :=
+theorem replicate_add (m n) (a : α) : replicate (m + n) a = replicate m a ++ replicate n a :=
 by induction m; simp only [*, zero_add, succ_add, replicate]; refl
 
-theorem replicate_subset_singleton (a : α) (n) : replicate n a ⊆ [a] :=
+theorem replicate_succ' (n) (a : α) : replicate (n + 1) a = replicate n a ++ [a] :=
+replicate_add n 1 a
+
+theorem replicate_subset_singleton (n) (a : α) : replicate n a ⊆ [a] :=
 λ b h, mem_singleton.2 (eq_of_mem_replicate h)
 
 lemma subset_singleton_iff {a : α} {L : list α} : L ⊆ [a] ↔ ∃ n, L = replicate n a :=
 by simp only [eq_replicate, subset_def, mem_singleton, exists_eq_left']
 
-@[simp] theorem map_replicate (f : α → β) (a : α) (n) : map f (replicate n a) = replicate n (f a) :=
+@[simp] theorem map_replicate (f : α → β) (n a) : map f (replicate n a) = replicate n (f a) :=
 by induction n; [refl, simp only [*, replicate, map]]; split; refl
 
 @[simp] theorem tail_replicate (n) (a : α) : tail (replicate n a) = replicate (n - 1) a :=
@@ -516,8 +521,7 @@ by cases n; refl
 @[simp] theorem join_replicate_nil (n : ℕ) : join (replicate n []) = @nil α :=
 by induction n; [refl, simp only [*, replicate, join, append_nil]]
 
-lemma replicate_right_injective {n : ℕ} (hn : n ≠ 0) :
-  function.injective (replicate n : α → list α) :=
+lemma replicate_right_injective {n : ℕ} (hn : n ≠ 0) : injective (replicate n : α → list α) :=
 λ _ _ h, (eq_replicate.1 h).2 _ $ mem_replicate.2 ⟨hn, rfl⟩
 
 lemma replicate_right_inj {a b : α} {n : ℕ} (hn : n ≠ 0) :
@@ -529,8 +533,8 @@ lemma replicate_right_inj {a b : α} {n : ℕ} (hn : n ≠ 0) :
 | 0 := by simp
 | (n + 1) := (replicate_right_inj n.succ_ne_zero).trans $ by simp only [n.succ_ne_zero, false_or]
 
-lemma replicate_left_injective (a : α) : function.injective (λ n, replicate n a) :=
-function.left_inverse.injective (λ n, length_replicate n a)
+lemma replicate_left_injective (a : α) : injective (λ n, replicate n a) :=
+left_inverse.injective (λ n, length_replicate n a)
 
 @[simp] lemma replicate_left_inj {a : α} {n m : ℕ} :
   replicate n a = replicate m a ↔ n = m :=
@@ -660,8 +664,8 @@ by simp only [reverse_core_eq, map_append, map_reverse]
 by induction l; [refl, simp only [*, reverse_cons, mem_append, mem_singleton, mem_cons_iff,
   not_mem_nil, false_or, or_false, or_comm]]
 
-@[simp] theorem reverse_replicate (a : α) (n) : reverse (replicate n a) = replicate n a :=
-eq_replicate.2 ⟨by simp only [length_reverse, length_replicate],
+@[simp] theorem reverse_replicate (n) (a : α) : reverse (replicate n a) = replicate n a :=
+eq_replicate.2 ⟨by rw [length_reverse, length_replicate],
   λ b h, eq_of_mem_replicate (mem_reverse.1 h)⟩
 
 /-! ### empty -/
@@ -729,12 +733,11 @@ theorem last_mem : ∀ {l : list α} (h : l ≠ []), last l h ∈ l
 | [a] h := or.inl rfl
 | (a::b::l) h := or.inr $ by { rw [last_cons_cons], exact last_mem (cons_ne_nil b l) }
 
-lemma last_replicate_succ (a m : ℕ) :
+lemma last_replicate_succ (m : ℕ) (a : α) :
   (replicate (m + 1) a).last (ne_nil_of_length_eq_succ (length_replicate (m + 1) a)) = a :=
 begin
-  induction m with k IH,
-  { simp },
-  { simpa only [replicate_succ, last] }
+  simp only [replicate_succ'],
+  exact last_append_singleton _
 end
 
 /-! ### last' -/
@@ -1796,12 +1799,13 @@ lemma map_eq_replicate_iff {l : list α} {f : α → β} {b : β} :
   l.map f = replicate l.length b ↔ (∀ x ∈ l, f x = b) :=
 by simp [eq_replicate]
 
-@[simp]
-theorem map_const (l : list α) (b : β) : map (function.const α b) l = replicate l.length b :=
+@[simp] theorem map_const (l : list α) (b : β) : map (const α b) l = replicate l.length b :=
 map_eq_replicate_iff.mpr (λ x _, rfl)
 
-theorem eq_of_mem_map_const {b₁ b₂ : β} {l : list α} (h : b₁ ∈ map (function.const α b₂) l) :
-  b₁ = b₂ :=
+-- Not a `simp` lemma because `function.const` is reducible in Lean 3
+theorem map_const' (l : list α) (b : β) : map (λ _, b) l = replicate l.length b := map_const l b
+
+theorem eq_of_mem_map_const {b₁ b₂ : β} {l : list α} (h : b₁ ∈ map (const α b₂) l) : b₁ = b₂ :=
 by rw map_const at h; exact eq_of_mem_replicate h
 
 /-! ### map₂ -/
diff --git a/src/data/list/big_operators/basic.lean b/src/data/list/big_operators/basic.lean
@@ -51,7 +51,7 @@ lemma prod_eq_foldr : l.prod = foldr (*) 1 l :=
 list.rec_on l rfl $ λ a l ihl, by rw [prod_cons, foldr_cons, ihl]
 
 @[simp, priority 500, to_additive]
-theorem prod_replicate (a : M) (n : ℕ) : (replicate n a).prod = a ^ n :=
+theorem prod_replicate (n : ℕ) (a : M) : (replicate n a).prod = a ^ n :=
 begin
   induction n with n ih,
   { rw pow_zero, refl },
@@ -94,13 +94,8 @@ l.prod_hom₂ (*) mul_mul_mul_comm (mul_one _) _ _
 @[simp]
 lemma prod_map_neg {α} [comm_monoid α] [has_distrib_neg α] (l : list α) :
   (l.map has_neg.neg).prod = (-1) ^ l.length * l.prod :=
-begin
-  convert @prod_map_mul α α _ l (λ _, -1) id,
-  { ext, rw neg_one_mul, refl },
-  { rw [← prod_replicate, map_eq_replicate_iff.2],
-    exact λ _ _, rfl },
-  { rw l.map_id },
-end
+by simpa only [id, neg_mul, one_mul, map_const', prod_replicate, map_id]
+    using @prod_map_mul α α _ l (λ _, -1) id
 
 @[to_additive]
 lemma prod_map_hom (L : list ι) (f : ι → M) {G : Type*} [monoid_hom_class G M N] (g : G) :
@@ -478,7 +473,7 @@ lemma prod_map_erase [decidable_eq ι] [comm_monoid M] (f : ι → M) {a} :
         mul_left_comm (f a) (f b)], }
   end
 
-@[simp] lemma sum_const_nat (m n : ℕ) : sum (replicate m n) = m * n :=
+lemma sum_const_nat (m n : ℕ) : sum (replicate m n) = m * n :=
 by rw [sum_replicate, smul_eq_mul]
 
 /-- The product of a list of positive natural numbers is positive,
diff --git a/src/data/list/count.lean b/src/data/list/count.lean
@@ -174,12 +174,15 @@ begin
   exacts [h ▸ count_replicate_self _ _, count_eq_zero_of_not_mem $ mt eq_of_mem_replicate h]
 end
 
+theorem filter_eq (l : list α) (a : α) : l.filter (eq a) = replicate (count a l) a :=
+by simp [eq_replicate, count, countp_eq_length_filter, @eq_comm _ _ a]
+
+theorem filter_eq' (l : list α) (a : α) : l.filter (λ x, x = a) = replicate (count a l) a :=
+by simp only [filter_eq, @eq_comm _ _ a]
+
 lemma le_count_iff_replicate_sublist {a : α} {l : list α} {n : ℕ} :
   n ≤ count a l ↔ replicate n a <+ l :=
-⟨λ h, ((replicate_sublist_replicate a).2 h).trans $
-  have filter (eq a) l = replicate (count a l) a, from eq_replicate.2
-    ⟨by simp only [count, countp_eq_length_filter], λ b m, (of_mem_filter m).symm⟩,
-  by rw ← this; apply filter_sublist,
+⟨λ h, ((replicate_sublist_replicate a).2 h).trans $ filter_eq l a ▸ filter_sublist _,
  λ h, by simpa only [count_replicate_self] using h.count_le a⟩
 
 lemma replicate_count_eq_of_count_eq_length  {a : α} {l : list α} (h : count a l = length l)  :
diff --git a/src/data/list/perm.lean b/src/data/list/perm.lean
@@ -150,21 +150,21 @@ theorem perm_cons_append_cons {l l₁ l₂ : list α} (a : α) (p : l ~ l₁++l
   a::l ~ l₁++(a::l₂) :=
 (p.cons a).trans perm_middle.symm
 
-@[simp] theorem perm_replicate {a : α} {n : ℕ} {l : list α} :
+@[simp] theorem perm_replicate {n : ℕ} {a : α} {l : list α} :
   l ~ replicate n a ↔ l = replicate n a :=
 ⟨λ p, eq_replicate.2
   ⟨p.length_eq.trans $ length_replicate _ _, λ b m, eq_of_mem_replicate $ p.subset m⟩,
   λ h, h ▸ perm.refl _⟩
 
-@[simp] theorem replicate_perm {a : α} {n : ℕ} {l : list α} :
+@[simp] theorem replicate_perm {n : ℕ} {a : α} {l : list α} :
   replicate n a ~ l ↔ replicate n a = l :=
 (perm_comm.trans perm_replicate).trans eq_comm
 
 @[simp] theorem perm_singleton {a : α} {l : list α} : l ~ [a] ↔ l = [a] :=
-@perm_replicate α a 1 l
+@perm_replicate α 1 a l
 
 @[simp] theorem singleton_perm {a : α} {l : list α} : [a] ~ l ↔ [a] = l :=
-@replicate_perm α a 1 l
+@replicate_perm α 1 a l
 
 alias perm_singleton ↔ perm.eq_singleton _
 alias singleton_perm ↔ perm.singleton_eq _
diff --git a/src/data/multiset/basic.lean b/src/data/multiset/basic.lean
@@ -623,20 +623,21 @@ instance is_well_founded_lt : _root_.well_founded_lt (multiset α) := ⟨well_fo
 /-- `replicate n a` is the multiset containing only `a` with multiplicity `n`. -/
 def replicate (n : ℕ) (a : α) : multiset α := replicate n a
 
-lemma coe_replicate (a : α) (n : ℕ) : (list.replicate n a : multiset α) = replicate n a := rfl
+lemma coe_replicate (n : ℕ) (a : α) : (list.replicate n a : multiset α) = replicate n a := rfl
 
 @[simp] lemma replicate_zero (a : α) : replicate 0 a = 0 := rfl
+@[simp] lemma replicate_succ (a : α) (n) : replicate (n + 1) a = a ::ₘ replicate n a := rfl
 
-@[simp] lemma replicate_succ (a : α) (n) : replicate (n+1) a = a ::ₘ replicate n a := rfl
-
-lemma replicate_add (a : α) (m n : ℕ) : replicate (m + n) a = replicate m a + replicate n a :=
+lemma replicate_add (m n : ℕ) (a : α) : replicate (m + n) a = replicate m a + replicate n a :=
 congr_arg _ $ list.replicate_add _ _ _
 
 /-- `multiset.replicate` as an `add_monoid_hom`. -/
 @[simps] def replicate_add_monoid_hom (a : α) : ℕ →+ multiset α :=
-{ to_fun := λ n, replicate n a, map_zero' := replicate_zero a, map_add' := replicate_add a }
+{ to_fun := λ n, replicate n a,
+  map_zero' := replicate_zero a,
+  map_add' := λ _ _, replicate_add _ _ a }
 
-@[simp] lemma replicate_one (a : α) : replicate 1 a = {a} := rfl
+lemma replicate_one (a : α) : replicate 1 a = {a} := rfl
 
 @[simp] lemma card_replicate : ∀ n (a : α), card (replicate n a) = n := length_replicate
 
@@ -645,7 +646,7 @@ lemma mem_replicate {a b : α} {n : ℕ} : b ∈ replicate n a ↔ n ≠ 0 ∧ b
 theorem eq_of_mem_replicate {a b : α} {n} : b ∈ replicate n a → b = a := eq_of_mem_replicate
 
 theorem eq_replicate_card {a : α} {s : multiset α} : s = replicate s.card a ↔ ∀ b ∈ s, b = a :=
-quot.induction_on s $ λ l, coe_eq_coe.trans $ perm_replicate.trans $ eq_replicate_length
+quot.induction_on s $ λ l, coe_eq_coe.trans $ perm_replicate.trans eq_replicate_length
 
 alias eq_replicate_card ↔ _ eq_replicate_of_mem
 
@@ -665,7 +666,7 @@ lemma replicate_right_injective {n : ℕ} (hn : n ≠ 0) :
 theorem replicate_left_injective (a : α) : function.injective (λ n, replicate n a) :=
 λ m n h, by rw [← (eq_replicate.1 h).1, card_replicate]
 
-theorem replicate_subset_singleton : ∀ (a : α) n, replicate n a ⊆ {a} := replicate_subset_singleton
+theorem replicate_subset_singleton : ∀ n (a : α), replicate n a ⊆ {a} := replicate_subset_singleton
 
 theorem replicate_le_coe {a : α} {n} {l : list α} :
   replicate n a ≤ l ↔ list.replicate n a <+ l :=
@@ -940,6 +941,9 @@ quot.induction_on s $ λ l, congr_arg coe $ map_id _
   map (function.const α b) s = replicate s.card b :=
 quot.induction_on s $ λ l, congr_arg coe $ map_const _ _
 
+-- Not a `simp` lemma because `function.const` is reducibel in Lean 3
+theorem map_const' (s : multiset α) (b : β) : map (λ _,  b) s = replicate s.card b := map_const s b
+
 theorem eq_of_mem_map_const {b₁ b₂ : β} {l : list α} (h : b₁ ∈ map (function.const α b₂) l) :
   b₁ = b₂ :=
 eq_of_mem_replicate $ by rwa map_const at h
@@ -1902,16 +1906,12 @@ calc m.attach.count a
 ... = m.count (a : α) : congr_arg _ m.attach_map_coe
 
 lemma filter_eq' (s : multiset α) (b : α) : s.filter (= b) = replicate (count b s) b :=
-begin
-  ext a,
-  rw [count_replicate, count_filter],
-  exact if_ctx_congr iff.rfl (λ h, congr_arg _ h) (λ h, rfl),
-end
+quotient.induction_on s $ λ l, congr_arg coe $ filter_eq' l b
 
 lemma filter_eq (s : multiset α) (b : α) : s.filter (eq b) = replicate (count b s) b :=
 by simp_rw [←filter_eq', eq_comm]
 
-@[simp] lemma replicate_inter (x : α) (n : ℕ) (s : multiset α) :
+@[simp] lemma replicate_inter (n : ℕ) (x : α) (s : multiset α) :
   replicate n x ∩ s = replicate (min n (s.count x)) x :=
 begin
   ext y,
diff --git a/src/data/nat/digits.lean b/src/data/nat/digits.lean
@@ -347,8 +347,7 @@ begin
     { cases hm rfl },
     { simp } },
   { cases m, { cases hm rfl },
-    simp_rw [digits_one, list.last_replicate_succ 1 m],
-    norm_num },
+    simpa only [digits_one, list.last_replicate_succ m 1] using one_ne_zero },
   revert hm,
   apply nat.strong_induction_on m,
   intros n IH hn,
diff --git a/src/data/nat/factors.lean b/src/data/nat/factors.lean
@@ -158,7 +158,7 @@ lemma prime.factors_pow {p : ℕ} (hp : p.prime) (n : ℕ) :
 begin
   symmetry,
   rw ← list.replicate_perm,
-  apply nat.factors_unique (list.prod_replicate p n),
+  apply nat.factors_unique (list.prod_replicate n p),
   intros q hq,
   rwa eq_of_mem_replicate hq,
 end
@@ -168,7 +168,7 @@ lemma eq_prime_pow_of_unique_prime_dvd {n p : ℕ} (hpos : n ≠ 0)
   n = p ^ n.factors.length :=
 begin
   set k := n.factors.length,
-  rw [←prod_factors hpos, ←prod_replicate p k,
+  rw [← prod_factors hpos, ← prod_replicate k p,
     eq_replicate_of_mem (λ d hd, h (prime_of_mem_factors hd) (dvd_of_mem_factors hd))],
 end
 
diff --git a/src/data/polynomial/ring_division.lean b/src/data/polynomial/ring_division.lean
@@ -617,9 +617,9 @@ end
   (s.map (λ a, X - C a)).prod.nat_degree = s.card :=
 begin
   rw [nat_degree_multiset_prod_of_monic, multiset.map_map],
-  { convert multiset.sum_replicate 1 _,
-    { convert multiset.map_const _ 1, ext, apply nat_degree_X_sub_C }, { simp } },
-  { intros f hf, obtain ⟨a, ha, rfl⟩ := multiset.mem_map.1 hf, exact monic_X_sub_C a },
+  { simp only [(∘), nat_degree_X_sub_C, multiset.map_const, multiset.sum_replicate, smul_eq_mul,
+      mul_one] },
+  { exact multiset.forall_mem_map_iff.2 (λ a _, monic_X_sub_C a) },
 end
 
 lemma card_roots_X_pow_sub_C {n : ℕ} (hn : 0 < n) (a : R) :
diff --git a/src/group_theory/perm/cycle/type.lean b/src/group_theory/perm/cycle/type.lean
@@ -482,7 +482,7 @@ begin
   λ k v, nat.rec (hf1 v).symm (λ k hk, eq.trans (by exact congr_arg σ hk) (hf2 k 1 v)) k,
   replace hσ : σ ^ (p ^ 1) = 1 := perm.ext (λ v, by rw [pow_one, hσ, hf3, one_apply]),
   let v₀ : vectors_prod_eq_one G p :=
-    ⟨vector.replicate p 1, (list.prod_replicate 1 p).trans (one_pow p)⟩,
+    ⟨vector.replicate p 1, (list.prod_replicate p 1).trans (one_pow p)⟩,
   have hv₀ : σ v₀ = v₀ := subtype.ext (subtype.ext (list.rotate_replicate (1 : G) p 1)),
   obtain ⟨v, hv1, hv2⟩ := exists_fixed_point_of_prime' Scard hσ hv₀,
   refine exists_imp_exists (λ g hg, order_of_eq_prime _ (λ hg', hv2 _))
