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: 4db29a340d585b5ca9cc45ba5b951a3939753d53
+    default: a498f841ad55c852a9203fba855432b922a1b653
   path:
     description: Checkout destination path.
     required: false

.github/actions/get-tools/action.yml

@@ -0,0 +1,129 @@
+# Populates `tools-branch/` with the trusted CI tooling (`cache` binary + the
+# `lake-build-*` helper scripts) that `build_template.yml` invokes by path.
+#
+# Fast path: download the `tools-bin` artifact published by `publish_tools.yml`
+# from its latest successful `master` `push` run, unpack it, and install the
+# matching toolchain. Fallback: check out `tools_source_ref` and build from source
+# (the original behaviour). The fallback also triggers automatically if anything
+# about the download/verification fails, so this action can never make CI worse
+# than building from source.
+#
+# Requires (fast path only): `actions: read` permission. The `gh` CLI is provided
+# by the Hoskinson runner image. Any lookup/download failure falls through to the
+# source build, so the fast path can never make CI worse.
+name: Get CI tools
+description: Download prebuilt CI tools from master, or build them from source.
+inputs:
+  use_artifact:
+    description: Whether to attempt the prebuilt-artifact fast path ('true'/'false').
+    required: true
+  tools_source_ref:
+    description: Git ref to check out and build from when not using the artifact.
+    required: true
+  github_token:
+    description: "Token with `actions: read` on artifact_repo (fast path only)."
+    required: false
+    default: ''
+  artifact_repo:
+    description: Repository that publishes the tools artifact.
+    required: false
+    default: leanprover-community/mathlib4
+  artifact_workflow:
+    description: Workflow file that publishes the tools artifact.
+    required: false
+    default: publish_tools.yml
+  path:
+    description: Destination directory for the tools.
+    required: false
+    default: tools-branch
+runs:
+  using: composite
+  steps:
+    # Resolve the run-id of the latest successful master push of the publisher.
+    # Pure lookup: on any failure (or when the fast path is disabled) we emit an
+    # empty run_id, which skips the download and lands us on the source-build path.
+    - name: Resolve tools artifact run
+      id: resolve
+      shell: bash
+      env:
+        GH_TOKEN: ${{ inputs.github_token }}
+      run: |
+        set -uo pipefail
+        run_id=""
+        if [[ "${{ inputs.use_artifact }}" == "true" && -n "${{ inputs.github_token }}" ]]; then
+          run_id=$(gh run list \
+            --repo "${{ inputs.artifact_repo }}" \
+            --workflow "${{ inputs.artifact_workflow }}" \
+            --branch master --status success --event push \
+            --limit 1 --json databaseId --jq '.[0].databaseId // empty' 2>/dev/null || true)
+        fi
+        echo "Resolved publisher run_id: '${run_id}'"
+        echo "run_id=${run_id}" >> "$GITHUB_OUTPUT"
+
+    - name: Download tools artifact
+      if: ${{ steps.resolve.outputs.run_id != '' }}
+      continue-on-error: true
+      uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
+      with:
+        name: tools-bin
+        path: tools-artifact
+        repository: ${{ inputs.artifact_repo }}
+        run-id: ${{ steps.resolve.outputs.run_id }}
+        github-token: ${{ inputs.github_token }}
+
+    # Unpack the tools and install the toolchain the `cache` binary was linked
+    # against (the one guarantee the old `lake build` of the tools gave us for
+    # free). If the tarball is missing, the unpack fails, or the toolchain won't
+    # install, wipe any partial state and signal a source build.
+    - name: Unpack tools
+      id: finalize
+      shell: bash
+      run: |
+        set -uo pipefail
+        result=build
+        tarball="tools-artifact/tools-bin.tar.gz"
+        if [[ -f "$tarball" ]]; then
+          echo "Found downloaded tools artifact; unpacking..."
+          rm -rf "${{ inputs.path }}"
+          mkdir -p "${{ inputs.path }}"
+          if tar -xzf "$tarball" -C "${{ inputs.path }}" \
+            && [[ -x "${{ inputs.path }}/.lake/build/bin/cache" ]]; then
+            toolchain="$(cat "${{ inputs.path }}/lean-toolchain")"
+            echo "Ensuring tools toolchain is installed: ${toolchain}"
+            # `elan toolchain install` exits non-zero when the toolchain is already
+            # present (the common case), so install best-effort and then confirm the
+            # toolchain is available rather than trusting the install exit code.
+            elan toolchain install "$toolchain" || true
+            if elan toolchain list | awk '{print $1}' | grep -qxF "$toolchain"; then
+              result=artifact
+            else
+              echo "WARNING: tools toolchain '${toolchain}' is not available; falling back to source build."
+            fi
+          else
+            echo "WARNING: tools artifact unpack/validation failed; falling back to source build."
+          fi
+        else
+          echo "No tools artifact available; will build from source."
+        fi
+        if [[ "$result" != "artifact" ]]; then
+          rm -rf "${{ inputs.path }}"
+        fi
+        echo "Tools source: ${result}"
+        echo "result=${result}" >> "$GITHUB_OUTPUT"
+
+    - name: Checkout tools branch (source build)
+      if: ${{ steps.finalize.outputs.result == 'build' }}
+      uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+      with:
+        ref: ${{ inputs.tools_source_ref }}
+        path: ${{ inputs.path }}
+
+    - name: Build tools from source
+      if: ${{ steps.finalize.outputs.result == 'build' }}
+      shell: bash # We're only building a trusted branch with the tools, so no need to run inside landrun.
+      run: |
+        cd "${{ inputs.path }}"
+        lake build cache check-yaml graph
+        ls .lake/build/bin/cache
+        ls .lake/build/bin/check-yaml
+        ls .lake/packages/importGraph/.lake/build/bin/graph

