Merge master into nightly-testing

Author: mathlib-nightly-testing[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: 06beacf5884fb7242468c573c8fede0095552b53
+    default: e7a159e9a129f92fd07e6852a742485798678473
   path:
     description: Checkout destination path.
     required: false

.github/workflows/PR_summary.yml

@@ -22,6 +22,8 @@ jobs:
         ref: ${{ github.event.pull_request.head.sha }}
         fetch-depth: 0
         path: pr-branch
+        # Untrusted (potentially fork) checkout: don't persist the GITHUB_TOKEN into its .git/config.
+        persist-credentials: false
 
     - name: Checkout local actions
       uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2

.github/workflows/add_label_from_diff.yaml

@@ -43,6 +43,8 @@ jobs:
         ref: ${{ github.event.pull_request.head.sha || github.sha }}
         fetch-depth: 0
         path: pr-branch
+        # Untrusted (potentially fork) checkout: don't persist the GITHUB_TOKEN into its .git/config.
+        persist-credentials: false
     - name: Run autolabel
       working-directory: pr-branch
       run: |

.github/workflows/bot_fix_style.yaml

@@ -12,6 +12,14 @@ on:
     # triggers on a review comment
     types: [created, edited]
 
+# `lint-style-action` in `fix` mode pushes a style-fix commit and reacts/comments
+# on the PR. Grant exactly those scopes rather than inheriting the default token
+# permissions; all other scopes are implicitly 'none'.
+permissions:
+  contents: write       # push the style-fix commit to the PR branch
+  pull-requests: write  # add the bot's reaction/comment
+  issues: write         # PR comment reactions go through the issues API
+
 jobs:
   fix_style:
     # we set some variables. The ones of the form `${{ X }}${{ Y }}` are typically not

.github/workflows/build_template.yml

@@ -127,6 +127,9 @@ jobs:
           ref: ${{ inputs.pr_branch_ref }}
           fetch-depth: 2 # we may fetch cache from the commit before this one (or earlier)
           path: pr-branch
+          # This is an untrusted (potentially fork) checkout whose code we build.
+          # Don't leave the GITHUB_TOKEN in pr-branch/.git/config, where that code could read it.
+          persist-credentials: false
 
       - name: Prepare DownstreamTest directory
         shell: bash
@@ -689,6 +692,8 @@ jobs:
       - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
           ref: ${{ inputs.pr_branch_ref }}
+          # Untrusted (potentially fork) checkout: don't persist the GITHUB_TOKEN into its .git/config.
+          persist-credentials: false
 
       - name: Configure Lean
         uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0

.github/workflows/decls-diff.yml

@@ -0,0 +1,142 @@
+# 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.
+
+name: Declarations diff (post-build)
+
+on:
+  workflow_run:
+    # Match the build workflows by their `name:` — `build.yml` (non-fork PRs,
+    # push-triggered) and `build_fork.yml` (fork PRs, pull_request_target).
+    workflows: ["continuous integration", "continuous integration (mathlib forks)"]
+    types: [completed]
+
+permissions:
+  contents: read
+  actions: read           # for cross-workflow artifact downloads
+
+jobs:
+  diff:
+    # The build never runs on a `pull_request` event: non-fork PRs build via
+    # `build.yml` on `push` (head_branch = the PR branch), fork PRs via
+    # `build_fork.yml` on `pull_request_target`. Accept both, and for `push`
+    # exclude master and the non-PR maintenance branches.
+    if: >-
+      github.repository == 'leanprover-community/mathlib4'
+      && github.event.workflow_run.conclusion == 'success'
+      && (
+        github.event.workflow_run.event == 'pull_request_target'
+        || (
+          github.event.workflow_run.event == 'push'
+          && github.event.workflow_run.head_branch != 'master'
+          && github.event.workflow_run.head_branch != 'nightly-testing'
+          && !startsWith(github.event.workflow_run.head_branch, 'lean-pr-testing-')
+        )
+      )
+    runs-on: ubuntu-latest
+    steps:
+      - name: Resolve Build run + SHA
+        id: meta
+        run: |
+          set -euo pipefail
+          RUN_ID="${{ github.event.workflow_run.id }}"
+          NEW_SHA="${{ github.event.workflow_run.head_sha }}"
+          {
+            echo "run-id=$RUN_ID"
+            echo "new-sha=$NEW_SHA"
+          } | tee -a "$GITHUB_OUTPUT"
+
+      - name: Checkout new commit
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        with:
+          ref: ${{ steps.meta.outputs.new-sha }}
+          fetch-depth: 0
+
+      - name: Resolve merge-base against master
+        id: resolve
+        env:
+          NEW_SHA: ${{ steps.meta.outputs.new-sha }}
+        run: |
+          set -euo pipefail
+          git fetch --quiet origin master
+          MB="$(git merge-base "$NEW_SHA" origin/master)"
+          echo "merge-base=$MB" | tee -a "$GITHUB_OUTPUT"
+
+      - name: Download new-side artifact
+        uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
+        with:
+          name: import-graph
+          path: ./new-artifact
+          run-id: ${{ steps.meta.outputs.run-id }}
+          github-token: ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Find master Build for the merge-base
+        id: master-run
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          REPO: ${{ github.repository }}
+          MB: ${{ steps.resolve.outputs.merge-base }}
+        run: |
+          set -euo pipefail
+          RUN="$(gh api "repos/$REPO/actions/runs?head_sha=$MB&event=push&status=success&branch=master" \
+                  --jq '[.workflow_runs[] | select(.name=="continuous integration")] | .[0].id // ""')"
+          # A successful run is not enough: it must also carry the `import-graph` artifact.
+          HAS_ARTIFACT=""
+          if [ -n "$RUN" ]; then
+            HAS_ARTIFACT="$(gh api "repos/$REPO/actions/runs/$RUN/artifacts" \
+                    --jq '[.artifacts[] | select(.name=="import-graph")] | length')"
+          fi
+          if [ -n "$RUN" ] && [ "${HAS_ARTIFACT:-0}" -gt 0 ]; then
+            {
+              echo "found=true"
+              echo "run-id=$RUN"
+            } | tee -a "$GITHUB_OUTPUT"
+          else
+            echo "found=false" | tee -a "$GITHUB_OUTPUT"
+            echo "No usable master Build for merge-base $MB (no run, or run lacks the import-graph artifact)."
+          fi
+
+      - name: Download master-side artifact
+        if: steps.master-run.outputs.found == 'true'
+        uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
+        with:
+          name: import-graph
+          path: ./ref-artifact
+          run-id: ${{ steps.master-run.outputs.run-id }}
+          github-token: ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Checkout local actions
+        if: steps.master-run.outputs.found == 'true'
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        with:
+          ref: ${{ github.workflow_sha }}
+          fetch-depth: 1
+          sparse-checkout: .github/actions
+          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'
+        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 }}
+
+      - name: Note cache miss
+        if: steps.master-run.outputs.found != 'true'
+        run: |
+          {
+            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"

.github/workflows/maintainer_bors.yml

@@ -13,6 +13,13 @@ on:
   pull_request_review_comment:
     types: [created]
 
+# This job only parses the triggering comment and emits an artifact for the
+# privileged `maintainer_bors_wf_run` workflow to consume; it never uses the
+# token to mutate the repo. Keep it read-only rather than inheriting the
+# default token permissions.
+permissions:
+  contents: read
+
 jobs:
   add_ready_to_merge_label:
     # we set some variables. The ones of the form `${{ X }}${{ Y }}` are typically not

.github/workflows/olean_report.yaml

@@ -88,6 +88,8 @@ jobs:
           ref: refs/pull/${{ github.event.issue.number }}/head
           fetch-depth: 0
           path: pr-branch
+          # Untrusted (potentially fork) checkout: don't persist the GITHUB_TOKEN into its .git/config.
+          persist-credentials: false
 
       # Check out master into tools-branch.  We build the `cache` binary from
       # here so that a single binary can fetch oleans for both checkouts.

Mathlib.lean

@@ -1318,6 +1318,7 @@ public import Mathlib.Algebra.Star.StarRingHom
 public import Mathlib.Algebra.Star.Subalgebra
 public import Mathlib.Algebra.Star.Subsemiring
 public import Mathlib.Algebra.Star.TensorProduct
+public import Mathlib.Algebra.Star.TransferInstance
 public import Mathlib.Algebra.Star.Unitary
 public import Mathlib.Algebra.Star.UnitaryStarAlgAut
 public import Mathlib.Algebra.Symmetrized
@@ -2661,6 +2662,7 @@ public import Mathlib.CategoryTheory.EpiMono
 public import Mathlib.CategoryTheory.EqToHom
 public import Mathlib.CategoryTheory.Equivalence
 public import Mathlib.CategoryTheory.Equivalence.Symmetry
+public import Mathlib.CategoryTheory.EquivalenceRelation
 public import Mathlib.CategoryTheory.EssentialImage
 public import Mathlib.CategoryTheory.EssentiallySmall
 public import Mathlib.CategoryTheory.Extensive
@@ -4378,6 +4380,7 @@ public import Mathlib.Data.Sum.Lattice
 public import Mathlib.Data.Sum.Order
 public import Mathlib.Data.Sym.Basic
 public import Mathlib.Data.Sym.Card
+public import Mathlib.Data.Sym.NatCard
 public import Mathlib.Data.Sym.Sym2
 public import Mathlib.Data.Sym.Sym2.Finsupp
 public import Mathlib.Data.Sym.Sym2.Init
@@ -4827,6 +4830,7 @@ public import Mathlib.GroupTheory.Submonoid.Centralizer
 public import Mathlib.GroupTheory.Submonoid.Inverses
 public import Mathlib.GroupTheory.Subsemigroup.Center
 public import Mathlib.GroupTheory.Subsemigroup.Centralizer
+public import Mathlib.GroupTheory.Subsemigroup.Lemmas
 public import Mathlib.GroupTheory.Sylow
 public import Mathlib.GroupTheory.Torsion
 public import Mathlib.GroupTheory.Transfer
@@ -5060,6 +5064,7 @@ public import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
 public import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
 public import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
 public import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
+public import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.MvPolynomial
 public import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
 public import Mathlib.LinearAlgebra.Matrix.Gershgorin
 public import Mathlib.LinearAlgebra.Matrix.Hadamard
@@ -6169,6 +6174,7 @@ public import Mathlib.Order.WithBotTop
 public import Mathlib.Order.Zorn
 public import Mathlib.Order.ZornAtoms
 public import Mathlib.Probability.BorelCantelli
+public import Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
 public import Mathlib.Probability.CDF
 public import Mathlib.Probability.CentralLimitTheorem
 public import Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
@@ -6394,6 +6400,8 @@ public import Mathlib.RingTheory.Bialgebra.TensorProduct
 public import Mathlib.RingTheory.Binomial
 public import Mathlib.RingTheory.ChainOfDivisors
 public import Mathlib.RingTheory.ClassGroup
+public import Mathlib.RingTheory.ClassGroup.Basic
+public import Mathlib.RingTheory.ClassGroup.ExtendedHom
 public import Mathlib.RingTheory.Coalgebra.Basic
 public import Mathlib.RingTheory.Coalgebra.CoassocSimps
 public import Mathlib.RingTheory.Coalgebra.Convolution
@@ -6554,6 +6562,7 @@ public import Mathlib.RingTheory.Ideal.Colon
 public import Mathlib.RingTheory.Ideal.Cotangent
 public import Mathlib.RingTheory.Ideal.CotangentBaseChange
 public import Mathlib.RingTheory.Ideal.Defs
+public import Mathlib.RingTheory.Ideal.Finsupp
 public import Mathlib.RingTheory.Ideal.GoingDown
 public import Mathlib.RingTheory.Ideal.GoingUp
 public import Mathlib.RingTheory.Ideal.Height
@@ -6852,6 +6861,7 @@ public import Mathlib.RingTheory.ReesAlgebra
 public import Mathlib.RingTheory.Regular.Category
 public import Mathlib.RingTheory.Regular.Depth
 public import Mathlib.RingTheory.Regular.Flat
+public import Mathlib.RingTheory.Regular.Free
 public import Mathlib.RingTheory.Regular.IsSMulRegular
 public import Mathlib.RingTheory.Regular.LinearMap
 public import Mathlib.RingTheory.Regular.ProjectiveDimension
@@ -7093,6 +7103,7 @@ public import Mathlib.Tactic.ArithMult
 public import Mathlib.Tactic.ArithMult.Init
 public import Mathlib.Tactic.Attr.Core
 public import Mathlib.Tactic.Attr.Register
+public import Mathlib.Tactic.BDSimp
 public import Mathlib.Tactic.Basic
 public import Mathlib.Tactic.Bound
 public import Mathlib.Tactic.Bound.Attribute

Mathlib/Algebra/Algebra/Defs.lean

@@ -380,6 +380,7 @@ theorem linearMap_apply (r : R) : Algebra.linearMap R A r = algebraMap R A r :=
 theorem coe_linearMap : ⇑(Algebra.linearMap R A) = algebraMap R A :=
   rfl
 
+-- see Note [higher instance priority]
 /-- The identity map inducing an `Algebra` structure. -/
 instance (priority := 1100) id : Algebra R R where
   -- We override `toFun` and `toSMul` because `RingHom.id` is not reducible and cannot