bump to nightly-2023-06-10-07

mathlib commit leanprover-community/mathlib@a3e83f0

Archive/100-theorems-list/42InverseTriangleSum.lean

@@ -31,7 +31,7 @@ open Finset
 
 /-- **Sum of the Reciprocals of the Triangular Numbers** -/
 theorem Theorem100.inverse_triangle_sum :
-    ∀ n, (∑ k in range n, (2 : ℚ) / (k * (k + 1))) = if n = 0 then 0 else 2 - (2 : ℚ) / n :=
+    ∀ n, ∑ k in range n, (2 : ℚ) / (k * (k + 1)) = if n = 0 then 0 else 2 - (2 : ℚ) / n :=
   by
   refine' sum_range_induction _ _ (if_pos rfl) _
   rintro (_ | n); · rw [if_neg, if_pos] <;> norm_num

Archive/100-theorems-list/45Partition.lean

@@ -92,7 +92,7 @@ It is stated for an arbitrary commutative semiring `α`, though it usually suffi
 or `ℝ`.
 -/
 def partialDistinctGf (m : ℕ) [CommSemiring α] :=
-  ∏ i in range m, 1 + (X : PowerSeries α) ^ (i + 1)
+  ∏ i in range m, (1 + (X : PowerSeries α) ^ (i + 1))
 #align theorems_100.partial_distinct_gf Theorems100.partialDistinctGf
 
 /--
@@ -511,26 +511,26 @@ theorem same_gf [Field α] (m : ℕ) :
   induction' m with m ih
   · simp
   rw [Nat.succ_eq_add_one]
-  set π₀ : PowerSeries α := ∏ i in range m, 1 - X ^ (m + 1 + i + 1) with hπ₀
+  set π₀ : PowerSeries α := ∏ i in range m, (1 - X ^ (m + 1 + i + 1)) with hπ₀
   set π₁ : PowerSeries α := ∏ i in range m, (1 - X ^ (2 * i + 1))⁻¹ with hπ₁
-  set π₂ : PowerSeries α := ∏ i in range m, 1 - X ^ (m + i + 1) with hπ₂
-  set π₃ : PowerSeries α := ∏ i in range m, 1 + X ^ (i + 1) with hπ₃
+  set π₂ : PowerSeries α := ∏ i in range m, (1 - X ^ (m + i + 1)) with hπ₂
+  set π₃ : PowerSeries α := ∏ i in range m, (1 + X ^ (i + 1)) with hπ₃
   rw [← hπ₃] at ih 
   have h : constant_coeff α (1 - X ^ (2 * m + 1)) ≠ 0 :=
     by
     rw [RingHom.map_sub, RingHom.map_pow, constant_coeff_one, constant_coeff_X,
       zero_pow (2 * m).succ_pos, sub_zero]
     exact one_ne_zero
   calc
