Merge remote-tracking branch 'upstream/master' into bump/v4.32.0

Author: mathlib4-bot

.github/actions/get-mathlib-ci/action.yml

@@ -10,7 +10,7 @@ inputs:
     # Default pinned commit used by workflows unless they explicitly override.
     # Update this ref as needed to pick up changes to mathlib-ci scripts
     # This is also updated automatically by .github/workflows/update_dependencies.yml
-    default: e7a159e9a129f92fd07e6852a742485798678473
+    default: 4db29a340d585b5ca9cc45ba5b951a3939753d53
   path:
     description: Checkout destination path.
     required: false

.github/workflows/PR_summary.yml

@@ -213,10 +213,16 @@ jobs:
         declDiff=$("${CI_SCRIPTS_DIR}/pr_summary/declarations_diff.sh")
         if [ "$(printf '%s' "${declDiff}" | wc -l)" -gt 15 ]
         then
-          declDiff="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Declarations diff" "${declDiff}")"
+          declDiff="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Declarations diff (regex)" "${declDiff}")"
         else
-          declDiff="$(printf '#### Declarations diff\n\n%s\n' "${declDiff}")"
+          declDiff="$(printf '#### Declarations diff (regex)\n\n%s\n' "${declDiff}")"
         fi
+        # Append a placeholder for the post-build, Lean-aware diff. The
+        # `decls-diff.yml` workflow replaces the region between the markers (see
+        # mathlib-ci's `updateDeclsDiffSection.py`); the regex block above is left
+        # as-is. The markers are HTML comments (invisible when rendered), and the
+        # heading carries the status (`pending` → `(Lean)` / `(Lean -- unavailable)`).
+        declDiff="$(printf '%s\n\n<!-- DECLS_DIFF_LEAN_BEGIN -->\n#### Declarations diff (Lean -- pending)\n\n_Computed after the build finishes._\n<!-- DECLS_DIFF_LEAN_END -->\n' "${declDiff}")"
         git checkout "${currentHash}" --
         hashURL="https://github.com/${{ github.repository }}/pull/${{ github.event.pull_request.number }}/commits/${currentHash}"
         printf 'hashURL: %s' "${hashURL}"

.github/workflows/build_template.yml

@@ -767,6 +767,21 @@ jobs:
         run: |
           lake env lean --run "${CI_SCRIPTS_DIR}/pr_summary/dumpReasonableDecls.lean" \
             --out decls.txt --imports-out imports.json Mathlib
+          ## Record the PR number so the post-build `decls-diff` workflow can find
+          ## the comment to patch without the (laggy) commit-SHA search API. Empty
+          ## for non-PR builds (push to master / bors); the consumer then falls
+          ## back to the commit's associated PRs.
+          printf '%s' "${{ github.event.pull_request.number }}" > pr_number.txt
+
+      - name: ensure dump outputs are regular files
+        run: |
+          for f in decls.txt imports.json import_graph.dot pr_number.txt; do
+            if [ -L "$f" ] || [ ! -f "$f" ]; then
+              echo "Refusing to upload: $f is not a regular file." >&2
+              ls -la -- "$f" >&2 || true
+              exit 1
+            fi
+          done
 
       - name: upload the import graph
         uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
@@ -776,12 +791,13 @@ jobs:
             import_graph.dot
             decls.txt
             imports.json
+            pr_number.txt
           ## Master pushes: 90 days, so later PRs forked from these commits
           ## can consume the dumps from the artifact. Other branches: 7 days.
           retention-days: ${{ github.ref == 'refs/heads/master' && '90' || '7' }}
 
       - name: clean up the import graph file
-        run: rm -f import_graph.dot decls.txt imports.json
+        run: rm -f import_graph.dot decls.txt imports.json pr_number.txt
 
       - name: check all scripts build successfully
         run: |

.github/workflows/decls-diff.yml

