chore: deprecate the ∑ x in s, f x notation (#21253)

Make the `∑ x in s, f x` and `∑ x : ty in s, f x` syntaxes print a code action suggesting to replace to `∑ x ∈ s, f x`. This makes the old syntaxes noisy and therefore unusable in mathlib. Therefore, we must also replace the last few uses of the old syntaxes by the new one.

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -1457,7 +1457,7 @@ injective. Rather, we assume that the image of `f` on `I` only overlaps where `g
 The conclusion is the same as in `sum_image`."]
 lemma prod_image_of_pairwise_eq_one [CommMonoid β] {f : ι → α} {g : α → β} {I : Finset ι}
     (hf : (I : Set ι).Pairwise fun i j ↦ f i = f j → g (f i) = 1) :
-    ∏ s in I.image f, g s = ∏ i in I, g (f i) := by
+    ∏ s ∈ I.image f, g s = ∏ i ∈ I, g (f i) := by
   rw [prod_image']
   exact fun n hnI => (prod_filter_of_pairwise_eq_one hnI hf).symm
 
@@ -1471,7 +1471,7 @@ conclusion is the same as in `sum_image`."
 ]
 lemma prod_image_of_disjoint [CommMonoid β] [PartialOrder α] [OrderBot α] {f : ι → α} {g : α → β}
     (hg_bot : g ⊥ = 1) {I : Finset ι} (hf_disj : (I : Set ι).PairwiseDisjoint f) :
-    ∏ s in I.image f, g s = ∏ i in I, g (f i) := by
+    ∏ s ∈ I.image f, g s = ∏ i ∈ I, g (f i) := by
   refine prod_image_of_pairwise_eq_one <| hf_disj.imp fun i j (hdisj : Disjoint _ _) hfij ↦ ?_
   rw [← hfij, disjoint_self] at hdisj
   rw [hdisj, hg_bot]
@@ -1590,7 +1590,7 @@ theorem prod_toFinset {M : Type*} [DecidableEq α] [CommMonoid M] (f : α → M)
 
 @[simp]
 theorem sum_toFinset_count_eq_length [DecidableEq α] (l : List α) :
-    ∑ a in l.toFinset, l.count a = l.length := by
+    ∑ a ∈ l.toFinset, l.count a = l.length := by
   simpa [List.map_const'] using (Finset.sum_list_map_count l fun _ => (1 : ℕ)).symm
 
 end List
@@ -1603,7 +1603,7 @@ lemma mem_sum {s : Finset ι} {m : ι → Multiset α} : a ∈ ∑ i ∈ s, m i
 
 variable [DecidableEq α]
 
-theorem toFinset_sum_count_eq (s : Multiset α) : ∑ a in s.toFinset, s.count a = card s := by
+theorem toFinset_sum_count_eq (s : Multiset α) : ∑ a ∈ s.toFinset, s.count a = card s := by
   simpa using (Finset.sum_multiset_map_count s (fun _ => (1 : ℕ))).symm
 
 @[simp] lemma sum_count_eq_card {s : Finset α} {m : Multiset α} (hms : ∀ a ∈ m, a ∈ s) :

Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean

@@ -194,21 +194,36 @@ macro_rules (kind := bigprod)
     | some p => `(Finset.prod (Finset.filter (fun $x ↦ $p) $s) (fun $x ↦ $v))
     | none => `(Finset.prod $s (fun $x ↦ $v))
 
-/-- (Deprecated, use `∑ x ∈ s, f x`)
-`∑ x in s, f x` is notation for `Finset.sum s f`. It is the sum of `f x`,
-where `x` ranges over the finite set `s`. -/
+section deprecated -- since 2024-30-01
+open Elab Term Tactic TryThis
+
+/-- Deprecated, use `∑ x ∈ s, f x` instead. -/
 syntax (name := bigsumin) "∑ " extBinder " in " term ", " term:67 : term
-macro_rules (kind := bigsumin)
-  | `(∑ $x:ident in $s, $r) => `(∑ $x:ident ∈ $s, $r)
-  | `(∑ $x:ident : $t in $s, $r) => `(∑ $x:ident ∈ ($s : Finset $t), $r)
 
-/-- (Deprecated, use `∏ x ∈ s, f x`)
-`∏ x in s, f x` is notation for `Finset.prod s f`. It is the product of `f x`,
-where `x` ranges over the finite set `s`. -/
+/-- Deprecated, use `∏ x ∈ s, f x` instead. -/
 syntax (name := bigprodin) "∏ " extBinder " in " term ", " term:67 : term
-macro_rules (kind := bigprodin)
-  | `(∏ $x:ident in $s, $r) => `(∏ $x:ident ∈ $s, $r)
-  | `(∏ $x:ident : $t in $s, $r) => `(∏ $x:ident ∈ ($s : Finset $t), $r)
+
+elab_rules : term
+  | `(∑%$tk $x:ident in $s, $r) => do
+    addSuggestion tk (← `(∑ $x ∈ $s, $r)) (origSpan? := ← getRef) (header :=
+      "The '∑ x in s, f x' notation is deprecated: please use '∑ x ∈ s, f x' instead:\n")
+    elabTerm (← `(∑ $x:ident ∈ $s, $r)) none
+  | `(∑%$tk $x:ident : $_t in $s, $r) => do
+    addSuggestion tk (← `(∑ $x ∈ $s, $r)) (origSpan? := ← getRef) (header :=
+      "The '∑ x : t in s, f x' notation is deprecated: please use '∑ x ∈ s, f x' instead:\n")
+    elabTerm (← `(∑ $x:ident ∈ $s, $r)) none
+
+elab_rules : term
+  | `(∏%$tk $x:ident in $s, $r) => do
+    addSuggestion tk (← `(∏ $x ∈ $s, $r)) (origSpan? := ← getRef) (header :=
+      "The '∏ x in s, f x' notation is deprecated: please use '∏ x ∈ s, f x' instead:\n")
+    elabTerm (← `(∏ $x:ident ∈ $s, $r)) none
+  | `(∏%$tk $x:ident : $_t in $s, $r) => do
+    addSuggestion tk (← `(∏ $x ∈ $s, $r)) (origSpan? := ← getRef) (header :=
+      "The '∏ x : t in s, f x' notation is deprecated: please use '∏ x ∈ s, f x' instead:\n")
+    elabTerm (← `(∏ $x:ident ∈ $s, $r)) none
+
+end deprecated
 
 open Lean Meta Parser.Term PrettyPrinter.Delaborator SubExpr
 open scoped Batteries.ExtendedBinder
@@ -271,7 +286,7 @@ lemma prod_map_val [CommMonoid β] (s : Finset α) (f : α → β) : (s.1.map f)
   rfl
 
 @[simp]
-theorem sum_multiset_singleton (s : Finset α) : (s.sum fun x => {x}) = s.val := by
+theorem sum_multiset_singleton (s : Finset α) : ∑ a ∈ s, {a} = s.val := by
   simp only [sum_eq_multiset_sum, Multiset.sum_map_singleton]
 
 end Finset

Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean

@@ -17,7 +17,7 @@ This file contains results about two kinds of actions:
 * sums over `DistribSMul`: `r • ∑ x ∈ s, f x = ∑ x ∈ s, r • f x`
 * products over `MulDistribMulAction` (with primed name): `r • ∏ x ∈ s, f x = ∏ x ∈ s, r • f x`
 * products over `SMulCommClass` (with unprimed name):
-  `b ^ s.card • ∏ x in s, f x = ∏ x in s, b • f x`
+  `b ^ s.card • ∏ x ∈ s, f x = ∏ x ∈ s, b • f x`
 
 Note that analogous lemmas for `Module`s like `Finset.sum_smul` appear in other files.
 -/
@@ -114,7 +114,7 @@ namespace Finset
 theorem smul_prod
     [CommMonoid β] [Monoid α] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β]
     (s : Finset β) (b : α) (f : β → β) :
-    b ^ s.card • ∏ x in s, f x = ∏ x in s, b • f x := by
+    b ^ s.card • ∏ x ∈ s, f x = ∏ x ∈ s, b • f x := by
   have : Multiset.map (fun (x : β) ↦ b • f x) s.val =
       Multiset.map (fun x ↦ b • x) (Multiset.map f s.val) := by
     simp only [Multiset.map_map, Function.comp_apply]
@@ -123,7 +123,7 @@ theorem smul_prod
 theorem prod_smul
     [CommMonoid β] [CommMonoid α] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β]
     (s : Finset β) (b : β → α) (f : β → β) :
-    ∏ i in s, b i • f i = (∏ i in s, b i) • ∏ i in s, f i := by
+    ∏ i ∈ s, b i • f i = (∏ i ∈ s, b i) • ∏ i ∈ s, f i := by
   induction s using Finset.cons_induction_on with
   | h₁ =>  simp
   | h₂ hj ih => rw [prod_cons, ih, smul_mul_smul_comm, ← prod_cons hj, ← prod_cons hj]

Mathlib/Algebra/BigOperators/Intervals.lean

@@ -136,7 +136,7 @@ theorem prod_Ioc_succ_top {a b : ℕ} (hab : a ≤ b) (f : ℕ → M) :
 
 @[to_additive]
 theorem prod_Icc_succ_top {a b : ℕ} (hab : a ≤ b + 1) (f : ℕ → M) :
-    (∏ k in Icc a (b + 1), f k) = (∏ k in Icc a b, f k) * f (b + 1) := by
+    (∏ k ∈ Icc a (b + 1), f k) = (∏ k ∈ Icc a b, f k) * f (b + 1) := by
   rw [← Nat.Ico_succ_right, prod_Ico_succ_top hab, Nat.Ico_succ_right]
 
 @[to_additive]

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -390,7 +390,7 @@ instance : AddCommGroup (M ⟶ N) :=
     rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
 
 @[simp] lemma hom_sum {ι : Type*} (f : ι → (M ⟶ N)) (s : Finset ι) :
-    (∑ i in s, f i).hom = ∑ i in s, (f i).hom :=
+    (∑ i ∈ s, f i).hom = ∑ i ∈ s, (f i).hom :=
   map_sum ({ toFun := ModuleCat.Hom.hom, map_zero' := ModuleCat.hom_zero, map_add' := hom_add } :
     (M ⟶ N) →+ (M →ₗ[R] N)) _ _
 

Mathlib/Algebra/Group/AddChar.lean

@@ -283,11 +283,11 @@ instance instAddCommMonoid : AddCommMonoid (AddChar A M) := Additive.addCommMono
 @[simp, norm_cast] lemma coe_nsmul (n : ℕ) (ψ : AddChar A M) : ⇑(n • ψ) = ψ ^ n := rfl
 
 @[simp, norm_cast]
-lemma coe_prod (s : Finset ι) (ψ : ι → AddChar A M) : ∏ i in s, ψ i = ∏ i in s, ⇑(ψ i) := by
+lemma coe_prod (s : Finset ι) (ψ : ι → AddChar A M) : ∏ i ∈ s, ψ i = ∏ i ∈ s, ⇑(ψ i) := by
   induction s using Finset.cons_induction <;> simp [*]
 
 @[simp, norm_cast]
-lemma coe_sum (s : Finset ι) (ψ : ι → AddChar A M) : ∑ i in s, ψ i = ∏ i in s, ⇑(ψ i) := by
+lemma coe_sum (s : Finset ι) (ψ : ι → AddChar A M) : ∑ i ∈ s, ψ i = ∏ i ∈ s, ⇑(ψ i) := by
   induction s using Finset.cons_induction <;> simp [*]
 
 @[simp] lemma mul_apply (ψ φ : AddChar A M) (a : A) : (ψ * φ) a = ψ a * φ a := rfl
@@ -296,14 +296,14 @@ lemma coe_sum (s : Finset ι) (ψ : ι → AddChar A M) : ∑ i in s, ψ i = ∏
 @[simp] lemma nsmul_apply (ψ : AddChar A M) (n : ℕ) (a : A) : (n • ψ) a = (ψ a) ^ n := rfl
 
 lemma prod_apply (s : Finset ι) (ψ : ι → AddChar A M) (a : A) :
-    (∏ i in s, ψ i) a = ∏ i in s, ψ i a := by rw [coe_prod, Finset.prod_apply]
+    (∏ i ∈ s, ψ i) a = ∏ i ∈ s, ψ i a := by rw [coe_prod, Finset.prod_apply]
 
 lemma sum_apply (s : Finset ι) (ψ : ι → AddChar A M) (a : A) :
-    (∑ i in s, ψ i) a = ∏ i in s, ψ i a := by rw [coe_sum, Finset.prod_apply]
+    (∑ i ∈ s, ψ i) a = ∏ i ∈ s, ψ i a := by rw [coe_sum, Finset.prod_apply]
 
 lemma mul_eq_add (ψ χ : AddChar A M) : ψ * χ = ψ + χ := rfl
 lemma pow_eq_nsmul (ψ : AddChar A M) (n : ℕ) : ψ ^ n = n • ψ := rfl
-lemma prod_eq_sum (s : Finset ι) (ψ : ι → AddChar A M) : ∏ i in s, ψ i = ∑ i in s, ψ i := rfl
+lemma prod_eq_sum (s : Finset ι) (ψ : ι → AddChar A M) : ∏ i ∈ s, ψ i = ∑ i ∈ s, ψ i := rfl
 
 @[simp] lemma toMonoidHomEquiv_add (ψ φ : AddChar A M) :
     toMonoidHomEquiv (ψ + φ) = toMonoidHomEquiv ψ * toMonoidHomEquiv φ := rfl

Mathlib/Algebra/Group/ForwardDiff.lean

@@ -135,7 +135,7 @@ Express the `n`-th forward difference of `f` at `y` in terms of the values `f (y
 `0 ≤ k ≤ n`.
 -/
 theorem fwdDiff_iter_eq_sum_shift (f : M → G) (n : ℕ) (y : M) :
-    Δ_[h]^[n] f y = ∑ k in range (n + 1), ((-1 : ℤ) ^ (n - k) * n.choose k) • f (y + k • h) := by
+    Δ_[h]^[n] f y = ∑ k ∈ range (n + 1), ((-1 : ℤ) ^ (n - k) * n.choose k) • f (y + k • h) := by
   -- rewrite in terms of `(shiftₗ - 1) ^ n`
   have : fwdDiffₗ M G h = shiftₗ M G h - 1 := by simp only [shiftₗ, add_sub_cancel_right]
   rw [← coe_fwdDiffₗ, this, ← LinearMap.pow_apply]
@@ -155,7 +155,7 @@ theorem fwdDiff_iter_eq_sum_shift (f : M → G) (n : ℕ) (y : M) :
 of `f` at `y`.
 -/
 theorem shift_eq_sum_fwdDiff_iter (f : M → G) (n : ℕ) (y : M) :
-    f (y + n • h) = ∑ k in range (n + 1), n.choose k • Δ_[h]^[k] f y := by
+    f (y + n • h) = ∑ k ∈ range (n + 1), n.choose k • Δ_[h]^[k] f y := by
   convert congr_fun (LinearMap.congr_fun
       ((Commute.one_right (fwdDiffₗ M G h)).add_pow n) f) y using 1
   · rw [← shiftₗ_pow_apply h f, shiftₗ]

Mathlib/Algebra/Group/Translate.lean

@@ -72,7 +72,7 @@ section AddCommMonoid
 variable [AddCommMonoid M]
 
 lemma translate_sum_right (a : G) (f : ι → G → M) (s : Finset ι) :
-    τ a (∑ i in s, f i) = ∑ i in s, τ a (f i) := by ext; simp
+    τ a (∑ i ∈ s, f i) = ∑ i ∈ s, τ a (f i) := by ext; simp
 
 lemma sum_translate [Fintype G] (a : G) (f : G → M) : ∑ b, τ a f b = ∑ b, f b :=
   Fintype.sum_equiv (Equiv.subRight _) _ _ fun _ ↦ rfl
@@ -90,4 +90,4 @@ end AddCommGroup
 variable [CommMonoid M]
 
 lemma translate_prod_right (a : G) (f : ι → G → M) (s : Finset ι) :
-    τ a (∏ i in s, f i) = ∏ i in s, τ a (f i) := by ext; simp
+    τ a (∏ i ∈ s, f i) = ∏ i ∈ s, τ a (f i) := by ext; simp

Mathlib/Algebra/Lie/Derivation/Basic.lean

@@ -127,7 +127,7 @@ open Finset Nat
 
 /-- The general Leibniz rule for Lie derivatives. -/
 theorem iterate_apply_lie (D : LieDerivation R L L) (n : ℕ) (a b : L) :
-    D^[n] ⁅a, b⁆ = ∑ ij in antidiagonal n, choose n ij.1 • ⁅D^[ij.1] a, D^[ij.2] b⁆ := by
+    D^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, choose n ij.1 • ⁅D^[ij.1] a, D^[ij.2] b⁆ := by
   induction n with
   | zero => simp
   | succ n ih =>
@@ -139,7 +139,7 @@ theorem iterate_apply_lie (D : LieDerivation R L L) (n : ℕ) (a b : L) :
 
 /-- Alternate version of the general Leibniz rule for Lie derivatives. -/
 theorem iterate_apply_lie' (D : LieDerivation R L L) (n : ℕ) (a b : L) :
-    D^[n] ⁅a, b⁆ = ∑ i in range (n + 1), n.choose i • ⁅D^[i] a, D^[n - i] b⁆ := by
+    D^[n] ⁅a, b⁆ = ∑ i ∈ range (n + 1), n.choose i • ⁅D^[i] a, D^[n - i] b⁆ := by
   rw [iterate_apply_lie D n a b]
   exact sum_antidiagonal_eq_sum_range_succ (fun i j ↦ n.choose i • ⁅D^[i] a, D^[j] b⁆) n
 

Mathlib/Algebra/Lie/TraceForm.lean

@@ -426,10 +426,10 @@ lemma traceForm_eq_sum_finrank_nsmul :
 /-- A variant of `LieModule.traceForm_eq_sum_finrank_nsmul` in which the sum is taken only over the
 non-zero weights. -/
 lemma traceForm_eq_sum_finrank_nsmul' :
-    traceForm K L M = ∑ χ in {χ : Weight K L M | χ.IsNonZero}, finrank K (genWeightSpace M χ) •
+    traceForm K L M = ∑ χ ∈ {χ : Weight K L M | χ.IsNonZero}, finrank K (genWeightSpace M χ) •
       (χ : L →ₗ[K] K).smulRight (χ : L →ₗ[K] K) := by
   classical
-  suffices ∑ χ in {χ : Weight K L M | χ.IsZero}, finrank K (genWeightSpace M χ) •
+  suffices ∑ χ ∈ {χ : Weight K L M | χ.IsZero}, finrank K (genWeightSpace M χ) •
       (χ : L →ₗ[K] K).smulRight (χ : L →ₗ[K] K) = 0 by
     rw [traceForm_eq_sum_finrank_nsmul,
       ← Finset.sum_filter_add_sum_filter_not (p := fun χ : Weight K L M ↦ χ.IsNonZero)]

Mathlib/Algebra/Lie/Weights/Killing.lean

@@ -561,7 +561,7 @@ lemma finrank_rootSpace_eq_one (α : Weight K H L) (hα : α.IsNonZero) :
 noncomputable abbrev _root_.LieSubalgebra.root : Finset (Weight K H L) := {α | α.IsNonZero}
 
 lemma restrict_killingForm_eq_sum :
-    (killingForm K L).restrict H = ∑ α in H.root, (α : H →ₗ[K] K).smulRight (α : H →ₗ[K] K) := by
+    (killingForm K L).restrict H = ∑ α ∈ H.root, (α : H →ₗ[K] K).smulRight (α : H →ₗ[K] K) := by
   rw [restrict_killingForm, traceForm_eq_sum_finrank_nsmul' K H L]
   refine Finset.sum_congr rfl fun χ hχ ↦ ?_
   replace hχ : χ.IsNonZero := by simpa [LieSubalgebra.root] using hχ

Mathlib/Analysis/BoxIntegral/Basic.lean

@@ -711,7 +711,7 @@ theorem integrable_of_bounded_and_ae_continuousWithinAt [CompleteSpace E] {I : B
         exact hC _ (TaggedPrepartition.tag_mem_Icc _ J)
     apply (norm_sum_le_of_le B' this).trans
     simp_rw [← sum_mul, μ.toBoxAdditive_apply, ← toReal_sum (fun J hJ ↦ μJ_ne_top J (hB' hJ))]
-    suffices (∑ J in B', μ J).toReal ≤ ε₂ by
+    suffices (∑ J ∈ B', μ J).toReal ≤ ε₂ by
       linarith [mul_le_mul_of_nonneg_right this <| (mul_nonneg_iff_of_pos_left two_pos).2 C0]
     rw [← toReal_ofReal (le_of_lt ε₂0)]
     refine toReal_mono ofReal_ne_top (le_trans ?_ (le_of_lt hU))

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean

@@ -364,7 +364,7 @@ open Finset in
 lemma cfcₙ_sum {ι : Type*} (f : ι → R → R) (a : A) (s : Finset ι)
     (hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a) := by cfc_cont_tac)
     (hf0 : ∀ i ∈ s, f i 0 = 0 := by cfc_zero_tac) :
-    cfcₙ (∑ i in s, f i) a = ∑ i in s, cfcₙ (f i) a := by
+    cfcₙ (∑ i ∈ s, f i) a = ∑ i ∈ s, cfcₙ (f i) a := by
   by_cases ha : p a
   · have hsum : s.sum f = fun z => ∑ i ∈ s, f i z := by ext; simp
     have hf' : ContinuousOn (∑ i : s, f i) (σₙ R a) := by

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

@@ -485,7 +485,7 @@ lemma cfc_add_const (r : R) (f : R → R) (a : A)
 open Finset in
 lemma cfc_sum {ι : Type*} (f : ι → R → R) (a : A) (s : Finset ι)
     (hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a) := by cfc_cont_tac) :
-    cfc (∑ i in s, f i)  a = ∑ i in s, cfc (f i) a := by
+    cfc (∑ i ∈ s, f i)  a = ∑ i ∈ s, cfc (f i) a := by
   by_cases ha : p a
   · have hsum : s.sum f = fun z => ∑ i ∈ s, f i z := by ext; simp
     have hf' : ContinuousOn (∑ i : s, f i) (spectrum R a) := by

Mathlib/Analysis/Distribution/FourierSchwartz.lean

@@ -50,9 +50,9 @@ noncomputable def fourierTransformCLM : 𝓢(V, E) →L[𝕜] 𝓢(V, E) := by
     simp only [mul_assoc]
     gcongr
     calc
-    ∑ p in Finset.range (n + 1) ×ˢ Finset.range (k + 1),
+    ∑ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
         ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 (⇑f) v‖
-      ≤ ∑ p in Finset.range (n + 1) ×ˢ Finset.range (k + 1),
+      ≤ ∑ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
         2 ^ integrablePower (volume : Measure V) *
         (∫ (x : V), (1 + ‖x‖) ^ (- (integrablePower (volume : Measure V) : ℝ))) * 2 *
         ((Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1)).sup