Merge branch 'master' into derived-set

Author: NoneMore

.github/workflows/build_template.yml

@@ -247,76 +247,6 @@ jobs:
             echo "✅ All inputRevs in lake-manifest.json are valid"
           fi
 
-      - name: validate ProofWidgets source repository
-        # Only enforce this on the main mathlib4 repository, not on nightly-testing
-        if: github.repository == 'leanprover-community/mathlib4'
-        shell: bash
-        run: |
-          cd pr-branch
-
-          expected_url='https://github.com/leanprover-community/ProofWidgets4'
-          proofwidgets_count=$(jq '[.packages[] | select(.name == "proofwidgets")] | length' lake-manifest.json)
-          if [ "$proofwidgets_count" -ne 1 ]; then
-            echo "❌ Error: expected exactly one proofwidgets entry in lake-manifest.json, found $proofwidgets_count"
-            exit 1
-          fi
-
-          proofwidgets_url=$(jq -r '.packages[] | select(.name == "proofwidgets") | .url' lake-manifest.json)
-          normalized_url="${proofwidgets_url%.git}"
-          if [ "$normalized_url" != "$expected_url" ]; then
-            echo "❌ Error: invalid ProofWidgets source URL in lake-manifest.json"
-            echo "  expected: $expected_url"
-            echo "  found:    $proofwidgets_url"
-            exit 1
-          fi
-
-          echo "✅ ProofWidgets source URL is allowed: $proofwidgets_url"
-
-      - name: verify ProofWidgets lean-toolchain matches on versioned releases
-        # Only enforce this on the main mathlib4 repository, not on nightly-testing
-        if: github.repository == 'leanprover-community/mathlib4'
-        shell: bash
-        run: |
-          cd pr-branch
-
-          # Read the lean-toolchain file
-          TOOLCHAIN=$(cat lean-toolchain | tr -d '[:space:]')
-          echo "Lean toolchain: $TOOLCHAIN"
-
-          # Check if toolchain matches the versioned release pattern: leanprover/lean4:vX.Y.Z (with optional suffix like -rc1)
-          if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?$ ]]; then
-            echo "✓ Detected versioned Lean release: $TOOLCHAIN"
-            echo "Verifying ProofWidgets lean-toolchain matches..."
-
-            # Check if ProofWidgets lean-toolchain exists
-            if [ ! -f .lake/packages/proofwidgets/lean-toolchain ]; then
-              echo "❌ Error: .lake/packages/proofwidgets/lean-toolchain does not exist"
-              echo "This file should be created by 'lake env' during dependency download."
-              exit 1
-            fi
-
-            # Read ProofWidgets lean-toolchain
-            PROOFWIDGETS_TOOLCHAIN=$(cat .lake/packages/proofwidgets/lean-toolchain | tr -d '[:space:]')
-            echo "ProofWidgets toolchain: $PROOFWIDGETS_TOOLCHAIN"
-
-            # Compare the two
-            if [ "$TOOLCHAIN" != "$PROOFWIDGETS_TOOLCHAIN" ]; then
-              echo "❌ Error: Lean toolchain mismatch!"
-              echo "  Main lean-toolchain: $TOOLCHAIN"
-              echo "  ProofWidgets lean-toolchain: $PROOFWIDGETS_TOOLCHAIN"
-              echo ""
-              echo "When using a versioned Lean release (leanprover/lean4:vX.Y.Z),"
-              echo "the ProofWidgets dependency must use the same toolchain."
-              echo "Please update the ProofWidgets dependency to use $TOOLCHAIN"
-              exit 1
-            else
-              echo "✅ ProofWidgets lean-toolchain matches: $TOOLCHAIN"
-            fi
-          else
-            echo "ℹ Lean toolchain is not a versioned release (pattern: leanprover/lean4:vX.Y.Z)"
-            echo "Skipping ProofWidgets toolchain verification."
-          fi
-
       - name: get cache (1/3 - setup and initial fetch)
         id: get_cache_part1_setup
         shell: bash # only runs `cache get` from `tools-branch`, so doesn't need to be inside landrun