@@ -1,10 +1,10 @@
-# Post-build workflow that emits a Lean-aware declarations-diff in the Actions
-# step summary for each successful PR build. Consumes the `import-graph`
-# artifact uploaded by `build_template.yml` on both sides (PR head + master
-# merge-base) and computes the diff via mathlib-ci's `decls-diff` action.
-#
-# Stage-2 scope: visibility only. No `### PR summary` comment patching; that
-# behaviour ships in a follow-up PR.
+# Post-build workflow that patches the `### PR summary` comment with a
+# Lean-aware declarations diff after each successful PR build. Consumes the
+# `import-graph` artifact uploaded by `build_template.yml` on both sides
+# (PR head + master merge-base), computes the diff via mathlib-ci's
+# `decls-diff` action, and replaces the `#### Declarations diff (Lean ...)`
+# region of the comment (the regex block is left untouched). On a cache miss
+# it marks that region unavailable instead.
 
 name: Declarations diff (post-build)
 
@@ -15,9 +15,16 @@ on:
     workflows: ["continuous integration", "continuous integration (mathlib forks)"]
     types: [completed]
 
+# Per upstream PR (repo + branch), keep only the latest post-build run so rapid
+# pushes don't race to patch the comment with a stale diff.
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.workflow_run.head_repository.full_name }}-${{ github.event.workflow_run.head_branch }}
+  cancel-in-progress: true
+
 permissions:
   contents: read
   actions: read           # for cross-workflow artifact downloads
+  pull-requests: write    # for PATCHing the `### PR summary` comment
 
 jobs:
   diff:
@@ -74,6 +81,23 @@ jobs:
           run-id: ${{ steps.meta.outputs.run-id }}
           github-token: ${{ secrets.GITHUB_TOKEN }}
 
+      - name: Resolve PR number
+        id: pr
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          REPO: ${{ github.repository }}
+          NEW_SHA: ${{ steps.meta.outputs.new-sha }}
+        run: |
+          set -euo pipefail
+          # The build records the PR number in the artifact — reliable for fork
+          # PRs, where the commit-SHA search API lags or misses. Fall back to the
+          # commit's associated PRs for same-repo pushes (commit is on this repo).
+          PR_NUMBER="$(tr -dc '0-9' < ./new-artifact/pr_number.txt 2>/dev/null || true)"
+          if [ -z "$PR_NUMBER" ]; then
+            PR_NUMBER="$(gh api "repos/$REPO/commits/$NEW_SHA/pulls" --jq '.[0].number // empty')"
+          fi
+          echo "pr-number=$PR_NUMBER" | tee -a "$GITHUB_OUTPUT"
+
       - name: Find master Build for the merge-base
         id: master-run
         env:
@@ -109,8 +133,9 @@ jobs:
           run-id: ${{ steps.master-run.outputs.run-id }}
           github-token: ${{ secrets.GITHUB_TOKEN }}
 
+      # Tooling is checked out unconditionally: the patcher (from CI_SCRIPTS_DIR)
+      # is needed on the cache-miss path too, to post the warning notice.
       - name: Checkout local actions
-        if: steps.master-run.outputs.found == 'true'
         uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
         with:
           ref: ${{ github.workflow_sha }}
@@ -119,24 +144,47 @@ jobs:
           path: workflow-actions
 
       - name: Get mathlib-ci
-        if: steps.master-run.outputs.found == 'true'
         uses: ./workflow-actions/.github/actions/get-mathlib-ci
 
       - name: Compute Lean-aware declarations diff
         if: steps.master-run.outputs.found == 'true'
+        id: diff
         uses: ./ci-tools/.github/actions/decls-diff
         with:
           reference-decls-file:   ${{ github.workspace }}/ref-artifact/decls.txt
           reference-imports-file: ${{ github.workspace }}/ref-artifact/imports.json
           new-decls-file:         ${{ github.workspace }}/new-artifact/decls.txt
           new-imports-file:       ${{ github.workspace }}/new-artifact/imports.json
           new-sha:                ${{ steps.meta.outputs.new-sha }}
