Update to Lean 4.11.0

The changes to the five files: * `putnam_1965_a5.lean` * `putnam_1985_b1.lean` * `putnam_1994_a6.lean` * `putnam_2011_b6.lean` * `putnam_2016_b2.lean` are fixes to account for the fact that Lean now tries to interpret certain expressions of the form `{ ... }.ncard` using `Finset.ncard` (which does not exist) rather than `Set.ncard`. Similar remarks for `Set.encard`. I have changed these to use `Finset.card`.
trishullab · Oct 7, 2024 · 26a8ffe · 26a8ffe
1 parent 737065d
commit 26a8ffe
Show file tree

Hide file tree

Showing 9 changed files with 17 additions and 18 deletions.
diff --git a/lean4/check_docstrings.lean b/lean4/check_docstrings.lean
@@ -1,6 +1,5 @@
 import Mathlib.Lean.CoreM
 import Mathlib.Util.GetAllModules
-import Batteries.Lean.Util.Path
 import Lean.Elab.Frontend
 import Batteries.Data.String.Matcher
 

diff --git a/lean4/lake-manifest.json b/lean4/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0",
+   "rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "01ad33937acd996ee99eb74eefb39845e4e4b9f5",
+   "rev": "9d0bdd07bdfe53383567509348b1fe917fc08de4",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "209712c78b16c795453b6da7f7adbda4589a8f21",
+   "rev": "deb279eb7be16848d0bc8387f80d6e41bcdbe738",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c87908619cccadda23f71262e6898b9893bffa36",
+   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.40",
+   "inputRev": "v0.0.41",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "543725b3bfed792097fc134adca628406f6145f5",
+   "rev": "1ef0b288623337cb37edd1222b9c26b4b77c6620",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,10 +65,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a719ba5c3115d47b68bf0497a9dd1bcbb21ea663",
+   "rev": "20c73142afa995ac9c8fb80a9bb585a55ca38308",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.10.0",
+   "inputRev": "v4.11.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "putnam",

diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean
@@ -6,7 +6,7 @@ package «putnam» where
   leanOptions := #[
     ⟨`autoImplicit, false⟩
   ]
-require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.10.0"
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.11.0"
 
 @[default_target]
 lean_lib «putnam» where

diff --git a/lean4/lean-toolchain b/lean4/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.10.0
+leanprover/lean4:v4.11.0
diff --git a/lean4/src/putnam_1965_a5.lean b/lean4/src/putnam_1965_a5.lean
@@ -9,5 +9,5 @@ abbrev putnam_1965_a5_solution : ℕ → ℕ := sorry
 How many orderings of the integers from $1$ to $n$ satisfy the condition that, for every integer $i$ except the first, there exists some earlier integer in the ordering which differs from $i$ by $1$?
 -/
 theorem putnam_1965_a5
-: ∀ n > 0, {p ∈ permsOfFinset (Finset.Icc 1 n) | ∀ m ∈ Finset.Icc 2 n, ∃ k ∈ Finset.Ico 1 m, p m = p k + 1 ∨ p m = p k - 1}.ncard = putnam_1965_a5_solution n :=
+: ∀ n > 0, {p ∈ permsOfFinset (Finset.Icc 1 n) | ∀ m ∈ Finset.Icc 2 n, ∃ k ∈ Finset.Ico 1 m, p m = p k + 1 ∨ p m = p k - 1}.card = putnam_1965_a5_solution n :=
 sorry
diff --git a/lean4/src/putnam_1985_b1.lean b/lean4/src/putnam_1985_b1.lean
@@ -16,6 +16,6 @@ theorem putnam_1985_b1
 (p : (Fin 5 → ℤ) → (Polynomial ℝ))
 (hp : p = fun m ↦ ∏ i : Fin 5, ((X : Polynomial ℝ) - m i))
 (numnzcoeff : Polynomial ℝ → ℕ)
-(hnumnzcoeff : numnzcoeff = fun p ↦ {j ∈ Finset.range (p.natDegree + 1) | coeff p j ≠ 0}.ncard)
+(hnumnzcoeff : numnzcoeff = fun p ↦ {j ∈ Finset.range (p.natDegree + 1) | coeff p j ≠ 0}.card)
 : (Injective putnam_1985_b1_solution ∧ ∀ m : Fin 5 → ℤ, Injective m → numnzcoeff (p putnam_1985_b1_solution) ≤ numnzcoeff (p m)) :=
 sorry
diff --git a/lean4/src/putnam_1994_a6.lean b/lean4/src/putnam_1994_a6.lean
@@ -1,7 +1,7 @@
 import Mathlib
 open BigOperators
 
-open Filter Topology
+open Classical Filter Topology
 
 -- Note: uses (ℕ → Fin 10) instead of (Fin m → Fin 10)
 /--
@@ -14,5 +14,5 @@ theorem putnam_1994_a6
 (hf: ∀ n : ℤ, ∃ m : ℕ, ∃ i : ℕ → Fin 10, m ≥ 1 ∧ (mijcomp m i 0) 0 = n)
 (hmijcomp : ∀ m ≥ 1, ∀ (i : ℕ → Fin 10) (j : Fin m), mijcomp m i j = if (j = m - 1) then (f (i j) : ℤ → ℤ) else (f (i j) ∘ mijcomp m i (j + 1)))
 (hF : F = {g : ℤ → ℤ | ∃ e : Fin 10 → Fin 2, g = (f 0)^[e 0] ∘ (f 1)^[e 1] ∘ (f 2)^[e 2] ∘ (f 3)^[e 3] ∘ (f 4)^[e 4] ∘ (f 5)^[e 5] ∘ (f 6)^[e 6] ∘ (f 7)^[e 7] ∘ (f 8)^[e 8] ∘ (f 9)^[e 9]})
-: ∀ A : Finset ℤ, A.Nonempty → {g ∈ F | g '' A = A}.encard ≤ 512 :=
+: ∀ A : Finset ℤ, A.Nonempty → {g ∈ F | g '' A = A}.card ≤ 512 :=
 sorry
diff --git a/lean4/src/putnam_2011_b6.lean b/lean4/src/putnam_2011_b6.lean
@@ -12,5 +12,5 @@ Let $p$ be an odd prime. Show that for at least $(p+1)/2$ values of $n$ in $\{0,
 theorem putnam_2011_b6
 (p : ℕ)
 (hp : Odd p ∧ Nat.Prime p)
-: {n ∈ Finset.range p | ¬ p ∣ ∑ k : Finset.range p, Nat.factorial k * n^(k : ℕ)}.ncard ≥ (p + 1)/2 :=
+: {n ∈ Finset.range p | ¬ p ∣ ∑ k : Finset.range p, Nat.factorial k * n^(k : ℕ)}.card ≥ (p + 1)/2 :=
 sorry
diff --git a/lean4/src/putnam_2016_b2.lean b/lean4/src/putnam_2016_b2.lean
@@ -1,7 +1,7 @@
 import Mathlib
 open BigOperators
 
-open Polynomial Filter Topology Real Set Nat List
+open Classical Polynomial Filter Topology Real Set Nat List
 
 noncomputable abbrev putnam_2016_b2_solution : ℝ × ℝ := sorry
 -- (3 / 4, 4 / 3)
@@ -19,7 +19,7 @@ theorem putnam_2016_b2
 (squarish : ℤ → Prop)
 (hsquarish : squarish = fun n ↦ IsSquare n ∨ ∃ w : ℤ, IsSquare |n - w ^ 2| ∧ ∀ v : ℕ, |n - w ^ 2| ≤ |n - v ^ 2|)
 (S : ℤ → ℕ)
-(hS : S = fun n ↦ {i ∈ Finset.Icc 1 n | squarish i}.ncard)
+(hS : S = fun n ↦ {i ∈ Finset.Icc 1 n | squarish i}.card)
 (p : ℝ → ℝ → Prop)
 (hp : p = fun α ↦ fun β ↦ α > 0 ∧ β > 0 ∧ Tendsto (fun N ↦ S N / (N : ℝ) ^ α) atTop (𝓝 β))
 : ((∀ α β : ℝ, ((α, β) = putnam_2016_b2_solution ↔ p α β)) ∨ ¬∃ α β : ℝ, p α β) :=