@@ -327,7 +257,7 @@ jobs:
 
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
           echo "Attempting to fetch olean for Mathlib/Init.lean from cache..."
-          ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Mathlib/Init.lean
+          ../tools-branch/.lake/build/bin/cache get Mathlib/Init.lean
 
       - name: get cache (2/3 - test Mathlib.Init cache)
         id: get_cache_part2_test
@@ -381,9 +311,9 @@ jobs:
             echo "Warming up cache using previous commit: $PREV_SHA (source: $PREV_SHA_SOURCE)"
             if git cat-file -e "$PREV_SHA^{commit}" 2>/dev/null || git fetch --no-tags --depth=1 origin "$PREV_SHA"; then
               git checkout "$PREV_SHA"
-              ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get
+              ../tools-branch/.lake/build/bin/cache get
               # Run again with --repo, to ensure we actually get the oleans.
-              ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" --skip-proofwidgets get
+              ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" get
 
               echo "Switching back to branch head"
               git checkout "$ORIG_SHA"
@@ -396,18 +326,10 @@ jobs:
 
           echo "Fetching all remaining cache..."
 
-          ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get
+          ../tools-branch/.lake/build/bin/cache get
 
           # Run again with --repo, to ensure we actually get the oleans.
-          ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" --skip-proofwidgets get
-
-      - name: fetch ProofWidgets release
-        # We need network access for ProofWidgets frontend assets.
-        # Run inside landrun so PR-controlled code remains sandboxed.
-        shell: landrun --unrestricted-network --rox /etc --rox /usr --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rw pr-branch/.lake/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
-        run: |
-          cd pr-branch
-          lake build proofwidgets:release
+          ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" get
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
@@ -462,8 +384,8 @@ jobs:
         shell: bash
         run: |
           cd pr-branch
-          ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Archive.lean
-          ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Counterexamples.lean
+          ../tools-branch/.lake/build/bin/cache get Archive.lean
+          ../tools-branch/.lake/build/bin/cache get Counterexamples.lean
 
       - name: build archive
         id: archive
@@ -955,6 +877,7 @@ jobs:
             steps.get-label-actor.outputs.username == 'mathlib-update-dependencies' ||
             steps.get-label-actor.outputs.username == 'mathlib-splicebot' ||
             contains(steps.actorTeams.outputs.teams, 'mathlib-maintainers') ||
+            contains(steps.actorTeams.outputs.teams, 'lean-release-managers') ||
             contains(steps.actorTeams.outputs.teams, 'bot-users')
           )
         name: If `auto-merge-after-CI` is present, add a `bors merge` comment.

.github/workflows/maintainer_merge_wf_run.yml

@@ -150,7 +150,8 @@ jobs:
             legacy_suffix=" (legacy)"
           fi
           metadata=$'['"${trigger_name}"$']('"${trigger_run_url}"$'), [wf_run]('"${wf_run_url}"$')'"${legacy_suffix}"
-          message="${message}"$'\n\n---\n'"${metadata}"
+          echo "${metadata}"
+          # message="${message}"$'\n\n---\n'"${metadata}"
           printf 'title<<EOF\n%s\nEOF' "${message}" | tee "$GITHUB_OUTPUT"
         env:
           AUTHOR: ${{ steps.inputs.outputs.author }}
@@ -188,7 +189,8 @@ jobs:
             legacy_suffix=" (legacy)"
           fi
           metadata=$'['"${trigger_name}"$']('"${trigger_run_url}"$'), [wf_run]('"${wf_run_url}"$')'"${legacy_suffix}"
-          body="${body}"$'\n\n---\n'"${metadata}"
+          echo "${metadata}"
+          # body="${body}"$'\n\n---\n'"${metadata}"
           printf 'body<<EOF\n%s\nEOF\n' "${body}" | tee -a "$GITHUB_OUTPUT"
 
       - name: Add comment to PR