+          with-heading:           'true'
+
+      - name: Patch PR summary comment (success)
+        if: steps.master-run.outputs.found == 'true'
+        env:
+          GH_TOKEN:      ${{ secrets.GITHUB_TOKEN }}
+          REPO:          ${{ github.repository }}
+          PR_HEAD_SHA:   ${{ steps.meta.outputs.new-sha }}
+          PR_NUMBER:     ${{ steps.pr.outputs.pr-number }}
+          MODE:          success
+          OVERRIDE_FILE: ${{ steps.diff.outputs.decls-override-file }}
+        run: python3 "$CI_SCRIPTS_DIR/pr_summary/updateDeclsDiffSection.py"
 
       - name: Note cache miss
         if: steps.master-run.outputs.found != 'true'
+        env:
+          GH_TOKEN:       ${{ secrets.GITHUB_TOKEN }}
+          REPO:           ${{ github.repository }}
+          PR_HEAD_SHA:    ${{ steps.meta.outputs.new-sha }}
+          PR_NUMBER:      ${{ steps.pr.outputs.pr-number }}
+          MODE:           warning
+          DEFAULT_BRANCH: master
         run: |
+          # Record the cache miss in the step summary first, so a later patcher
+          # error (e.g. a transient GitHub failure) still leaves this run-local
+          # note; then mark the comment's Lean region unavailable.
           {
             echo "## Declarations diff"
             echo
             echo "⚠️ The Mathlib cache for this PR's merge-base \`${{ steps.resolve.outputs.merge-base }}\` isn't on the server (typically because the merge-base is a bors-batch intermediate that CI never built). Merge \`master\` into this PR and push to retrigger the build."
           } >> "$GITHUB_STEP_SUMMARY"
+          python3 "$CI_SCRIPTS_DIR/pr_summary/updateDeclsDiffSection.py"

Counterexamples/HomogeneousPrimeNotPrime.lean

@@ -5,7 +5,7 @@ Authors: Johan Commelin, Eric Wieser, Jujian Zhang
 -/
 import Mathlib.Algebra.Divisibility.Finite
 import Mathlib.Algebra.Divisibility.Prod
-import Mathlib.Data.Fintype.Units
+import Mathlib.Algebra.GroupWithZero.Units.Fintype
 import Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
 
 /-!

Mathlib.lean

@@ -552,6 +552,7 @@ public import Mathlib.Algebra.GroupWithZero.TransferInstance
 public import Mathlib.Algebra.GroupWithZero.ULift
 public import Mathlib.Algebra.GroupWithZero.Units.Basic
 public import Mathlib.Algebra.GroupWithZero.Units.Equiv
+public import Mathlib.Algebra.GroupWithZero.Units.Fintype
 public import Mathlib.Algebra.GroupWithZero.Units.Lemmas
 public import Mathlib.Algebra.GroupWithZero.WithZero
 public import Mathlib.Algebra.HierarchyDesign
@@ -1485,6 +1486,7 @@ public import Mathlib.AlgebraicTopology.DoldKan.Notations
 public import Mathlib.AlgebraicTopology.DoldKan.PInfty
 public import Mathlib.AlgebraicTopology.DoldKan.Projections
 public import Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
+public import Mathlib.AlgebraicTopology.EilenbergSteenrod
 public import Mathlib.AlgebraicTopology.ExtraDegeneracy
 public import Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
 public import Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
@@ -1553,6 +1555,7 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUnique
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
+public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
@@ -1585,6 +1588,7 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.Nerve
 public import Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
 public import Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
 public import Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
+public import Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit
 public import Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
 public import Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
 public import Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
@@ -2166,6 +2170,7 @@ public import Mathlib.Analysis.Normed.Lp.PiLp
 public import Mathlib.Analysis.Normed.Lp.ProdLp
 public import Mathlib.Analysis.Normed.Lp.SmoothApprox
 public import Mathlib.Analysis.Normed.Lp.WithLp
+public import Mathlib.Analysis.Normed.Lp.lpHolder
 public import Mathlib.Analysis.Normed.Lp.lpSpace
 public import Mathlib.Analysis.Normed.Module.Alternating.Basic
 public import Mathlib.Analysis.Normed.Module.Alternating.Curry
