bump mathlib

Author: mo271

FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean

@@ -94,8 +94,9 @@ lemma fermat_product (n : ℕ) : ∏ k in range n, F k = F n - 2 := by
   rw [prod_range_succ, hn]
   unfold F
   norm_num
-  rw [succ_eq_add_one, mul_comm, ← Nat.sq_sub_sq]
+  rw [mul_comm, (show 2 ^ 2 ^ n + 1 - 2 = 2 ^ 2 ^ n - 1 by aesop),  ← Nat.sq_sub_sq]
   ring_nf
+  omega
 
 theorem infinity_of_primes₂  (k n : ℕ) (h : k < n): Coprime (F n) (F k) := by
   let m := (F n).gcd (F k)
@@ -132,6 +133,11 @@ lemma ZMod.two_ne_one (q : ℕ)  [Fact (1 < q)] : (2 : ZMod q) ≠ 1 := by
   intro h1
   have h : (2 - 1 : ZMod q) = 0 := by exact Iff.mpr sub_eq_zero h1
   norm_num at h
+#check pred_le_pred
+
+lemma sub_one_le_sub_one {n m : ℕ} : n ≤ m → n - 1 ≤ m - 1 := by
+  intro h
+  exact pred_le_pred h
 
 
 theorem infinity_of_primes₃:
@@ -143,7 +149,7 @@ theorem infinity_of_primes₃:
   -- This m has a prime factor;
   -- we pick the minimal one, the argument works with any prime factor
   let q := m.minFac
-  have hq : q.Prime := minFac_prime <| Nat.ne_of_gt <| one_lt_mersenne <| Prime.one_lt hp
+  have hq : q.Prime := minFac_prime <| Nat.ne_of_gt <| one_lt_mersenne.mpr <| Prime.one_lt hp
   have : Fact (Nat.Prime q) := by exact { out := hq }
   have h_mod_q : 2 ^ p  ≡ 1 [MOD q] := by
     have : (2^p - 1) % q = 0 :=  mod_eq_zero_of_dvd (minFac_dvd m)
@@ -155,7 +161,7 @@ theorem infinity_of_primes₃:
         zero_sub, neg_sub] at hc
     simp [cast_one, cast_pow, cast_ofNat, hc.symm]
   have h_mod_q' : (2 : (ZMod q)) ^ p = 1 := by
-    have := (ZMod.nat_cast_eq_nat_cast_iff _ _ _).mpr h_mod_q
+    have := (ZMod.natCast_eq_natCast_iff _ _ _).mpr h_mod_q
     norm_cast at this
     rw [← this, cast_pow, cast_ofNat]
   have : (2 : (ZMod q)) * (2 ^ (p - 1)) = 1 := by
@@ -193,13 +199,13 @@ theorem infinity_of_primes₃:
   · refine' minFac_prime <| Nat.ne_of_gt _
     dsimp [mersenne]
     calc 1 < 2^2 - 1 := by norm_num
-        _  ≤ 2^p - 1 := (pred_eq_sub_one 4).symm ▸ pred_le_pred <|
-            pow_le_pow_of_le_right (succ_pos 1) (Prime.two_le hp)
+        _  ≤ 2^p - 1 := sub_one_le_sub_one <| pow_le_pow_of_le_right (succ_pos 1) (Prime.two_le hp)
   · have h2q : 2 ≤ q := by
       exact Prime.two_le <| minFac_prime <| Nat.ne_of_gt <| lt_of_succ_lt <|
           Nat.sub_le_sub_right ((pow_le_pow_of_le_right (succ_pos 1) (Prime.two_le hp))) 1
     exact lt_of_le_of_lt (Nat.le_of_dvd  (Nat.sub_pos_of_lt <| h2q) h_piv_div_q_sub_one)
         <| pred_lt <| Nat.ne_of_gt <| Nat.le_of_lt h2q
+
 /-!
 ### Fourth proof
 

FormalBook/Ch02_Bertrand's_postulate.lean

