chore(algebra/big_operators/basic): rename sum_(nat/int)_cast and (na…

…t/int).coe_prod (#8264)

The current names aren't great because
1. For `sum_nat_cast` and `sum_int_cast`, the LHS isn't a sum of casts but a cast of sums, and it doesn't follow any other naming convention (`nat.cast_...` or `....coe_sum`).
2. For `.coe_prod`, the coercion from `ℕ` or `ℤ` should be called `cast`.

archive/100-theorems-list/83_friendship_graphs.lean

@@ -85,7 +85,7 @@ end
 lemma adj_matrix_pow_three_of_not_adj {v w : V} (non_adj : ¬ G.adj v w) :
   ((G.adj_matrix R) ^ 3) v w = degree G v :=
 begin
-  rw [pow_succ, mul_eq_mul, adj_matrix_mul_apply, degree, card_eq_sum_ones, sum_nat_cast],
+  rw [pow_succ, mul_eq_mul, adj_matrix_mul_apply, degree, card_eq_sum_ones, nat.cast_sum],
   apply sum_congr rfl,
   intros x hx,
   rw [adj_matrix_sq_of_ne _ hG, nat.cast_one],

src/algebra/big_operators/basic.lean

@@ -1145,16 +1145,6 @@ lemma sum_boole {s : finset α} {p : α → Prop} [non_assoc_semiring β] {hp :
   (∑ x in s, if p x then (1 : β) else (0 : β)) = (s.filter p).card :=
 by simp [sum_ite]
 
-@[norm_cast]
-lemma sum_nat_cast [add_comm_monoid β] [has_one β] (s : finset α) (f : α → ℕ) :
-  ↑(∑ x in s, f x : ℕ) = (∑ x in s, (f x : β)) :=
-(nat.cast_add_monoid_hom β).map_sum f s
-
-@[norm_cast]
-lemma sum_int_cast [add_comm_group β] [has_one β] (s : finset α) (f : α → ℤ) :
-  ↑(∑ x in s, f x : ℤ) = (∑ x in s, (f x : β)) :=
-(int.cast_add_hom β).map_sum f s
-
 lemma sum_comp [add_comm_monoid β] [decidable_eq γ] {s : finset α} (f : γ → β) (g : α → γ) :
   ∑ a in s, f (g a) = ∑ b in s.image g, (s.filter (λ a, g a = b)).card • (f b) :=
 @prod_comp (multiplicative β) _ _ _ _ _ _ _
@@ -1406,16 +1396,24 @@ end
 
 end multiset
 
-@[simp, norm_cast] lemma nat.coe_prod {R : Type*} [comm_semiring R]
-  (f : α → ℕ) (s : finset α) : (↑∏ i in s, f i : R) = ∏ i in s, f i :=
+@[simp, norm_cast] lemma nat.cast_sum [add_comm_monoid β] [has_one β] (s : finset α) (f : α → ℕ) :
+  ↑(∑ x in s, f x : ℕ) = (∑ x in s, (f x : β)) :=
+(nat.cast_add_monoid_hom β).map_sum f s
+
+@[simp, norm_cast] lemma int.cast_sum [add_comm_group β] [has_one β] (s : finset α) (f : α → ℤ) :
+  ↑(∑ x in s, f x : ℤ) = (∑ x in s, (f x : β)) :=
+(int.cast_add_hom β).map_sum f s
+
+@[simp, norm_cast] lemma nat.cast_prod {R : Type*} [comm_semiring R] (f : α → ℕ) (s : finset α) :
+  (↑∏ i in s, f i : R) = ∏ i in s, f i :=
 (nat.cast_ring_hom R).map_prod _ _
 
-@[simp, norm_cast] lemma int.coe_prod {R : Type*} [comm_ring R]
-  (f : α → ℤ) (s : finset α) : (↑∏ i in s, f i : R) = ∏ i in s, f i :=
+@[simp, norm_cast] lemma int.cast_prod {R : Type*} [comm_ring R] (f : α → ℤ) (s : finset α) :
+  (↑∏ i in s, f i : R) = ∏ i in s, f i :=
 (int.cast_ring_hom R).map_prod _ _
 
-@[simp, norm_cast] lemma units.coe_prod {M : Type*} [comm_monoid M]
-  (f : α → units M) (s : finset α) : (↑∏ i in s, f i : M) = ∏ i in s, f i :=
+@[simp, norm_cast] lemma units.coe_prod {M : Type*} [comm_monoid M] (f : α → units M)
+  (s : finset α) : (↑∏ i in s, f i : M) = ∏ i in s, f i :=
 (units.coe_hom M).map_prod _ _
 
 lemma nat_abs_sum_le {ι : Type*} (s : finset ι) (f : ι → ℤ) :
@@ -1428,4 +1426,3 @@ begin
     simp only [his, finset.sum_insert, not_false_iff],
     exact (int.nat_abs_add_le _ _).trans (add_le_add le_rfl IH) }
 end
-

src/combinatorics/simple_graph/degree_sum.lean

@@ -183,7 +183,7 @@ begin
   classical,
   have h := congr_arg ((λ n, ↑n) : ℕ → zmod 2) G.sum_degrees_eq_twice_card_edges,
   simp only [zmod.nat_cast_self, zero_mul, nat.cast_mul] at h,
-  rw [sum_nat_cast, ←sum_filter_ne_zero] at h,
+  rw [nat.cast_sum, ←sum_filter_ne_zero] at h,
   rw @sum_congr _ _ _ _ (λ v, (G.degree v : zmod 2)) (λ v, (1 : zmod 2)) _ rfl at h,
   { simp only [filter_congr_decidable, mul_one, nsmul_eq_mul, sum_const, ne.def] at h,
     rw ←zmod.eq_zero_iff_even,

src/field_theory/chevalley_warning.lean

@@ -125,7 +125,7 @@ begin
       rw [pow_card_sub_one_eq_one (eval x (f i)) hx, sub_self], } },
   -- In particular, we can now show:
   have key : ∑ x, eval x F = fintype.card {x : σ → K // ∀ i ∈ s, eval x (f i) = 0},
-  rw [fintype.card_of_subtype S hS, card_eq_sum_ones, sum_nat_cast, nat.cast_one,
+  rw [fintype.card_of_subtype S hS, card_eq_sum_ones, nat.cast_sum, nat.cast_one,
       ← fintype.sum_extend_by_zero S, sum_congr rfl (λ x hx, hF x)],
   -- With these preparations under our belt, we will approach the main goal.
   show p ∣ fintype.card {x // ∀ (i : ι), i ∈ s → eval x (f i) = 0},

src/group_theory/sylow.lean

@@ -67,7 +67,7 @@ calc card α = card (Σ y : quotient (orbit_rel G α), {x // quotient.mk' x = y}
 ... = ∑ a : quotient (orbit_rel G α), card {x // quotient.mk' x = a} : card_sigma _
 ... ≡ ∑ a : fixed_points G α, 1 [MOD p] :
 begin
-  rw [← zmod.eq_iff_modeq_nat p, sum_nat_cast, sum_nat_cast],
+  rw [←zmod.eq_iff_modeq_nat p, nat.cast_sum, nat.cast_sum],
   refine eq.symm (sum_bij_ne_zero (λ a _ _, quotient.mk' a.1)
     (λ _ _ _, mem_univ _)
     (λ a₁ a₂ _ _ _ _ h,

src/linear_algebra/matrix/determinant.lean

@@ -485,7 +485,7 @@ begin
     simp only [prod_congr_left_apply] },
   { intros σ _,
     rw [finset.prod_mul_distrib, ←finset.univ_product_univ, finset.prod_product, finset.prod_comm],
-    simp only [sign_prod_congr_left, units.coe_prod, int.coe_prod, block_diagonal_apply_eq,
+    simp only [sign_prod_congr_left, units.coe_prod, int.cast_prod, block_diagonal_apply_eq,
       prod_congr_left_apply] },
   { intros σ σ' _ _ eq,
     ext x hx k,

src/measure_theory/probability_mass_function.lean

@@ -249,7 +249,7 @@ def seq (f : pmf (α → β)) (p : pmf α) : pmf β := f.bind (λ m, p.bind $ λ
 def of_multiset (s : multiset α) (hs : s ≠ 0) : pmf α :=
 ⟨λ a, s.count a / s.card,
   have ∑ a in s.to_finset, (s.count a : ℝ) / s.card = 1,
-    by simp [div_eq_inv_mul, finset.mul_sum.symm, (finset.sum_nat_cast _ _).symm, hs],
+    by simp [div_eq_inv_mul, finset.mul_sum.symm, (nat.cast_sum _ _).symm, hs],
   have ∑ a in s.to_finset, (s.count a : ℝ≥0) / s.card = 1,
     by rw [← nnreal.eq_iff, nnreal.coe_one, ← this, nnreal.coe_sum]; simp,
   begin

src/number_theory/arithmetic_function.lean

@@ -735,7 +735,7 @@ begin
       int.cast_one, sum_singleton, coe_mul_zeta_apply, one_one, int_coe_apply, pow_zero] },
   rw [coe_mul_zeta_apply, one_apply_ne (ne_of_gt (succ_lt_succ (nat.succ_pos _)))],
   simp_rw [int_coe_apply],
-  rw [← finset.sum_int_cast, ← sum_filter_ne_zero],
+  rw [←int.cast_sum, ← sum_filter_ne_zero],
   convert int.cast_zero,
   simp only [moebius_ne_zero_iff_squarefree],
   suffices :

src/number_theory/quadratic_reciprocity.lean

@@ -234,21 +234,21 @@ calc ((∑ x in Ico 1 (p / 2).succ, a * x : ℕ) : zmod 2)
 ... = (∑ x in Ico 1 (p / 2).succ, ((a * x : ℕ) : zmod p).val : ℕ) +
     (∑ x in Ico 1 (p / 2).succ, (a * x) / p : ℕ) :
   by simp only [val_nat_cast];
-    simp [sum_add_distrib, mul_sum.symm, nat.cast_add, nat.cast_mul, sum_nat_cast, hp2]
+    simp [sum_add_distrib, mul_sum.symm, nat.cast_add, nat.cast_mul, nat.cast_sum, hp2]
 ... = _ : congr_arg2 (+)
   (calc ((∑ x in Ico 1 (p / 2).succ, ((a * x : ℕ) : zmod p).val : ℕ) : zmod 2)
       = ∑ x in Ico 1 (p / 2).succ,
           ((((a * x : zmod p).val_min_abs +
             (if (a * x : zmod p).val ≤ p / 2 then 0 else p)) : ℤ) : zmod 2) :
-        by simp only [(val_eq_ite_val_min_abs _).symm]; simp [sum_nat_cast]
+        by simp only [(val_eq_ite_val_min_abs _).symm]; simp [nat.cast_sum]
   ... = ((Ico 1 (p / 2).succ).filter
         (λ x : ℕ, p / 2 < (a * x : zmod p).val)).card +
       ((∑ x in Ico 1 (p / 2).succ, (a * x : zmod p).val_min_abs.nat_abs) : ℕ) :
-    by { simp [ite_cast, add_comm, sum_add_distrib, finset.sum_ite, hp2, sum_nat_cast], }
+    by { simp [ite_cast, add_comm, sum_add_distrib, finset.sum_ite, hp2, nat.cast_sum], }
   ... = _ : by rw [finset.sum_eq_multiset_sum,
       Ico_map_val_min_abs_nat_abs_eq_Ico_map_id p a hap,
       ← finset.sum_eq_multiset_sum];
-    simp [sum_nat_cast]) rfl
+    simp [nat.cast_sum]) rfl
 
 private lemma eisenstein_lemma_aux₂ (p : ℕ) [fact p.prime] [fact (p % 2 = 1)]
   {a : ℕ} (ha2 : a % 2 = 1) (hap : (a : zmod p) ≠ 0) :
@@ -257,7 +257,7 @@ private lemma eisenstein_lemma_aux₂ (p : ℕ) [fact p.prime] [fact (p % 2 = 1)
   ≡ ∑ x in Ico 1 (p / 2).succ, (x * a) / p [MOD 2] :=
 have ha2 : (a : zmod 2) = (1 : ℕ), from (eq_iff_modeq_nat _).2 ha2,
 (eq_iff_modeq_nat 2).1 $ sub_eq_zero.1 $
-  by simpa [add_left_comm, sub_eq_add_neg, finset.mul_sum.symm, mul_comm, ha2, sum_nat_cast,
+  by simpa [add_left_comm, sub_eq_add_neg, finset.mul_sum.symm, mul_comm, ha2, nat.cast_sum,
             add_neg_eq_iff_eq_add.symm, neg_eq_self_mod_two, add_assoc]
     using eq.symm (eisenstein_lemma_aux₁ p hap)