Archive/Imo/Imo2024Q3.lean

@@ -941,8 +941,6 @@ lemma exists_a_apply_add_eq : ∃ b c, 0 < c ∧ ∀ n, b < n →
     rcases hc.even_p (by lia) (hs n) with ⟨_, ht⟩
     simp [ht, ← two_mul]
 
-variable {a N}
-
 end Condition
 
 theorem result {a : ℕ → ℕ} {N : ℕ} (h : Condition a N) :

Cache/IO.lean

@@ -122,15 +122,12 @@ def rootHashGeneration : UInt64 := 4
   folders are located. However, `lake` has multiple options to customise these paths, like
   setting `srcDir` in a `lean_lib`. See `mkBuildPaths` below which currently assumes
   that no such options are set in any mathlib dependency)
-* the build directory for proofwidgets
 -/
 structure CacheM.Context where
   /-- source directory for mathlib files -/
   mathlibDepPath : FilePath
   /-- the Lean source search path -/
   srcSearchPath : SearchPath
-  /-- build directory for proofwidgets -/
-  proofWidgetsBuildDir : FilePath
 
 @[inherit_doc CacheM.Context]
 abbrev CacheM := ReaderT CacheM.Context IO
@@ -158,8 +155,7 @@ private def CacheM.getContext : IO CacheM.Context := do
   let mathlibSource ← CacheM.mathlibDepPath sp
   return {
     mathlibDepPath := mathlibSource,
-    srcSearchPath := sp,
-    proofWidgetsBuildDir := LAKEPACKAGESDIR / "proofwidgets" / ".lake" / "build"}
+    srcSearchPath := sp}
 
 /-- Run a `CacheM` in `IO` by loading the context from `LEAN_SRC_PATH`. -/
 def CacheM.run (f : CacheM α) : IO α := do ReaderT.run f (← getContext)

Cache/Main.lean

@@ -39,7 +39,6 @@ Commands:
 Options:
   --repo=OWNER/REPO  Override the repository to fetch/push cache from
   --staging-dir=<output-directory> Required for 'stage', 'stage!', 'unstage' and 'put-staged': staging directory.
-  --skip-proofwidgets  Skip fetching/building ProofWidgets release assets during 'get'
 
 * Linked files refer to local cache files with corresponding Lean sources
 * Commands ending with '!' should be used manually, when hot-fixes are needed
@@ -101,7 +100,6 @@ def main (args : List String) : IO Unit := do
   -- parse relevant options, ignore the rest
   let repo? ← parseNamedOpt "repo" options
   let stagingDir? ← parseNamedOpt "staging-dir" options
-  let skipProofWidgets := parseFlagOpt "skip-proofwidgets" options
 
   let mut roots : Std.HashMap Lean.Name FilePath ← parseArgs args
   if roots.isEmpty then do
@@ -118,7 +116,7 @@ def main (args : List String) : IO Unit := do
   if leanTarArgs.contains (args.headD "") then validateLeanTar
   let get (args : List String) (force := false) (decompress := true) := do
     let hashMap ← if args.isEmpty then pure hashMap else hashMemo.filterByRootModules roots.keys
-    getFiles repo? hashMap force force goodCurl decompress skipProofWidgets
+    getFiles repo? hashMap force force goodCurl decompress
   let pack (overwrite verbose unpackedOnly := false) := do
     packCache hashMap overwrite verbose unpackedOnly (← getGitCommitHash)
   let put (overwrite unpackedOnly := false) := do

Cache/Requests.lean

@@ -641,61 +641,15 @@ def checkForManifestMismatch : IO.CacheM Unit := do
         precedence, then run `lake update`."
     IO.Process.exit 1
 
