update mathlib

Compfiles/Bulgaria1998P3.lean

@@ -91,7 +91,7 @@ problem bulgaria1998_p3
     | succ pn hpn =>
     have hpp : x_seq pn.succ = x_seq pn + f 1 / 2^pn := by
       rw [show x_seq _ = 1 + ∑ i ∈ Finset.range _, (f 1) / (2^i) by rfl]
-      have : ∑ i in Finset.range pn.succ, f 1 / 2 ^ i =
+      have : ∑ i ∈ Finset.range pn.succ, f 1 / 2 ^ i =
               f 1 / 2 ^ pn + ∑ i ∈ Finset.range pn, f 1 / 2 ^ i :=
         Finset.sum_range_succ_comm (λ (x : ℕ) ↦ f 1 / 2 ^ x) pn
       rw [this]

Compfiles/Imo2003P6.lean

@@ -68,7 +68,7 @@ problem imo2003_p6 (p : ℕ) (hp : p.Prime) :
     interval_cases m <;> norm_num at this
 
   -- p > 2
-  let N := ∑ i in range p, p^i
+  let N := ∑ i ∈ range p, p^i
   have N_nz : N ≠ 0 := by
     apply Nat.ne_zero_iff_zero_lt.mpr
     apply sum_pos
@@ -90,7 +90,7 @@ problem imo2003_p6 (p : ℕ) (hp : p.Prime) :
             exact ⟨Nat.Prime.pos hp, by simp [hp.one_lt], Or.inl hp.one_lt⟩
           _ = p ^ 2 - p := by simp [Nat.pow_two, Nat.mul_sub]
       exact Nat.mod_eq_of_lt this
-    have : ∀ m ≥ 2, (∑ i in range m, p^i) % (p ^ 2) = p + 1 := by
+    have : ∀ m ≥ 2, (∑ i ∈ range m, p^i) % (p ^ 2) = p + 1 := by
       intro m hm
       cases' m with m; norm_num at hm
       cases' m with m; norm_num at hm
@@ -174,8 +174,8 @@ problem imo2003_p6 (p : ℕ) (hp : p.Prime) :
         simp [this, one_mod_p_1]
       · exact Nat.sub_le _ _
     have : N % (p - 1) = 1 := calc N % (p - 1)
-      _ = (∑ i in range p, (p^i) % (p - 1)) % (p - 1) := Finset.sum_nat_mod _ _ _
-      _ = (∑ i in range p, 1) % (p - 1) := by
+      _ = (∑ i ∈ range p, (p^i) % (p - 1)) % (p - 1) := Finset.sum_nat_mod _ _ _
+      _ = (∑ i ∈ range p, 1) % (p - 1) := by
         congr; funext i
         simp [Nat.pow_mod, one_mod_p_1, p_mod_p_1]
       _ = 1 := by simp [p_mod_p_1]
@@ -204,13 +204,13 @@ problem imo2003_p6 (p : ℕ) (hp : p.Prime) :
     rw [ZMod.natCast_zmod_eq_zero_iff_dvd] at q_dvd_p
 
     have : N % p = 1 := calc N % p
-      _ = (∑ i in range p, (p^i) % p) % p := Finset.sum_nat_mod _ _ _
-      _ = (∑ i in range (p - 1 + 1), (p^i) % p) % p := by
+      _ = (∑ i ∈ range p, (p^i) % p) % p := Finset.sum_nat_mod _ _ _
+      _ = (∑ i ∈ range (p - 1 + 1), (p^i) % p) % p := by
         nth_rw 1 [← Nat.succ_pred_prime hp]
         simp
