chore: avoid deprecated notation (∑ x in s, f x and ∏ x in s, f x) (#289)

Co-authored-by: u <u@h>

Author: euprunin

MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean

@@ -198,16 +198,16 @@ open BigOperators
 open Finset
 
 -- EXAMPLES:
-example : s.sum f = ∑ x in s, f x :=
+example : s.sum f = ∑ x ∈ s, f x :=
   rfl
 
-example : s.prod f = ∏ x in s, f x :=
+example : s.prod f = ∏ x ∈ s, f x :=
   rfl
 
-example : (range n).sum f = ∑ x in range n, f x :=
+example : (range n).sum f = ∑ x ∈ range n, f x :=
   rfl
 
-example : (range n).prod f = ∏ x in range n, f x :=
+example : (range n).prod f = ∏ x ∈ range n, f x :=
   rfl
 -- QUOTE.
 
@@ -217,16 +217,16 @@ provide a recursive description of summation up to :math:`n`,
 and similarly for products.
 EXAMPLES: -/
 -- QUOTE:
-example (f : ℕ → ℕ) : ∑ x in range 0, f x = 0 :=
+example (f : ℕ → ℕ) : ∑ x ∈ range 0, f x = 0 :=
   Finset.sum_range_zero f
 
-example (f : ℕ → ℕ) (n : ℕ) : ∑ x in range n.succ, f x = ∑ x in range n, f x + f n :=
+example (f : ℕ → ℕ) (n : ℕ) : ∑ x ∈ range n.succ, f x = ∑ x ∈ range n, f x + f n :=
   Finset.sum_range_succ f n
 
-example (f : ℕ → ℕ) : ∏ x in range 0, f x = 1 :=
+example (f : ℕ → ℕ) : ∏ x ∈ range 0, f x = 1 :=
   Finset.prod_range_zero f
 
-example (f : ℕ → ℕ) (n : ℕ) : ∏ x in range n.succ, f x = (∏ x in range n, f x) * f n :=
+example (f : ℕ → ℕ) (n : ℕ) : ∏ x ∈ range n.succ, f x = (∏ x ∈ range n, f x) * f n :=
   Finset.prod_range_succ f n
 -- QUOTE.
 
@@ -237,7 +237,7 @@ you can replace the proofs by ``rfl``.
 The following expresses the factorial function that we defined as a product.
 EXAMPLES: -/
 -- QUOTE:
-example (n : ℕ) : fac n = ∏ i in range n, (i + 1) := by
+example (n : ℕ) : fac n = ∏ i ∈ range n, (i + 1) := by
   induction' n with n ih
   · simp [fac, prod_range_zero]
   simp [fac, ih, prod_range_succ, mul_comm]
@@ -276,7 +276,7 @@ because calculations with division generally have side conditions.
 (It is similarly useful to avoid using subtraction on the natural numbers when possible.)
 EXAMPLES: -/
 -- QUOTE:
-theorem sum_id (n : ℕ) : ∑ i in range (n + 1), i = n * (n + 1) / 2 := by
+theorem sum_id (n : ℕ) : ∑ i ∈ range (n + 1), i = n * (n + 1) / 2 := by
   symm; apply Nat.div_eq_of_eq_mul_right (by norm_num : 0 < 2)
   induction' n with n ih
   · simp
@@ -289,7 +289,7 @@ We encourage you to prove the analogous identity for sums of squares,
 and other identities you can find on the web.
 BOTH: -/
 -- QUOTE:
-theorem sum_sqr (n : ℕ) : ∑ i in range (n + 1), i ^ 2 = n * (n + 1) * (2 * n + 1) / 6 := by
+theorem sum_sqr (n : ℕ) : ∑ i ∈ range (n + 1), i ^ 2 = n * (n + 1) * (2 * n + 1) / 6 := by
 /- EXAMPLES:
   sorry
 SOLUTIONS: -/

MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean

@@ -272,10 +272,10 @@ end
 /- TEXT:
 The theorem ``Finset.dvd_prod_of_mem`` tells us that if an
 ``n`` is an element of a finite set ``s``, then ``n`` divides
-``∏ i in s, i``.
+``∏ i ∈ s, i``.
 EXAMPLES: -/
 -- QUOTE:
-example (s : Finset ℕ) (n : ℕ) (h : n ∈ s) : n ∣ ∏ i in s, i :=
+example (s : Finset ℕ) (n : ℕ) (h : n ∈ s) : n ∣ ∏ i ∈ s, i :=
   Finset.dvd_prod_of_mem _ h
 -- QUOTE.
 
@@ -318,7 +318,7 @@ and then finish it off.
 BOTH: -/
 -- QUOTE:
 theorem mem_of_dvd_prod_primes {s : Finset ℕ} {p : ℕ} (prime_p : p.Prime) :
-    (∀ n ∈ s, Nat.Prime n) → (p ∣ ∏ n in s, n) → p ∈ s := by
+    (∀ n ∈ s, Nat.Prime n) → (p ∣ ∏ n ∈ s, n) → p ∈ s := by
   intro h₀ h₁
   induction' s using Finset.induction_on with a s ans ih
   · simp at h₁
@@ -372,7 +372,7 @@ theorem primes_infinite' : ∀ s : Finset Nat, ∃ p, Nat.Prime p ∧ p ∉ s :=
     intro n
     simp [s'_def]
     apply h
-  have : 2 ≤ (∏ i in s', i) + 1 := by
+  have : 2 ≤ (∏ i ∈ s', i) + 1 := by
 /- EXAMPLES:
     sorry
 SOLUTIONS: -/
@@ -383,7 +383,7 @@ SOLUTIONS: -/
     apply (mem_s'.mp ns').pos
 -- BOTH:
   rcases exists_prime_factor this with ⟨p, pp, pdvd⟩
-  have : p ∣ ∏ i in s', i := by
+  have : p ∣ ∏ i ∈ s', i := by
 /- EXAMPLES:
     sorry
 SOLUTIONS: -/
@@ -595,7 +595,7 @@ theorem primes_mod_4_eq_3_infinite : ∀ n, ∃ p > n, Nat.Prime p ∧ p % 4 = 3
     rcases hn with ⟨p, ⟨pp, p4⟩, pltn⟩
     exact ⟨p, pltn, pp, p4⟩
   rcases this with ⟨s, hs⟩
-  have h₁ : ((4 * ∏ i in erase s 3, i) + 3) % 4 = 3 := by
+  have h₁ : ((4 * ∏ i ∈ erase s 3, i) + 3) % 4 = 3 := by
 /- EXAMPLES:
     sorry
 SOLUTIONS: -/
@@ -624,7 +624,7 @@ SOLUTIONS: -/
       tauto
     simp at this
 -- BOTH:
-  have : p ∣ 4 * ∏ i in erase s 3, i := by
+  have : p ∣ 4 * ∏ i ∈ erase s 3, i := by
 /- EXAMPLES:
     sorry
 SOLUTIONS: -/

MIL/C10_Topology/S02_Metric_Spaces.lean

@@ -430,9 +430,9 @@ theorem cauchySeq_of_le_geometric_two' {u : ℕ → X}
   obtain ⟨k, rfl : n = N + k⟩ := le_iff_exists_add.mp hn
   calc
     dist (u (N + k)) (u N) = dist (u (N + 0)) (u (N + k)) := sorry
-    _ ≤ ∑ i in range k, dist (u (N + i)) (u (N + (i + 1))) := sorry
-    _ ≤ ∑ i in range k, (1 / 2 : ℝ) ^ (N + i) := sorry
-    _ = 1 / 2 ^ N * ∑ i in range k, (1 / 2 : ℝ) ^ i := sorry
+    _ ≤ ∑ i  ∈ range k, dist (u (N + i)) (u (N + (i + 1))) := sorry
+    _ ≤ ∑ i  ∈ range k, (1 / 2 : ℝ) ^ (N + i) := sorry
+    _ = 1 / 2 ^ N * ∑ i  ∈ range k, (1 / 2 : ℝ) ^ i := sorry
     _ ≤ 1 / 2 ^ N * 2 := sorry
     _ < ε := sorry
 
@@ -456,10 +456,10 @@ example {u : ℕ → X} (hu : ∀ n : ℕ, dist (u n) (u (n + 1)) ≤ (1 / 2) ^
   obtain ⟨k, rfl : n = N + k⟩ := le_iff_exists_add.mp hn
   calc
     dist (u (N + k)) (u N) = dist (u (N + 0)) (u (N + k)) := by rw [dist_comm, add_zero]
-    _ ≤ ∑ i in range k, dist (u (N + i)) (u (N + (i + 1))) :=
+    _ ≤ ∑ i  ∈ range k, dist (u (N + i)) (u (N + (i + 1))) :=
       (dist_le_range_sum_dist (fun i ↦ u (N + i)) k)
-    _ ≤ ∑ i in range k, (1 / 2 : ℝ) ^ (N + i) := (sum_le_sum fun i _ ↦ hu <| N + i)
-    _ = 1 / 2 ^ N * ∑ i in range k, (1 / 2 : ℝ) ^ i := by simp_rw [← one_div_pow, pow_add, ← mul_sum]
+    _ ≤ ∑ i  ∈ range k, (1 / 2 : ℝ) ^ (N + i) := (sum_le_sum fun i _ ↦ hu <| N + i)
+    _ = 1 / 2 ^ N * ∑ i  ∈ range k, (1 / 2 : ℝ) ^ i := by simp_rw [← one_div_pow, pow_add, ← mul_sum]
     _ ≤ 1 / 2 ^ N * 2 :=
       (mul_le_mul_of_nonneg_left (sum_geometric_two_le _)
         (one_div_nonneg.mpr (pow_nonneg (zero_le_two : (0 : ℝ) ≤ 2) _)))