bump mathlib

mo271 · Sep 18, 2024 · 3162a7f · 3162a7f
1 parent 6fbe8c2
commit 3162a7f
Show file tree

Hide file tree

Showing 9 changed files with 65 additions and 47 deletions.
diff --git a/FormalBook/Chapter_01.lean b/FormalBook/Chapter_01.lean
@@ -82,7 +82,7 @@ lemma fermat_bounded (n : ℕ) : 2 < F n := by
   · exact lt_trans h fermat_stricly_monotone
 
 lemma fermat_odd {n : ℕ} : Odd (F n) := by
-  rw [F, odd_iff_not_even, even_add_one, not_not, even_pow]
+  rw [F, ← not_even_iff_odd, even_add_one, not_not, even_pow]
   refine' ⟨even_two, Nat.ne_of_gt (pow_pos _ _)⟩
   exact zero_lt_two
 
@@ -93,7 +93,6 @@ lemma fermat_product (n : ℕ) : ∏ k in range n, F k = F n - 2 := by
   · trivial
   rw [prod_range_succ, hn]
   unfold F
-  norm_num
   rw [mul_comm, (show 2 ^ 2 ^ n + 1 - 2 = 2 ^ 2 ^ n - 1 by aesop),  ← Nat.sq_sub_sq]
   ring_nf
   omega
@@ -118,7 +117,7 @@ theorem infinity_of_primes₂  (k n : ℕ) (h : k < n): Coprime (F n) (F k) := b
     rw [h_two] at h_n
     have h_even : Even (F n) := even_iff_two_dvd.mpr h_n
     have h_odd : Odd (F n) := fermat_odd
-    exact (odd_iff_not_even.mp h_odd) h_even
+    exact (not_even_iff_odd.mpr h_odd) h_even
 /-!
 ### Third proof
 
@@ -190,8 +189,10 @@ theorem infinity_of_primes₃:
     -- Using Lagrange's theorem here!
     convert Subgroup.card_subgroup_dvd_card (Subgroup.zpowers (two))
     · rw [← orderOf_eq_prime h_two two_ne_one]
+      simp only [card_eq_fintype_card]
       exact Fintype.card_zpowers.symm
-    · exact ((prime_iff_card_units q).mp hq).symm
+    · simp only [card_eq_fintype_card, ZMod.card_units_eq_totient]
+      exact Eq.symm (totient_prime hq)
   use q
   constructor
   · refine' minFac_prime <| Nat.ne_of_gt _
@@ -210,6 +211,7 @@ theorem infinity_of_primes₃:
 using elementary calculus
 -/
 open Filter
+open Nat.Prime
 
 noncomputable def primeCountingReal (x : ℝ) : ℕ :=
   if (x ≤ 0) then 0 else primeCounting ⌊x⌋₊

diff --git a/FormalBook/Chapter_02.lean b/FormalBook/Chapter_02.lean
@@ -15,12 +15,13 @@ limitations under the License.
 
 Authors: Moritz Firsching
 -/
-import Mathlib.Tactic
-import Mathlib.Data.Nat.Choose.Factorization
-import Mathlib.Data.Nat.PrimeNormNum
-import Mathlib.NumberTheory.Primorial
+import Mathlib.Algebra.Lie.OfAssociative
 import Mathlib.Analysis.Convex.SpecificFunctions.Basic
 import Mathlib.Analysis.Convex.SpecificFunctions.Deriv
+import Mathlib.Data.Nat.Choose.Factorization
+import Mathlib.Data.Real.StarOrdered
+import Mathlib.NumberTheory.Primorial
+import Mathlib.Tactic.NormNum.Prime
 /-!
 # Bertrand's postulate
 

diff --git a/FormalBook/Chapter_03.lean b/FormalBook/Chapter_03.lean
@@ -15,9 +15,10 @@ limitations under the License.
 
 Authors: Moritz Firsching, Christopher Schmidt
 -/
-import Mathlib.Tactic
-import Mathlib.RingTheory.Prime
-import Mathlib.Data.Nat.Prime
+import Mathlib.Analysis.Normed.Field.Lemmas
+import Mathlib.Data.Int.Star
+import Mathlib.Data.Rat.Star
+import Mathlib.Tactic.Qify
 --import data.nat.sqrt
 --set_option trace.simp_lemmas true
 
@@ -75,7 +76,7 @@ theorem prime_div_descFactorial (n k m l p : ℕ) (h_klen : k ≤ n)
   have h_fac_div' : ↑(n - k)! ∣ (n ! : ℤ) := dvd_of_mul_left_dvd h_fac_div
   have h_fac_div'' : (k ! : ℤ) ∣ (↑n ! / ↑(n - k)!) := by
     norm_cast
-    refine' (dvd_div_iff ((Int.coe_nat_dvd).mp h_fac_div')).mpr _
+    refine' (dvd_div_iff_mul_dvd ((Int.natCast_dvd_natCast).mp h_fac_div')).mpr _
     norm_cast at h_fac_div
     rw [mul_comm]
     exact h_fac_div