@@ -91,9 +91,9 @@ theorem real_main_inequality {x : ℝ} (n_large : (512 : ℝ) ≤ x) :
     conv in 512 => equals 2 ^ 9 => norm_num1
     conv in 2 * 512 => equals 2 ^ 10 => norm_num1
     conv in 32 => rw [← Nat.cast_ofNat]
-    rw [rpow_nat_cast, ← pow_mul, ← pow_add]
+    rw [rpow_natCast, ← pow_mul, ← pow_add]
     conv in 4 => equals 2 ^ (2 : ℝ) => rw [rpow_two]; norm_num1
-    rw [← rpow_mul, ← rpow_nat_cast]
+    rw [← rpow_mul, ← rpow_natCast]
     apply rpow_le_rpow_of_exponent_le
     all_goals norm_num1
 end Bertrand
@@ -106,7 +106,7 @@ open Nat
 theorem bertrand_main_inequality {n : ℕ} (n_large : 512 ≤ n) :
     n * (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ (2 * n / 3) ≤ 4 ^ n := by
   rw [← @cast_le ℝ]
-  simp only [cast_add, cast_one, cast_mul, cast_pow, ← Real.rpow_nat_cast]
+  simp only [cast_add, cast_one, cast_mul, cast_pow, ← Real.rpow_natCast]
   refine' _root_.trans ?_ (Bertrand.real_main_inequality (by exact_mod_cast n_large))
   gcongr
   · have n2_pos : 0 < 2 * n := by positivity

FormalBook/Ch06_Every_finite_division_ring_is_a_field.lean

@@ -283,9 +283,12 @@ theorem wedderburn (h: Fintype R): IsField R := by
   have h1 : (q ^ n - 1) = q - 1  + ∑ A : S', (q ^ n - 1) / (q ^ (n_k A) - 1) := by
     convert H1
     sorry
+  have hZ : Nonempty <| @Subtype R fun x => x ∈ Z := by
+      exact Zero.instNonempty
   have hq_pow_pos : ∀ m,  1 ≤ q ^ m := by
     intro m
     refine' one_le_pow m q _
+
     exact Fintype.card_pos
 
   have h_n_k_A_dvd: ∀ A : S', (n_k A ∣ n) := by sorry

lake-manifest.json

@@ -1,19 +1,19 @@
 {"version": 7,
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
-   "name": "std",
+   "rev": "14f258593e8c261d8834f13c6edc7b970c253ee8",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
+   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,25 +22,25 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
+   "rev": "f617e0673845925e612b62141ff54c4b7980dc63",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
+   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.30",
+   "inputRev": "v0.0.36",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,16 +49,16 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
+   "rev": "35e38eb320982cfd2fcc864e0e0467ca223c8cdb",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "9125a0936fd86f4bb74bebe27f0b1cd0c5a2b7cf",
+   "rev": "aad19d883960cbdd1807a3c31ef7a351c3f0c733",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -67,7 +67,7 @@
   {"url": "https://github.com/PatrickMassot/checkdecls.git",
    "type": "git",
    "subDir": null,
-   "rev": "2ee81a0269048010900117b675876a1d8db5883c",
+   "rev": "88ec21589a8eef430f4ea01147cde1aaa7963e16",
    "name": "checkdecls",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -76,7 +76,7 @@
   {"url": "https://github.com/xubaiw/CMark.lean",
    "type": "git",
    "subDir": null,
-   "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
+   "rev": "ba7b47bd773954b912ecbf5b1c9993c71a166f05",
    "name": "CMark",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,
-   "rev": "6a350f4ec7323a4e8ad6bf50736f779853d441e9",
+   "rev": "8b53cc65534bc2c6888c3d4c53a3439648213f74",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -103,7 +103,7 @@
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
-   "rev": "a34d3c1f7b72654c08abe5741d94794db40dbb2e",
+   "rev": "b91fea210b7b6b451f19c6344d1f82765b9607af",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.8.0-rc1