-    ((∏ i in range (m + 1), (1 - X ^ (2 * i + 1))⁻¹) *
-          ∏ i in range (m + 1), 1 - X ^ (m + 1 + i + 1)) =
+    (∏ i in range (m + 1), (1 - X ^ (2 * i + 1))⁻¹) *
+          ∏ i in range (m + 1), (1 - X ^ (m + 1 + i + 1)) =
         π₁ * (1 - X ^ (2 * m + 1))⁻¹ * (π₀ * (1 - X ^ (m + 1 + m + 1))) :=
       by rw [prod_range_succ _ m, ← hπ₁, prod_range_succ _ m, ← hπ₀]
     _ = π₁ * (1 - X ^ (2 * m + 1))⁻¹ * (π₀ * ((1 + X ^ (m + 1)) * (1 - X ^ (m + 1)))) := by
       rw [← sq_sub_sq, one_pow, add_assoc _ m 1, ← two_mul (m + 1), pow_mul']
     _ = π₀ * (1 - X ^ (m + 1)) * (1 - X ^ (2 * m + 1))⁻¹ * (π₁ * (1 + X ^ (m + 1))) := by ring
     _ =
-        (∏ i in range (m + 1), 1 - X ^ (m + 1 + i)) * (1 - X ^ (2 * m + 1))⁻¹ *
+        (∏ i in range (m + 1), (1 - X ^ (m + 1 + i))) * (1 - X ^ (2 * m + 1))⁻¹ *
           (π₁ * (1 + X ^ (m + 1))) :=
       by rw [prod_range_succ', add_zero, hπ₀]; simp_rw [← add_assoc]
     _ = π₂ * (1 - X ^ (m + 1 + m)) * (1 - X ^ (2 * m + 1))⁻¹ * (π₁ * (1 + X ^ (m + 1))) := by

Archive/100-theorems-list/81SumOfPrimeReciprocalsDiverges.lean

@@ -80,7 +80,7 @@ is less than 1/2.
 -/
 theorem sum_lt_half_of_not_tendsto
     (h : ¬Tendsto (fun n => ∑ p in {p ∈ range n | Nat.Prime p}, 1 / (p : ℝ)) atTop atTop) :
-    ∃ k, ∀ x, (∑ p in p x k, 1 / (p : ℝ)) < 1 / 2 :=
+    ∃ k, ∀ x, ∑ p in p x k, 1 / (p : ℝ) < 1 / 2 :=
   by
   have h0 :
     (fun n => ∑ p in {p ∈ range n | Nat.Prime p}, 1 / (p : ℝ)) = fun n =>

Archive/100-theorems-list/9AreaOfACircle.lean

@@ -91,7 +91,7 @@ theorem area_disc : volume (disc r) = NNReal.pi * r ^ 2 :=
   let f x := sqrt (r ^ 2 - x ^ 2)
   let F x := (r : ℝ) ^ 2 * arcsin (r⁻¹ * x) + x * sqrt (r ^ 2 - x ^ 2)
   have hf : Continuous f := by continuity
-  suffices (∫ x in -r..r, 2 * f x) = NNReal.pi * r ^ 2
+  suffices ∫ x in -r..r, 2 * f x = NNReal.pi * r ^ 2
     by
     have h : integrable_on f (Ioc (-r) r) := hf.integrable_on_Icc.mono_set Ioc_subset_Icc_self
     calc
@@ -130,7 +130,7 @@ theorem area_disc : volume (disc r) = NNReal.pi * r ^ 2 :=
     · nlinarith
   have hcont := (by continuity : Continuous F).ContinuousOn
   calc
-    (∫ x in -r..r, 2 * f x) = F r - F (-r) :=
+    ∫ x in -r..r, 2 * f x = F r - F (-r) :=
       integral_eq_sub_of_has_deriv_at_of_le (neg_le_self r.2) hcont hderiv
         (continuous_const.mul hf).ContinuousOn.IntervalIntegrable
     _ = NNReal.pi * r ^ 2 := by norm_num [F, inv_mul_cancel hlt.ne', ← mul_div_assoc, mul_comm π]

Archive/Imo/Imo1975Q1.lean

@@ -41,11 +41,11 @@ variable (hy : AntitoneOn y (Finset.Icc 1 n))
 include hx hy hσ
 
 theorem imo1975_q1 :
-    (∑ i in Finset.Icc 1 n, (x i - y i) ^ 2) ≤ ∑ i in Finset.Icc 1 n, (x i - y (σ i)) ^ 2 :=
+    ∑ i in Finset.Icc 1 n, (x i - y i) ^ 2 ≤ ∑ i in Finset.Icc 1 n, (x i - y (σ i)) ^ 2 :=
   by
   simp only [sub_sq, Finset.sum_add_distrib, Finset.sum_sub_distrib]
   -- a finite sum is invariant if we permute the order of summation
-  have hσy : (∑ i : ℕ in Finset.Icc 1 n, y i ^ 2) = ∑ i : ℕ in Finset.Icc 1 n, y (σ i) ^ 2 := by
+  have hσy : ∑ i : ℕ in Finset.Icc 1 n, y i ^ 2 = ∑ i : ℕ in Finset.Icc 1 n, y (σ i) ^ 2 := by
     rw [← Equiv.Perm.sum_comp σ (Finset.Icc 1 n) _ hσ]
   -- let's cancel terms appearing on both sides
   norm_num [hσy, mul_assoc, ← Finset.mul_sum]

Archive/Imo/Imo1987Q1.lean

@@ -96,20 +96,20 @@ def fixedPointsEquiv' :
 #align imo1987_q1.fixed_points_equiv' Imo1987Q1.fixedPointsEquiv'
 
 /-- Main statement for any `(α : Type*) [fintype α]`. -/
-theorem main_fintype : (∑ k in range (card α + 1), k * p α k) = card α * (card α - 1)! :=
+theorem main_fintype : ∑ k in range (card α + 1), k * p α k = card α * (card α - 1)! :=
   by
   have A : ∀ (k) (σ : fiber α k), card (fixedPoints ⇑(↑σ : Perm α)) = k := fun k σ => σ.2
   simpa [A, ← Fin.sum_univ_eq_sum_range, -card_of_finset, Finset.card_univ, card_fixed_points,
     mul_comm] using card_congr (fixed_points_equiv' α)
 #align imo1987_q1.main_fintype Imo1987Q1.main_fintype
 
 /-- Main statement for permutations of `fin n`, a version that works for `n = 0`. -/
-theorem main₀ (n : ℕ) : (∑ k in range (n + 1), k * p (Fin n) k) = n * (n - 1)! := by
+theorem main₀ (n : ℕ) : ∑ k in range (n + 1), k * p (Fin n) k = n * (n - 1)! := by
   simpa using main_fintype (Fin n)
 #align imo1987_q1.main₀ Imo1987Q1.main₀
 
 /-- Main statement for permutations of `fin n`. -/
-theorem main {n : ℕ} (hn : 1 ≤ n) : (∑ k in range (n + 1), k * p (Fin n) k) = n ! := by
+theorem main {n : ℕ} (hn : 1 ≤ n) : ∑ k in range (n + 1), k * p (Fin n) k = n ! := by
   rw [main₀, Nat.mul_factorial_pred (zero_lt_one.trans_le hn)]
 #align imo1987_q1.main Imo1987Q1.main
 

Archive/Imo/Imo1994Q1.lean

@@ -67,18 +67,18 @@ theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : Finset ℕ) (hm : A.card = m + 1)
   set rev := Equiv.subLeft (Fin.last m)
   -- `i ↦ m-i`
   -- We reindex the sum by fin (m+1)
-  have : (∑ x in A, x) = ∑ i : Fin (m + 1), a i :=
+  have : ∑ x in A, x = ∑ i : Fin (m + 1), a i :=
     by
     convert sum_image fun x hx y hy => (OrderEmbedding.eq_iff_eq a).1
     rw [← coe_inj]; simp
   rw [this]; clear this
   -- The main proof is a simple calculation by rearranging one of the two sums
   suffices hpair : ∀ k ∈ univ, a k + a (rev k) ≥ n + 1
   calc
-    (2 * ∑ i : Fin (m + 1), a i) = (∑ i : Fin (m + 1), a i) + ∑ i : Fin (m + 1), a i := two_mul _
-    _ = (∑ i : Fin (m + 1), a i) + ∑ i : Fin (m + 1), a (rev i) := by rw [Equiv.sum_comp rev]
-    _ = ∑ i : Fin (m + 1), a i + a (rev i) := sum_add_distrib.symm
-    _ ≥ ∑ i : Fin (m + 1), n + 1 := (sum_le_sum hpair)
+    2 * ∑ i : Fin (m + 1), a i = ∑ i : Fin (m + 1), a i + ∑ i : Fin (m + 1), a i := two_mul _
+    _ = ∑ i : Fin (m + 1), a i + ∑ i : Fin (m + 1), a (rev i) := by rw [Equiv.sum_comp rev]
+    _ = ∑ i : Fin (m + 1), (a i + a (rev i)) := sum_add_distrib.symm
+    _ ≥ ∑ i : Fin (m + 1), (n + 1) := (sum_le_sum hpair)
     _ = (m + 1) * (n + 1) := by rw [sum_const, card_fin, Nat.nsmul_eq_mul]
   -- It remains to prove the key inequality, by contradiction
   rintro k -

Archive/Imo/Imo2013Q1.lean

@@ -43,8 +43,8 @@ theorem arith_lemma (k n : ℕ) : 0 < 2 * n + 2 ^ k.succ :=
 #align imo2013_q1.arith_lemma Imo2013Q1.arith_lemma
 
 theorem prod_lemma (m : ℕ → ℕ+) (k : ℕ) (nm : ℕ+) :
-    (∏ i : ℕ in Finset.range k, (1 : ℚ) + 1 / ↑(if i < k then m i else nm)) =
-      ∏ i : ℕ in Finset.range k, 1 + 1 / m i :=
+    ∏ i : ℕ in Finset.range k, ((1 : ℚ) + 1 / ↑(if i < k then m i else nm)) =
+      ∏ i : ℕ in Finset.range k, (1 + 1 / m i) :=
   by
   suffices : ∀ i, i ∈ Finset.range k → (1 : ℚ) + 1 / ↑(if i < k then m i else nm) = 1 + 1 / m i
   exact Finset.prod_congr rfl this
@@ -57,7 +57,7 @@ end imo2013_q1
 open imo2013_q1
 
 theorem imo2013_q1 (n : ℕ+) (k : ℕ) :
-    ∃ m : ℕ → ℕ+, (1 : ℚ) + (2 ^ k - 1) / n = ∏ i in Finset.range k, 1 + 1 / m i :=
+    ∃ m : ℕ → ℕ+, (1 : ℚ) + (2 ^ k - 1) / n = ∏ i in Finset.range k, (1 + 1 / m i) :=
   by
   revert n
   induction' k with pk hpk
@@ -87,9 +87,9 @@ theorem imo2013_q1 (n : ℕ+) (k : ℕ) :
         field_simp [t.cast_add_one_ne_zero]
         ring
       _ = (1 + 1 / (2 * t + 2 ^ pk.succ)) * (1 + (2 ^ pk - 1) / t_succ) := by norm_cast
-      _ = (∏ i in Finset.range pk, 1 + 1 / m i) * (1 + 1 / m pk) := by
+      _ = (∏ i in Finset.range pk, (1 + 1 / m i)) * (1 + 1 / m pk) := by
         rw [prod_lemma, hpm, ← hmpk, mul_comm]
-      _ = ∏ i in Finset.range pk.succ, 1 + 1 / m i := by rw [← Finset.prod_range_succ _ pk]
+      _ = ∏ i in Finset.range pk.succ, (1 + 1 / m i) := by rw [← Finset.prod_range_succ _ pk]
   · -- odd case
     let t_succ : ℕ+ := ⟨t + 1, t.succ_pos⟩
     obtain ⟨pm, hpm⟩ := hpk t_succ
@@ -106,8 +106,8 @@ theorem imo2013_q1 (n : ℕ+) (k : ℕ) :
         field_simp [t.cast_add_one_ne_zero]
         ring
       _ = (1 + 1 / (2 * t + 1)) * (1 + (2 ^ pk - 1) / t_succ) := by norm_cast
-      _ = (∏ i in Finset.range pk, 1 + 1 / m i) * (1 + 1 / ↑(m pk)) := by
+      _ = (∏ i in Finset.range pk, (1 + 1 / m i)) * (1 + 1 / ↑(m pk)) := by
         rw [prod_lemma, hpm, ← hmpk, mul_comm]
-      _ = ∏ i in Finset.range pk.succ, 1 + 1 / m i := by rw [← Finset.prod_range_succ _ pk]
+      _ = ∏ i in Finset.range pk.succ, (1 + 1 / m i) := by rw [← Finset.prod_range_succ _ pk]
 #align imo2013_q1 imo2013_q1
 

Archive/Imo/Imo2019Q4.lean

@@ -37,7 +37,7 @@ open Nat hiding zero_le Prime
 
 namespace imo2019_q4
 
-theorem upper_bound {k n : ℕ} (hk : k > 0) (h : (k ! : ℤ) = ∏ i in range n, 2 ^ n - 2 ^ i) :
+theorem upper_bound {k n : ℕ} (hk : k > 0) (h : (k ! : ℤ) = ∏ i in range n, (2 ^ n - 2 ^ i)) :
     n < 6 := by
   have prime_2 : Prime (2 : ℤ) := prime_iff_prime_int.mp prime_two
   have h2 : n * (n - 1) / 2 < k :=
@@ -85,7 +85,7 @@ theorem upper_bound {k n : ℕ} (hk : k > 0) (h : (k ! : ℤ) = ∏ i in range n
 end imo2019_q4
 
 theorem imo2019_q4 {k n : ℕ} (hk : k > 0) (hn : n > 0) :
-    ((k ! : ℤ) = ∏ i in range n, 2 ^ n - 2 ^ i) ↔ (k, n) = (1, 1) ∨ (k, n) = (3, 2) :=
+    (k ! : ℤ) = ∏ i in range n, (2 ^ n - 2 ^ i) ↔ (k, n) = (1, 1) ∨ (k, n) = (3, 2) :=
   by
   -- The implication `←` holds.
   constructor;

Archive/OxfordInvariants/2021summer/Week3P1.lean

@@ -92,7 +92,7 @@ theorem OxfordInvariants.week3_p1 (n : ℕ) (a : ℕ → ℕ) (a_pos : ∀ i ≤
     Set up the stronger induction hypothesis -/
   rsuffices ⟨b, hb, -⟩ :
     ∃ b : ℕ,
-      ((b : α) = ∑ i in Finset.range (n + 1), a 0 * a (n + 1) / (a i * a (i + 1))) ∧
+      (b : α) = ∑ i in Finset.range (n + 1), a 0 * a (n + 1) / (a i * a (i + 1)) ∧
         a (n + 1) ∣ a n * b - a 0
   · exact ⟨b, hb⟩
   simp_rw [← @Nat.cast_pos α] at a_pos 

Counterexamples/Phillips.lean

@@ -474,7 +474,7 @@ theorem to_functions_to_measure [MeasurableSpace α] (μ : Measure α) [IsFinite
         (of_normed_add_comm_group_discrete (indicator s 1) 1 (norm_indicator_le_one s)) =
       (μ s).toReal
   rw [extension_to_bounded_functions_apply]
-  · change (∫ x, s.indicator (fun y => (1 : ℝ)) x ∂μ) = _
+  · change ∫ x, s.indicator (fun y => (1 : ℝ)) x ∂μ = _
     simp [integral_indicator hs]
   · change integrable (indicator s 1) μ
     have : integrable (fun x => (1 : ℝ)) μ := integrable_const (1 : ℝ)
@@ -629,7 +629,7 @@ theorem integrable_comp (Hcont : (#ℝ) = aleph 1) (φ : (DiscreteCopy ℝ →
 #align counterexample.phillips_1940.integrable_comp Counterexample.Phillips1940.integrable_comp
 
 theorem integral_comp (Hcont : (#ℝ) = aleph 1) (φ : (DiscreteCopy ℝ →ᵇ ℝ) →L[ℝ] ℝ) :
-    (∫ x in Icc 0 1, φ (f Hcont x)) = φ.toBoundedAdditiveMeasure.continuousPart univ :=
+    ∫ x in Icc 0 1, φ (f Hcont x) = φ.toBoundedAdditiveMeasure.continuousPart univ :=
   by
   rw [← integral_congr_ae (comp_ae_eq_const Hcont φ)]
   simp
@@ -661,7 +661,7 @@ theorem norm_bound (Hcont : (#ℝ) = aleph 1) (x : ℝ) : ‖f Hcont x‖ ≤ 1
 /-- The function `f Hcont : ℝ → (discrete_copy ℝ →ᵇ ℝ)` has no Pettis integral. -/
 theorem no_pettis_integral (Hcont : (#ℝ) = aleph 1) :
     ¬∃ g : DiscreteCopy ℝ →ᵇ ℝ,
-        ∀ φ : (DiscreteCopy ℝ →ᵇ ℝ) →L[ℝ] ℝ, (∫ x in Icc 0 1, φ (f Hcont x)) = φ g :=
+        ∀ φ : (DiscreteCopy ℝ →ᵇ ℝ) →L[ℝ] ℝ, ∫ x in Icc 0 1, φ (f Hcont x) = φ g :=
   by
   rintro ⟨g, h⟩
   simp only [integral_comp] at h 

Mathbin/Algebra/Algebra/Operations.lean

@@ -634,7 +634,7 @@ instance : IdemCommSemiring (Submodule R A) :=
   { Submodule.idemSemiring with mul_comm := Submodule.mul_comm }
 
 theorem prod_span {ι : Type _} (s : Finset ι) (M : ι → Set A) :
-    (∏ i in s, Submodule.span R (M i)) = Submodule.span R (∏ i in s, M i) :=
+    ∏ i in s, Submodule.span R (M i) = Submodule.span R (∏ i in s, M i) :=
   by
   letI := Classical.decEq ι
   refine' Finset.induction_on s _ _
@@ -644,7 +644,7 @@ theorem prod_span {ι : Type _} (s : Finset ι) (M : ι → Set A) :
 #align submodule.prod_span Submodule.prod_span
 
 theorem prod_span_singleton {ι : Type _} (s : Finset ι) (x : ι → A) :
-    (∏ i in s, span R ({x i} : Set A)) = span R {∏ i in s, x i} := by
+    ∏ i in s, span R ({x i} : Set A) = span R {∏ i in s, x i} := by
   rw [prod_span, Set.finset_prod_singleton]
 #align submodule.prod_span_singleton Submodule.prod_span_singleton
 

Mathbin/Algebra/Algebra/Subalgebra/Basic.lean

@@ -180,7 +180,7 @@ protected theorem multiset_sum_mem {m : Multiset A} (h : ∀ x ∈ m, x ∈ S) :
 #align subalgebra.multiset_sum_mem Subalgebra.multiset_sum_mem
 
 protected theorem sum_mem {ι : Type w} {t : Finset ι} {f : ι → A} (h : ∀ x ∈ t, f x ∈ S) :
-    (∑ x in t, f x) ∈ S :=
+    ∑ x in t, f x ∈ S :=
   sum_mem h
 #align subalgebra.sum_mem Subalgebra.sum_mem
 
@@ -191,7 +191,7 @@ protected theorem multiset_prod_mem {R : Type u} {A : Type v} [CommSemiring R] [
 
 protected theorem prod_mem {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A]
     (S : Subalgebra R A) {ι : Type w} {t : Finset ι} {f : ι → A} (h : ∀ x ∈ t, f x ∈ S) :
-    (∏ x in t, f x) ∈ S :=
+    ∏ x in t, f x ∈ S :=
   prod_mem h
 #align subalgebra.prod_mem Subalgebra.prod_mem
 
@@ -1490,7 +1490,7 @@ end Centralizer
 `r ^ n • x ∈ M'` for some `n` for each `r : s`. -/
 theorem mem_of_finset_sum_eq_one_of_pow_smul_mem {S : Type _} [CommRing S] [Algebra R S]
     (S' : Subalgebra R S) {ι : Type _} (ι' : Finset ι) (s : ι → S) (l : ι → S)
-    (e : (∑ i in ι', l i * s i) = 1) (hs : ∀ i, s i ∈ S') (hl : ∀ i, l i ∈ S') (x : S)
+    (e : ∑ i in ι', l i * s i = 1) (hs : ∀ i, s i ∈ S') (hl : ∀ i, l i ∈ S') (x : S)
     (H : ∀ i, ∃ n : ℕ, (s i ^ n : S) • x ∈ S') : x ∈ S' := by
   classical
   suffices x ∈ (Algebra.ofId S' S).range.toSubmodule by obtain ⟨x, rfl⟩ := this; exact x.2

Mathbin/Algebra/BigOperators/Associated.lean

@@ -99,7 +99,7 @@ theorem Multiset.prod_primes_dvd [CancelCommMonoidWithZero α]
 
 #print Finset.prod_primes_dvd /-
 theorem Finset.prod_primes_dvd [CancelCommMonoidWithZero α] [Unique αˣ] {s : Finset α} (n : α)
-    (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) : (∏ p in s, p) ∣ n := by
+    (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) : ∏ p in s, p ∣ n := by
   classical exact
     Multiset.prod_primes_dvd n (by simpa only [Multiset.map_id', Finset.mem_def] using h)
       (by simpa only [Multiset.map_id', Finset.mem_def] using div)
@@ -120,7 +120,7 @@ theorem prod_mk {p : Multiset α} : (p.map Associates.mk).Prod = Associates.mk p
 #align associates.prod_mk Associates.prod_mk
 
 theorem finset_prod_mk {p : Finset β} {f : β → α} :
-    (∏ i in p, Associates.mk (f i)) = Associates.mk (∏ i in p, f i) := by
+    ∏ i in p, Associates.mk (f i) = Associates.mk (∏ i in p, f i) := by
   rw [Finset.prod_eq_multiset_prod, ← Multiset.map_map, prod_mk, ← Finset.prod_eq_multiset_prod]
 #align associates.finset_prod_mk Associates.finset_prod_mk