@@ -3067,6 +3072,7 @@ public import Mathlib.CategoryTheory.Monoidal.Bimon_
 public import Mathlib.CategoryTheory.Monoidal.Braided.Basic
 public import Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
 public import Mathlib.CategoryTheory.Monoidal.Braided.Opposite
+public import Mathlib.CategoryTheory.Monoidal.Braided.PushoutObjObj
 public import Mathlib.CategoryTheory.Monoidal.Braided.Reflection
 public import Mathlib.CategoryTheory.Monoidal.Braided.Transport
 public import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
@@ -3661,6 +3667,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
 public import Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
 public import Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
 public import Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
+public import Mathlib.Combinatorics.SimpleGraph.Star
 public import Mathlib.Combinatorics.SimpleGraph.StronglyRegular
 public import Mathlib.Combinatorics.SimpleGraph.Subgraph
 public import Mathlib.Combinatorics.SimpleGraph.Sum
@@ -3853,7 +3860,6 @@ public import Mathlib.Data.Fin.Tuple.Take
 public import Mathlib.Data.Fin.VecNotation
 public import Mathlib.Data.FinEnum
 public import Mathlib.Data.FinEnum.Option
-public import Mathlib.Data.Finite.Card
 public import Mathlib.Data.Finite.Defs
 public import Mathlib.Data.Finite.Perm
 public import Mathlib.Data.Finite.Prod
@@ -3972,7 +3978,6 @@ public import Mathlib.Data.Fintype.Shrink
 public import Mathlib.Data.Fintype.Sigma
 public import Mathlib.Data.Fintype.Sort
 public import Mathlib.Data.Fintype.Sum
-public import Mathlib.Data.Fintype.Units
 public import Mathlib.Data.Fintype.Vector
 public import Mathlib.Data.Fintype.WithTopBot
 public import Mathlib.Data.FunLike.Basic
@@ -4085,19 +4090,14 @@ public import Mathlib.Data.List.TakeWhile
 public import Mathlib.Data.List.ToFinsupp
 public import Mathlib.Data.List.Triplewise
 public import Mathlib.Data.List.Zip
-public import Mathlib.Data.Matrix.Action
 public import Mathlib.Data.Matrix.Auto
 public import Mathlib.Data.Matrix.Basic
 public import Mathlib.Data.Matrix.Basis
-public import Mathlib.Data.Matrix.Bilinear
 public import Mathlib.Data.Matrix.Block
-public import Mathlib.Data.Matrix.Cartan
 public import Mathlib.Data.Matrix.ColumnRowPartitioned
 public import Mathlib.Data.Matrix.Composition
 public import Mathlib.Data.Matrix.DMatrix
 public import Mathlib.Data.Matrix.Diagonal
-public import Mathlib.Data.Matrix.DualNumber
-public import Mathlib.Data.Matrix.Invertible
 public import Mathlib.Data.Matrix.Mul
 public import Mathlib.Data.Matrix.PEquiv
 public import Mathlib.Data.Matrix.Reflection
@@ -4273,7 +4273,6 @@ public import Mathlib.Data.QPF.Multivariate.Constructions.Sigma
 public import Mathlib.Data.QPF.Univariate.Basic
 public import Mathlib.Data.Quot
 public import Mathlib.Data.Rat.BigOperators
-public import Mathlib.Data.Rat.Cardinal
 public import Mathlib.Data.Rat.Cast.CharZero
 public import Mathlib.Data.Rat.Cast.Defs
 public import Mathlib.Data.Rat.Cast.Lemmas
@@ -4547,7 +4546,9 @@ public import Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
 public import Mathlib.Geometry.Convex.ConvexSpace.Defs
 public import Mathlib.Geometry.Convex.ConvexSpace.Module
 public import Mathlib.Geometry.Convex.ConvexSpace.Prod
+public import Mathlib.Geometry.Convex.Hull
 public import Mathlib.Geometry.Convex.Set