-/-- Fetches the ProofWidgets cloud release and prunes non-JS files. -/
-def getProofWidgets (buildDir : FilePath) : IO Unit := do
-  if (← buildDir.pathExists) then
-    -- Check if the ProofWidgets build is out-of-date via `lake`.
-    -- This is done through Lake as cache has no simple heuristic
-    -- to determine whether the ProofWidgets JS is out-of-date.
-    let out ← IO.Process.output
-      {cmd := "lake", args := #["-v", "build", "--no-build", "proofwidgets:release"]}
-    if out.exitCode == 0 then -- up-to-date
-      return
-    else if out.exitCode == 3 then -- needs fetch (`--no-build` triggered)
-      pure ()
-    else
-      printLakeOutput out
-      throw <| IO.userError s!"Failed to validate ProofWidgets cloud release: \
-        lake failed with error code {out.exitCode}"
-  -- Download and unpack the ProofWidgets cloud release (for its `.js` files)
-  IO.print "Fetching ProofWidgets cloud release..."
-  let out ← IO.Process.output
-     {cmd := "lake", args := #["-v", "build", "proofwidgets:release"]}
-  if out.exitCode == 0 then
-    IO.println " done!"
-  else
-    IO.print "\n"
-    printLakeOutput out
-    throw <| IO.userError s!"Failed to fetch ProofWidgets cloud release: \
-      lake failed with error code {out.exitCode}"
-  -- Prune non-JS ProofWidgets files (e.g., `olean`, `.c`)
-  try
-    IO.FS.removeDirAll (buildDir / "lib")
-    IO.FS.removeDirAll (buildDir / "ir")
-  catch e =>
-    throw <| IO.userError s!"Failed to prune ProofWidgets cloud release: {e}"
-where
-  printLakeOutput out := do
-    unless out.stdout.isEmpty do
-      IO.eprintln "lake stdout:"
-      IO.eprint out.stdout
-    unless out.stderr.isEmpty do
-      IO.eprintln "lake stderr:"
-      IO.eprint out.stderr
-
 /-- Downloads missing files, and unpacks files. -/
 def getFiles
     (repo? : Option String) (hashMap : IO.ModuleHashMap)
-    (forceDownload forceUnpack parallel decompress skipProofWidgets : Bool)
+    (forceDownload forceUnpack parallel decompress : Bool)
     : IO.CacheM Unit := do
   let isMathlibRoot ← IO.isMathlibRoot
   unless isMathlibRoot do
     checkForToolchainMismatch
     checkForManifestMismatch
-  if skipProofWidgets then
-    IO.println "Skipping ProofWidgets release fetch"
-  else
-    getProofWidgets (← read).proofWidgetsBuildDir
 
   let mathlibDepPath := (← read).mathlibDepPath
 

Counterexamples/Phillips.lean

@@ -460,7 +460,7 @@ We need the continuum hypothesis to construct it.
 
 theorem sierpinski_pathological_family (Hcont : #ℝ = ℵ₁) :
     ∃ f : ℝ → Set ℝ, (∀ x, (univ \ f x).Countable) ∧ ∀ y, {x : ℝ | y ∈ f x}.Countable := by
-  rcases Cardinal.ord_eq ℝ with ⟨r, hr, H⟩
+  rcases Cardinal.exists_ord_eq ℝ with ⟨r, hr, H⟩
   refine ⟨fun x => {y | r x y}, fun x => ?_, fun y => ?_⟩
   · have : univ \ {y | r x y} = {y | r y x} ∪ {x} := by
       ext y
@@ -474,9 +474,9 @@ theorem sierpinski_pathological_family (Hcont : #ℝ = ℵ₁) :
       · simp only [h, iff_true, or_true]; exact asymm h
     rw [this]
     apply Countable.union _ (countable_singleton _)
-    rw [Cardinal.countable_iff_lt_aleph_one, ← Hcont]
+    rw [← Cardinal.le_aleph0_iff_set_countable, ← Cardinal.lt_aleph_one_iff, ← Hcont]
     exact Cardinal.card_typein_lt x H
-  · rw [Cardinal.countable_iff_lt_aleph_one, ← Hcont]
+  · rw [← Cardinal.le_aleph0_iff_set_countable, ← Cardinal.lt_aleph_one_iff, ← Hcont]
     exact Cardinal.card_typein_lt y H
 
 /-- A family of sets in `ℝ` which only miss countably many points, but such that any point is

Mathlib.lean

@@ -709,6 +709,7 @@ public import Mathlib.Algebra.Lie.Engel
 public import Mathlib.Algebra.Lie.EngelSubalgebra
 public import Mathlib.Algebra.Lie.Extension
 public import Mathlib.Algebra.Lie.Free
+public import Mathlib.Algebra.Lie.Graded
 public import Mathlib.Algebra.Lie.Ideal
 public import Mathlib.Algebra.Lie.IdealOperations
 public import Mathlib.Algebra.Lie.InvariantForm
@@ -822,6 +823,7 @@ public import Mathlib.Algebra.Module.Torsion.Basic
 public import Mathlib.Algebra.Module.Torsion.Field
 public import Mathlib.Algebra.Module.Torsion.Free
 public import Mathlib.Algebra.Module.Torsion.Pi
+public import Mathlib.Algebra.Module.Torsion.PrimaryComponent
 public import Mathlib.Algebra.Module.Torsion.Prod
 public import Mathlib.Algebra.Module.TransferInstance
 public import Mathlib.Algebra.Module.ULift
@@ -1613,6 +1615,7 @@ public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
+public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
@@ -1851,6 +1854,7 @@ public import Mathlib.Analysis.Convex.Exposed
 public import Mathlib.Analysis.Convex.Extrema
 public import Mathlib.Analysis.Convex.Extreme
 public import Mathlib.Analysis.Convex.Function
+public import Mathlib.Analysis.Convex.FunctionTopology
 public import Mathlib.Analysis.Convex.Gauge
 public import Mathlib.Analysis.Convex.GaugeRescale
 public import Mathlib.Analysis.Convex.Hull
@@ -1902,6 +1906,7 @@ public import Mathlib.Analysis.Distribution.SchwartzSpace
 public import Mathlib.Analysis.Distribution.SchwartzSpace.Basic
 public import Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
 public import Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
+public import Mathlib.Analysis.Distribution.Support
 public import Mathlib.Analysis.Distribution.TemperateGrowth
 public import Mathlib.Analysis.Distribution.TemperedDistribution
 public import Mathlib.Analysis.Distribution.TestFunction
@@ -2150,6 +2155,7 @@ public import Mathlib.Analysis.Normed.Order.Lattice
 public import Mathlib.Analysis.Normed.Order.UpperLower
 public import Mathlib.Analysis.Normed.Ring.Basic
 public import Mathlib.Analysis.Normed.Ring.Finite
+public import Mathlib.Analysis.Normed.Ring.InfiniteProd
 public import Mathlib.Analysis.Normed.Ring.InfiniteSum
 public import Mathlib.Analysis.Normed.Ring.Int
 public import Mathlib.Analysis.Normed.Ring.Lemmas
@@ -5571,6 +5577,7 @@ public import Mathlib.NumberTheory.ModularForms.Cusps
 public import Mathlib.NumberTheory.ModularForms.DedekindEta
 public import Mathlib.NumberTheory.ModularForms.Delta
 public import Mathlib.NumberTheory.ModularForms.Derivative
+public import Mathlib.NumberTheory.ModularForms.Discriminant
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
@@ -6655,6 +6662,7 @@ public import Mathlib.RingTheory.Regular.Depth
 public import Mathlib.RingTheory.Regular.Flat
 public import Mathlib.RingTheory.Regular.IsSMulRegular
 public import Mathlib.RingTheory.Regular.RegularSequence
+public import Mathlib.RingTheory.RegularLocalRing.Defs
 public import Mathlib.RingTheory.RingHom.Bijective
 public import Mathlib.RingTheory.RingHom.EssFiniteType
 public import Mathlib.RingTheory.RingHom.Etale