Update to v4.33.x

lean4/lake-manifest.json

@@ -1,21 +1,21 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900",
+   "rev": "0df444a360eaa60ab8c11dca51a86af692955474",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0",
+   "inputRev": "v4.33.1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f",
+   "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
+   "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8f497d55985a189cea8020d9dc51260af1e41ad2",
+   "rev": "16f02aa7642864af59f1ff0e384a015994db9118",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c04225ee7c0585effbd933662b3151f01b600e40",
+   "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.85",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d",
+   "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c",
+   "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
+   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,11 +85,12 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "55c37290ff6186e2e965d68cf853a57c0702db82",
+   "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0",
+   "inputRev": "v4.33.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "putnam",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

lean4/lakefile.lean

@@ -6,7 +6,7 @@ package «putnam» where
   leanOptions := #[
     ⟨`autoImplicit, false⟩
   ]
-require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.27.0"
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.33.1"
 
 @[default_target]
 lean_lib «putnam» where

lean4/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.27.0
+leanprover/lean4:v4.33.1

lean4/src/putnam_1966_b5.lean

@@ -8,7 +8,7 @@ Prove that any set of $n \ge 3$ distinct points in the Euclidean plane, no three
 theorem putnam_1966_b5
 (S : Finset (EuclideanSpace ℝ (Fin 2)))
 (hcard : S.card ≥ 3)
-(hS : ∀ s ⊆ S, s.card = 3 → ¬Collinear ℝ s.toSet)
+(hS : ∀ s ⊆ S, s.card = 3 → ¬Collinear ℝ (s : Set (EuclideanSpace ℝ (Fin 2))))
 : ∃ L : ZMod S.card → (EuclideanSpace ℝ (Fin 2)), (∀ p ∈ S, ∃! i : ZMod S.card, p = L i) ∧
 ∀ i j : ZMod S.card, i ≠ j → (∀ I : EuclideanSpace ℝ (Fin 2),
 (I ∈ segment ℝ (L i) (L (i + 1)) ∧ I ∈ segment ℝ (L j) (L (j + 1))) →

lean4/src/putnam_1976_b1.lean

@@ -9,5 +9,5 @@ Find $$\lim_{n \to \infty} \frac{1}{n} \sum_{k=1}^{n}\left(\left\lfloor \frac{2n
 -/
 theorem putnam_1976_b1
 : Tendsto (fun n : ℕ => ((1 : ℝ)/n)*∑ k ∈ Finset.Icc (1 : ℤ) n, (Int.floor ((2*n)/k) - 2*Int.floor (n/k))) atTop
-(𝓝 (Real.log putnam_1976_b1_solution.1 - putnam_1976_b1_solution.2)) :=
+    (𝓝 (Real.log putnam_1976_b1_solution.1 - putnam_1976_b1_solution.2)) :=
 sorry