-      _ = (∑ i in range (p - 1), p^(i+1) % p + 1) % p := by
+      _ = (∑ i ∈ range (p - 1), p^(i+1) % p + 1) % p := by
         simp [Finset.sum_range_succ']
-      _ = (∑ i in range (p - 1), 0 + 1) % p := by
+      _ = (∑ i ∈ range (p - 1), 0 + 1) % p := by
         congr; funext i
         apply Nat.mod_eq_zero_of_dvd
         exact Dvd.intro_left (p.pow i) rfl

Compfiles/Imo2013P5.lean

@@ -50,10 +50,10 @@ lemma le_of_all_pow_lt_succ {x y : ℝ} (hx : 1 < x) (hy : 1 < y)
            _ ≤ x^i * y^(n-1-i) := by gcongr; apply one_le_pow₀ hy.le
     calc (x - y) * (n : ℝ)
         = (n : ℝ) * (x - y) := mul_comm _ _
-      _ = (∑ _i in Finset.range n, (1 : ℝ)) * (x - y) :=
+      _ = (∑ _i ∈ Finset.range n, (1 : ℝ)) * (x - y) :=
                                  by simp only [mul_one, Finset.sum_const, nsmul_eq_mul,
                                     Finset.card_range]
-      _ ≤ (∑ i in Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x-y) :=
+      _ ≤ (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x-y) :=
                                   (mul_le_mul_right hxmy).mpr (Finset.sum_le_sum hterm)
       _ = x^n - y^n         := geom_sum₂_mul x y n
 

Compfiles/Imo2014P1.lean

@@ -80,13 +80,13 @@ snip end
 
 problem imo2014_p1 (a : ℕ → ℤ) (apos : ∀ i, 0 < a i) (ha : ∀ i, a i < a (i + 1)) :
     ∃! n : ℕ, 0 < n ∧
-              n * a n < (∑ i in Finset.range (n + 1), a i) ∧
-              (∑ i in Finset.range (n + 1), a i) ≤ n * a (n + 1) := by
+              n * a n < (∑ i ∈ Finset.range (n + 1), a i) ∧
+              (∑ i ∈ Finset.range (n + 1), a i) ≤ n * a (n + 1) := by
   -- Informal solution by Fedor Petrov, via Evan Chen:
   -- https://web.evanchen.cc/exams/IMO-2014-notes.pdf
 
-  let b : ℕ → ℤ := fun i ↦ ∑ j in Finset.range i, (a i - a (j + 1))
-  have hb : ∀ i, b i = i * a i - ∑ j in Finset.range i, a (j + 1) := by
+  let b : ℕ → ℤ := fun i ↦ ∑ j ∈ Finset.range i, (a i - a (j + 1))
+  have hb : ∀ i, b i = i * a i - ∑ j ∈ Finset.range i, a (j + 1) := by
     intro i
     simp [b]
   have hb1 : b 1 = 0 := by norm_num [b]
@@ -99,14 +99,14 @@ problem imo2014_p1 (a : ℕ → ℤ) (apos : ∀ i, 0 < a i) (ha : ∀ i, a i <
     nlinarith
 
   have h1 : ∀ j,
-    (0 < j ∧ j * a j < (∑ i in Finset.range (j + 1), a i) ∧
-                       (∑ i in Finset.range (j + 1), a i) ≤ j * a (j + 1)) ↔
+    (0 < j ∧ j * a j < (∑ i ∈ Finset.range (j + 1), a i) ∧
+                       (∑ i ∈ Finset.range (j + 1), a i) ≤ j * a (j + 1)) ↔
     (0 < j ∧ b j < a 0 ∧ a 0 ≤ b (j + 1)) := fun j ↦ by
     rw [hb, hb]
     constructor
     · rintro ⟨hj0, hj1, hj2⟩
       refine ⟨hj0, ?_, ?_⟩
-      · suffices H : ↑j * a j < ∑ i in Finset.range j, a (i + 1) + a 0 by
+      · suffices H : ↑j * a j < ∑ i ∈ Finset.range j, a (i + 1) + a 0 by
           exact Int.sub_left_lt_of_lt_add H
         rwa [Finset.sum_range_succ'] at hj1
       · rw [Finset.sum_range_succ'] at hj2

Compfiles/Imo2018P5.lean

@@ -32,7 +32,7 @@ problem imo2018_p5
     (hN : 0 < N)
     (h : ∀ n, N ≤ n →
       ∃ z : ℤ,
-        z = ∑ i in Finset.range n, (a i : ℚ) / a ((i + 1) % n))
+        z = ∑ i ∈ Finset.range n, (a i : ℚ) / a ((i + 1) % n))
     : ∃ M, ∀ m, M ≤ m → a m = a (m + 1) := by
   sorry
 

Compfiles/KolmogorovStreams.lean

@@ -59,12 +59,12 @@ lemma break_into_words_closed_form
     (lengths : Stream' ℕ)
     (a : Stream' α)
    : break_into_words lengths a =
-      (λ i ↦ Stream'.take (lengths i) (Stream'.drop (∑ j in Finset.range i, lengths j) a)) := by
+      (λ i ↦ Stream'.take (lengths i) (Stream'.drop (∑ j ∈ Finset.range i, lengths j) a)) := by
   funext n
   convert_to ((Stream'.corec (λ x ↦ Stream'.take (x.fst.head) x.snd)
                  (λ x ↦ ⟨x.fst.tail, Stream'.drop (x.fst.head) x.snd⟩)) :
                   Stream' ℕ × Stream' α → Stream' (List α)) ⟨lengths, a⟩ n =
-             Stream'.take (lengths n) (Stream'.drop (∑ j in Finset.range n, lengths j) a)
+             Stream'.take (lengths n) (Stream'.drop (∑ j ∈ Finset.range n, lengths j) a)
   rw [Stream'.corec_def,Stream'.map]
   congr
   · revert a lengths
@@ -132,7 +132,7 @@ lemma chosen_decent_closed_form
     (hnot: ∀ (n : ℕ), ∃ (k : ℕ), 0 < k ∧
             all_prefixes is_decent (a.drop (n + k)))
     : ∀ n : ℕ, (((choose_decent_words is_decent a hinit hnot).get n).start =
-              ∑ j in Finset.range n, ((choose_decent_words is_decent a hinit hnot).get j).length)
+              ∑ j ∈ Finset.range n, ((choose_decent_words is_decent a hinit hnot).get j).length)
             := by
   intro n
   induction n with
@@ -191,7 +191,7 @@ lemma chosen_indecent_closed_form
     (a : Stream' α)
     (h: ∀ (k : ℕ), ¬all_prefixes is_decent (a.drop k))
     : ∀ n : ℕ, (((choose_indecent_words is_decent a h).get n).start =
-                ∑ j in Finset.range n, ((choose_indecent_words is_decent a h).get j).length)
+                ∑ j ∈ Finset.range n, ((choose_indecent_words is_decent a h).get j).length)
              := by
   intro n
   induction n with

Compfiles/Usa1989P5.lean

@@ -26,15 +26,15 @@ determine u_is_larger : Bool := false
 
 problem usa1989_p5
     (u v : ℝ)
-    (hu : (∑ i in Finset.range 8, u^(i + 1)) + 10 * u^9 = 8)
-    (hv : (∑ i in Finset.range 10, v^(i + 1)) + 10 * v^11 = 8) :
+    (hu : (∑ i ∈ Finset.range 8, u^(i + 1)) + 10 * u^9 = 8)
+    (hv : (∑ i ∈ Finset.range 10, v^(i + 1)) + 10 * v^11 = 8) :
     if u_is_larger then v < u else u < v := by
   -- solution from
   -- https://artofproblemsolving.com/wiki/index.php/1989_USAMO_Problems/Problem_5
   simp only [u_is_larger, ite_false]
 
-  let U (x : ℝ) : ℝ := (∑ i in Finset.range 8, x^(i + 1)) + 10 * x^9
-  let V (x : ℝ) : ℝ := (∑ i in Finset.range 10, x^(i + 1)) + 10 * x^11
+  let U (x : ℝ) : ℝ := (∑ i ∈ Finset.range 8, x^(i + 1)) + 10 * x^9
+  let V (x : ℝ) : ℝ := (∑ i ∈ Finset.range 10, x^(i + 1)) + 10 * x^11
 
   change U u = 8 at hu
   change V v = 8 at hv

Compfiles/Usa1998P5.lean

@@ -37,7 +37,7 @@ problem usa1998_p5 (n : ℕ) (_hn : 2 ≤ n) :
   | zero => use ∅; simp
   | succ n ih =>
     obtain ⟨Sp, sp_nonnegative, sp_card, hsp⟩ := ih
-    let L : ℤ := ∏ s in Sp, ∏ t in Sp.erase s, (s-t)^2
+    let L : ℤ := ∏ s ∈ Sp, ∏ t ∈ Sp.erase s, (s-t)^2
 
     have L_pos : 0 < L := by
       refine Finset.prod_pos fun s _ ↦ Finset.prod_pos ?_
@@ -92,12 +92,12 @@ problem usa1998_p5 (n : ℕ) (_hn : 2 ≤ n) :
             replace hb2 : L + b = β := hb2
             have a_ne_b : a ≠ b := by omega
             have ih := hsp a ha b hb a_ne_b
-            have h5 : L = (∏ t in Sp.erase a, (a-t)^2) *
-                         ∏ s in Sp.erase a, ∏ t in Sp.erase s, (s-t)^2 :=
+            have h5 : L = (∏ t ∈ Sp.erase a, (a-t)^2) *
+                         ∏ s ∈ Sp.erase a, ∏ t ∈ Sp.erase s, (s-t)^2 :=
               (Finset.mul_prod_erase Sp _ ha).symm
             have hbb := Finset.mem_erase.mpr ⟨a_ne_b.symm, hb⟩
-            have h6 : (a-b)^2 * ∏ t in (Sp.erase a).erase b, (a-t)^2 =
-                      ∏ t in Sp.erase a, (a-t)^2 :=
+            have h6 : (a-b)^2 * ∏ t ∈ (Sp.erase a).erase b, (a-t)^2 =
+                      ∏ t ∈ Sp.erase a, (a-t)^2 :=
                Finset.mul_prod_erase (Sp.erase a) (fun x ↦ (a-x)^2) hbb
             have Lmod : L % (a - b)^2 = 0 := by
                  rw [h5, ←h6, mul_assoc, Int.mul_emod, Int.emod_self]

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b848c8d0c15bae84d026e1c3aa1f89bb78f87d80",
+   "rev": "b9c7233cfdbab76db1cf230182a5e4447e081e90",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",