diff --git a/Compfiles/Bulgaria1998P3.lean b/Compfiles/Bulgaria1998P3.lean index d76b3c4..8ea2fc6 100644 --- a/Compfiles/Bulgaria1998P3.lean +++ b/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] diff --git a/Compfiles/Imo2003P6.lean b/Compfiles/Imo2003P6.lean index a1894e6..18cdbb5 100644 --- a/Compfiles/Imo2003P6.lean +++ b/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 diff --git a/Compfiles/Imo2013P5.lean b/Compfiles/Imo2013P5.lean index b566b67..e70cd6c 100644 --- a/Compfiles/Imo2013P5.lean +++ b/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 diff --git a/Compfiles/Imo2014P1.lean b/Compfiles/Imo2014P1.lean index acdd67d..8de1793 100644 --- a/Compfiles/Imo2014P1.lean +++ b/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 diff --git a/Compfiles/Imo2018P5.lean b/Compfiles/Imo2018P5.lean index 687eaa6..0328413 100644 --- a/Compfiles/Imo2018P5.lean +++ b/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 diff --git a/Compfiles/KolmogorovStreams.lean b/Compfiles/KolmogorovStreams.lean index d445a2d..0eaaaa9 100644 --- a/Compfiles/KolmogorovStreams.lean +++ b/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 diff --git a/Compfiles/Usa1989P5.lean b/Compfiles/Usa1989P5.lean index de385ec..8010ee9 100644 --- a/Compfiles/Usa1989P5.lean +++ b/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 diff --git a/Compfiles/Usa1998P5.lean b/Compfiles/Usa1998P5.lean index 4709f51..9682e7a 100644 --- a/Compfiles/Usa1998P5.lean +++ b/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] diff --git a/lake-manifest.json b/lake-manifest.json index 592ba82..6470553 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "b848c8d0c15bae84d026e1c3aa1f89bb78f87d80", + "rev": "b9c7233cfdbab76db1cf230182a5e4447e081e90", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master",