diff --git a/FormalBook/Chapter_06.lean b/FormalBook/Chapter_06.lean
@@ -134,7 +134,6 @@ lemma div_of_qpoly_div (k n q : ℕ) (hq : 1 < q) (hk : 0 < k) (hn : 0 < n)
   have : q ^ m - 1 = q^(m - k)*(q ^ k - 1) + (q^(m - k) - 1) := by
     zify
     simp [one_le_pow m q hq', one_le_pow k q hq', one_le_pow (m - k) q hq']
-    push_cast
     rw [mul_sub, mul_one]
     ring_nf
     simp only [ge_iff_le, add_right_inj]

diff --git a/FormalBook/Chapter_08.lean b/FormalBook/Chapter_08.lean
@@ -51,7 +51,7 @@ open BigOperators
 -/
 
 namespace book
-namespace irrational
+namespace Irrational
 
 /-- A real number is irrational if it is not rational. This is the same definition as in mathlib -/
 def irrational (x : ℝ) := x ∉ Set.range (fun (q : ℚ) => (q : ℝ))
@@ -143,5 +143,5 @@ theorem Theorem_3 (n : ℕ) (h_n : n ≥ 3) : irrational ( arccos (1 / (n : ℝ)
   sorry
 -/
 
-end irrational
+end Irrational
 end book
diff --git a/FormalBook/Chapter_44.lean b/FormalBook/Chapter_44.lean
@@ -114,7 +114,7 @@ theorem friendship_theorem [Nonempty V]
 
 
   -- Consider the adjacency matrix
-  let A := G.adjMatrix R
-  have : (A ^ 2) = (k - 1) • (1 : Matrix V V R) + of (fun _ _ => 1) := by sorry
+  let A := G.adjMatrix ℝ
+  have : (A ^ 2) = (k - 1) • (1 : Matrix V V ℝ) + of (fun _ _ => 1) := by sorry
 
   sorry
diff --git a/FormalBook/Chapter_45.lean b/FormalBook/Chapter_45.lean
@@ -15,14 +15,7 @@ limitations under the License.
 
 Authors: Moritz Firsching
 -/
-import Mathlib.Tactic
-import Mathlib.Data.Finset.Basic
-import Mathlib.Combinatorics.SimpleGraph.AdjMatrix
-import Mathlib.Combinatorics.SimpleGraph.Subgraph
-import Mathlib.Combinatorics.SimpleGraph.Coloring
-import Mathlib.Combinatorics.SimpleGraph.Connectivity
-import Mathlib.Order.WellFoundedSet
-import Mathlib.Data.Set.Basic
+import Mathlib.Combinatorics.SimpleGraph.Maps
 --import Mathlib.Analysis.SpecialFunctions.Exp
 --import Mathlib.Analysis.SpecialFunctions.Log.Base
 

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -1,10 +1,11 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "/~https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "14f258593e8c261d8834f13c6edc7b970c253ee8",
+   "scope": "leanprover-community",
+   "rev": "2ce0037d487217469a1efeb9ea8196fe15ab9c46",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +14,8 @@
   {"url": "/~https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
+   "scope": "leanprover-community",
+   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +24,8 @@
   {"url": "/~https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "f617e0673845925e612b62141ff54c4b7980dc63",
+   "scope": "leanprover-community",
+   "rev": "2c39748d927749624f480b641f1d2d77b8632b92",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,34 +34,48 @@
   {"url": "/~https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
+   "scope": "leanprover-community",
+   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.36",
+   "inputRev": "v0.0.42",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "/~https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "scope": "",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "/~https://github.com/leanprover-community/import-graph.git",
+   "configFile": "lakefile.toml"},
+  {"url": "/~https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "35e38eb320982cfd2fcc864e0e0467ca223c8cdb",
+   "scope": "leanprover-community",
+   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "/~https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "3e9460c40e09457b2fd079ef55316535536425fc",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "/~https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "aad19d883960cbdd1807a3c31ef7a351c3f0c733",
+   "scope": "",
+   "rev": "a98504654ef7be55256372c20fb12e889fc0d431",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -67,43 +84,48 @@
   {"url": "/~https://github.com/PatrickMassot/checkdecls.git",
    "type": "git",
    "subDir": null,
-   "rev": "88ec21589a8eef430f4ea01147cde1aaa7963e16",
+   "scope": "",
+   "rev": "11fa569b1b52f987dc5dcea97fd80eaff95c2fce",
    "name": "checkdecls",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "/~https://github.com/xubaiw/CMark.lean",
+  {"url": "/~https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,
-   "rev": "ba7b47bd773954b912ecbf5b1c9993c71a166f05",
-   "name": "CMark",
+   "scope": "",
+   "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
+   "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "/~https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,
-   "rev": "8b53cc65534bc2c6888c3d4c53a3439648213f74",
+   "scope": "",
+   "rev": "7afce91e4fcee25c1ed06dca8d71b82bed396776",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "/~https://github.com/hargonix/LeanInk",
+  {"url": "/~https://github.com/dupuisf/BibtexQuery",
    "type": "git",
    "subDir": null,
-   "rev": "f1f904e00d79a91ca6a76dec6e318531a7fd2a0f",
-   "name": "leanInk",
+   "scope": "",
+   "rev": "0a294fe9bf23b396c5cc955054c50b9b652ec5ad",
+   "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "doc-gen",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "/~https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
-   "rev": "b91fea210b7b6b451f19c6344d1f82765b9607af",
+   "scope": "",
+   "rev": "1b0072fea2aa6a0ef8ef8b506ec5223b184cb4d0",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc1
+leanprover/lean4:v4.12.0-rc1
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.8.0-rc1
		leanprover/lean4:v4.12.0-rc1