.github/workflows/build.yml

@@ -24,6 +24,7 @@ concurrency:
 permissions:
   contents: read
   id-token: write
+  actions: read  # Allow get-tools to download the prebuilt tools artifact from master's publish_tools runs
   pull-requests: write  # Only allow PR comments/labels
   # All other permissions are implicitly 'none'
 

.github/workflows/build_fork.yml

@@ -25,6 +25,7 @@ concurrency:
 permissions:
   contents: read
   id-token: write
+  actions: read  # Allow get-tools to download the prebuilt tools artifact from master's publish_tools runs
   pull-requests: write  # Only allow PR comments/labels
   # All other permissions are implicitly 'none'
 

.github/workflows/build_template.yml

@@ -93,17 +93,6 @@ jobs:
       - name: 'Setup jq'
         uses: dcarbone/install-jq-action@b7ef57d46ece78760b4019dbc4080a1ba2a40b45 # v3.2.0
 
-      # Checkout a trusted branch to build the tooling from
-      - name: Checkout tools branch
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
-        with:
-          # Recall that on the `leanprover-community/mathlib4-nightly-testing` repository,
-          # we don't maintain a `master` branch at all.
-          # For PRs and pushes to this repository, we will use `nightly-testing-green` instead,
-          # so that even when `nightly-testing` is broken, we can still build tools from a known good state.
-          ref: ${{ inputs.tools_branch_ref != '' && inputs.tools_branch_ref || (github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing-green' || 'master') }}
-          path: tools-branch
-
       - name: Checkout local actions
         uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
         with:
@@ -208,14 +197,22 @@ jobs:
           # Set it as an environment variable for subsequent steps
           echo "LEAN_SRC_PATH=$LEAN_SRC_PATH" >> "$GITHUB_ENV"
 
-      - name: build tools-branch tools
-        shell: bash # We're only building a trusted branch with the tools, so no need to run inside landrun.
-        run: |
-          cd tools-branch
-          lake build cache check-yaml graph
-          ls .lake/build/bin/cache
-          ls .lake/build/bin/check-yaml
-          ls .lake/packages/importGraph/.lake/build/bin/graph
+      # Populate `tools-branch/` with the trusted CI tooling (the `cache` binary and
+      # the `lake-build-*` helper scripts invoked by path below). On the common path
+      # this downloads the prebuilt `tools-bin` artifact published from `master` by
+      # `publish_tools.yml`; otherwise (bors/ci_dev overrides, nightly-testing, or any
+      # download failure) it falls back to checking out and building from source.
+      #
+      # Recall that on the `leanprover-community/mathlib4-nightly-testing` repository,
+      # we don't maintain a `master` branch at all. For PRs and pushes to this
+      # repository, we build tools from `nightly-testing-green` instead, so that even
+      # when `nightly-testing` is broken, we can still build tools from a known good state.
+      - name: Get CI tools
+        uses: ./workflow-actions/.github/actions/get-tools
+        with:
+          use_artifact: ${{ inputs.tools_branch_ref == '' && github.repository == 'leanprover-community/mathlib4' }}
+          tools_source_ref: ${{ inputs.tools_branch_ref != '' && inputs.tools_branch_ref || (github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing-green' || 'master') }}
+          github_token: ${{ github.token }}
 
       - name: download dependencies
         # We need network access to download dependencies

.github/workflows/labels_from_comment.yml

@@ -45,8 +45,13 @@ jobs:
           inComment=""
           label="${labelArray[$i]}"
           printf $'\nProcessing label \'%s\'\n' "${label}"
-          # extract the last line that, up to leading/trailing whitespace, matches the current label
-          inComment="$(printf '%s' "${COMMENT}" | grep "[-]\?${label}$" | tail -1)"
+          # extract the last line whose *entire* content (up to leading/trailing
+          # whitespace, already stripped above) is the label, optionally preceded
+          # by `-`. Anchoring both ends (not just `$`) is what stops bot directives
+          # such as `!downstream-check FLT` — and the downstream-reports automation
+          # comments — from being mistaken for a label request just because the line
+          # happens to end in a label name.
+          inComment="$(printf '%s' "${COMMENT}" | grep "^[-]\?${label}$" | tail -1)"
           if [ -n "${inComment}" ]
           then
             printf $'Found \'%s\'\n' "${inComment}"

Counterexamples/Phillips.lean

@@ -283,7 +283,7 @@ theorem exists_discrete_support_nonpos (f : BoundedAdditiveMeasure α) :
   have I1 : ∀ n, ε / 2 ≤ f (↑(s (n + 1)) \ ↑(s n)) := by
     intro n
     rw [div_le_iff₀' (show (0 : ℝ) < 2 by simp), hε]
-    convert hF (s n) u using 2
+    convert! hF (s n) u using 2
     · ext x
       simp only [u, not_exists, mem_iUnion, mem_diff]
       tauto

Mathlib.lean

@@ -3370,6 +3370,7 @@ public import Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
 public import Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
 public import Mathlib.CategoryTheory.Sites.Hypercover.Zero
 public import Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
+public import Mathlib.CategoryTheory.Sites.InducedTopology
 public import Mathlib.CategoryTheory.Sites.IsSheafFor
 public import Mathlib.CategoryTheory.Sites.JointlySurjective
 public import Mathlib.CategoryTheory.Sites.LeftExact
@@ -3860,6 +3861,7 @@ 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
@@ -3978,6 +3980,7 @@ 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
@@ -4090,14 +4093,19 @@ 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,6 +4281,7 @@ 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
@@ -4285,16 +4294,21 @@ public import Mathlib.Data.Rat.Floor
 public import Mathlib.Data.Rat.Init
 public import Mathlib.Data.Rat.Lemmas
 public import Mathlib.Data.Rat.NatSqrt.Defs
+public import Mathlib.Data.Rat.NatSqrt.Real
 public import Mathlib.Data.Rat.Sqrt
 public import Mathlib.Data.Rat.Star
+public import Mathlib.Data.Real.Archimedean
 public import Mathlib.Data.Real.Basic
 public import Mathlib.Data.Real.CompleteField
 public import Mathlib.Data.Real.ConjExponents
 public import Mathlib.Data.Real.ENatENNReal
 public import Mathlib.Data.Real.Embedding
+public import Mathlib.Data.Real.Hom
 public import Mathlib.Data.Real.Pointwise
 public import Mathlib.Data.Real.Sign
+public import Mathlib.Data.Real.Sqrt
 public import Mathlib.Data.Real.Star
+public import Mathlib.Data.Real.StarOrdered
 public import Mathlib.Data.Rel
 public import Mathlib.Data.Rel.Cover
 public import Mathlib.Data.Rel.Separated
@@ -4517,6 +4531,7 @@ public import Mathlib.FieldTheory.PerfectClosure
 public import Mathlib.FieldTheory.PolynomialGaloisGroup
 public import Mathlib.FieldTheory.PrimeField
 public import Mathlib.FieldTheory.PrimitiveElement
+public import Mathlib.FieldTheory.PurelyInseparable.AdjoinPthRoots
 public import Mathlib.FieldTheory.PurelyInseparable.Basic
 public import Mathlib.FieldTheory.PurelyInseparable.Exponent
 public import Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Mathlib/Algebra/BigOperators/Pi.lean

@@ -12,6 +12,7 @@ public import Mathlib.Algebra.Group.Action.Pi
 public import Mathlib.Algebra.Notation.Indicator
 public import Mathlib.Algebra.Ring.Pi
 public import Mathlib.Data.Fintype.Basic
+public import Mathlib.Data.FunLike.IsApply
 
 /-!
 # Big operators for Pi Types
@@ -230,3 +231,21 @@ theorem eqOn_fun_finsetProd {ι α β : Type*} [CommMonoid α]
   convert! eqOn_finsetProd h v <;> simp
 
 end EqOn
+
+section FunLike
+
+variable {F α β ι : Type*} [FunLike F α β] [CommMonoid β] [CommMonoid F]
+  [IsOneApply F α β] [IsMulApply F α β]
+
+open Classical in
+@[to_additive (attr := simp, grind =)]
+theorem prod_apply (s : Finset ι) (f : ι → F) (x : α) : (∏ i ∈ s, f i) x = ∏ i ∈ s, f i x := by
+  induction s using Finset.induction_on with
+  | empty => simp
+  | insert i s his h => simp [his, h]
+
+@[to_additive (attr := norm_cast)]
+theorem FunLike.coe_prod (s : Finset ι) (f : ι → F) : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, (f i : α → β) := by
+  ext; simp
+
+end FunLike

Mathlib/Algebra/Group/End.lean

@@ -63,7 +63,7 @@ instance : Inhabited (Function.End α) := ⟨1⟩
 
 namespace Equiv.Perm
 
-attribute [to_additive_dont_translate] Perm
+attribute [to_additive_dont_translate] Perm Equiv
 
 instance instOne : One (Perm α) where one := Equiv.refl _
 instance instMul : Mul (Perm α) where mul f g := Equiv.trans g f