+public import Mathlib.Geometry.Convex.Star
 public import Mathlib.Geometry.Diffeology.Basic
 public import Mathlib.Geometry.Euclidean.Altitude
 public import Mathlib.Geometry.Euclidean.Angle.Bisector
@@ -5038,11 +5039,14 @@ public import Mathlib.LinearAlgebra.LinearIndependent.Defs
 public import Mathlib.LinearAlgebra.LinearIndependent.Lemmas
 public import Mathlib.LinearAlgebra.LinearPMap
 public import Mathlib.LinearAlgebra.Matrix.AbsoluteValue
+public import Mathlib.LinearAlgebra.Matrix.Action
 public import Mathlib.LinearAlgebra.Matrix.Adjugate
 public import Mathlib.LinearAlgebra.Matrix.BaseChange
 public import Mathlib.LinearAlgebra.Matrix.Basis
+public import Mathlib.LinearAlgebra.Matrix.Bilinear
 public import Mathlib.LinearAlgebra.Matrix.BilinearForm
 public import Mathlib.LinearAlgebra.Matrix.Block
+public import Mathlib.LinearAlgebra.Matrix.Cartan
 public import Mathlib.LinearAlgebra.Matrix.CharP
 public import Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
 public import Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
@@ -5061,6 +5065,7 @@ public import Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
 public import Mathlib.LinearAlgebra.Matrix.Diagonal
 public import Mathlib.LinearAlgebra.Matrix.DotProduct
 public import Mathlib.LinearAlgebra.Matrix.Dual
+public import Mathlib.LinearAlgebra.Matrix.DualNumber
 public import Mathlib.LinearAlgebra.Matrix.FiniteDimensional
 public import Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
 public import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
@@ -5076,6 +5081,7 @@ public import Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus
 public import Mathlib.LinearAlgebra.Matrix.Ideal
 public import Mathlib.LinearAlgebra.Matrix.Integer
 public import Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
+public import Mathlib.LinearAlgebra.Matrix.Invertible
 public import Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
 public import Mathlib.LinearAlgebra.Matrix.IsDiag
 public import Mathlib.LinearAlgebra.Matrix.Kronecker
@@ -6185,6 +6191,7 @@ public import Mathlib.Probability.CondVar
 public import Mathlib.Probability.ConditionalExpectation
 public import Mathlib.Probability.ConditionalProbability
 public import Mathlib.Probability.Decision.Risk.Basic
+public import Mathlib.Probability.Decision.Risk.Countable
 public import Mathlib.Probability.Decision.Risk.Defs
 public import Mathlib.Probability.Density
 public import Mathlib.Probability.Distributions.Bernoulli
@@ -7058,10 +7065,12 @@ public import Mathlib.SetTheory.Cardinal.Finite
 public import Mathlib.SetTheory.Cardinal.Finsupp
 public import Mathlib.SetTheory.Cardinal.Free
 public import Mathlib.SetTheory.Cardinal.HasCardinalLT
+public import Mathlib.SetTheory.Cardinal.NatCard
 public import Mathlib.SetTheory.Cardinal.NatCount
 public import Mathlib.SetTheory.Cardinal.Order
 public import Mathlib.SetTheory.Cardinal.Ordinal
 public import Mathlib.SetTheory.Cardinal.Pigeonhole
+public import Mathlib.SetTheory.Cardinal.Rat
 public import Mathlib.SetTheory.Cardinal.Regular
 public import Mathlib.SetTheory.Cardinal.SchroederBernstein
 public import Mathlib.SetTheory.Cardinal.Subfield
@@ -7854,6 +7863,7 @@ public import Mathlib.Topology.LocallyConstant.Algebra
 public import Mathlib.Topology.LocallyConstant.Basic
 public import Mathlib.Topology.LocallyFinite
 public import Mathlib.Topology.LocallyFinsupp
+public import Mathlib.Topology.LocallyFinsupp.Pushforward
 public import Mathlib.Topology.Maps.Basic
 public import Mathlib.Topology.Maps.OpenQuotient
 public import Mathlib.Topology.Maps.Proper.Basic