Merge remote-tracking branch 'upstream/master' into kim/move-OrderDual

# Conflicts:
#	Mathlib/Order/Filter/AtTopBot/Defs.lean

Author: kim-em

.github/workflows/add_label_from_diff.yaml

@@ -21,33 +21,42 @@ jobs:
     # Don't run on forks, where we wouldn't have permissions to add the label anyway.
     if: github.repository == 'leanprover-community/mathlib4'
     steps:
-    - name: Checkout code
+    - name: Checkout master branch to build autolabel from
       uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
       with:
-        ref: ${{ github.event.pull_request.head.sha }}
-        fetch-depth: 0
+        ref: master
+        path: tools
     - name: Configure Lean
       uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0
       with:
         auto-config: false
         use-github-cache: false
         use-mathlib-cache: false
-    - name: lake exe autolabel
+        lake-package-directory: tools # Building here
+    - name: Build autolabel from master
+      working-directory: tools
+      run: |
+        lake build autolabel
+    - name: Checkout branch to label
+      uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      with:
+        ref: ${{ github.event.pull_request.head.sha || github.sha }}
+        fetch-depth: 0
+        path: pr-branch
+    - name: Run autolabel
+      working-directory: pr-branch
       run: |
-        # the checkout dance, to avoid a detached head
-        git checkout master
-        git checkout -
-        labels="$(lake exe autolabel)"
+        labels="$("${GITHUB_WORKSPACE}/tools/.lake/build/bin/autolabel")"
         printf '%s\n' "${labels}"
         # extract
         label="$(printf '%s' "${labels}" | sed -n 's=^::notice::.*#\[\([^,]*\)\].*=\1=p')"
         printf 'label: "%s"\n' "${label}"
-        if [ -n "${label}" ]
+        if [ -n "${label}" ] && [ -n "${PR_NUMBER}" ]
         then
           printf 'Applying label %s\n' "${label}"
           # we use curl rather than octokit/request-action so that the job won't fail
           # (and send an annoying email) if the labels don't exist
-          url="https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels"
+          url="https://api.github.com/repos/${{ github.repository }}/issues/${PR_NUMBER}/labels"
           printf 'url: %s\n' "${url}"
           jsonLabel="$(printf '{"labels":["%s"]}' "${label}")"
           printf 'jsonLabel: %s\n' "${jsonLabel}"
@@ -62,3 +71,6 @@ jobs:
         fi
       env:
         GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        # the PR number could be undefined in workflows triggered by 'push',
+        # in which case we only log the applicable label and exit
+        PR_NUMBER: ${{ github.event.pull_request.number }}

.github/workflows/build.yml

@@ -10,6 +10,8 @@ on:
       # ignore staging and trying branches used by bors, these are handled by bors.yml
       - 'staging'
       - 'trying'
+      # ignore branches meant for experiments
+      - 'ci-dev/**'
   merge_group:
 
 concurrency:

.github/workflows/build_template.yml

@@ -1,14 +1,22 @@
-# Reusable workflow invoked by build.yml, bors.yml, and build_fork.yml.
+# Reusable workflow invoked by build.yml, bors.yml, build_fork.yml, and ci_dev.yml.
 
 on:
   workflow_call:
     inputs:
       concurrency_group:
         type: string
         required: true
+      tools_branch_ref:
+        type: string
+        required: false
+        default: ''
       pr_branch_ref:
         type: string
         required: true
+      run_post_ci:
+        type: boolean
+        required: false
+        default: true
       runs_on:
         type: string
         required: true
@@ -71,16 +79,16 @@ jobs:
       - name: 'Setup jq'
         uses: dcarbone/install-jq-action@b7ef57d46ece78760b4019dbc4080a1ba2a40b45 # v3.2.0
 
-      # Checkout the master branch into a subdirectory
-      - name: Checkout master branch
+      # Checkout a trusted branch to build the tooling from
+      - name: Checkout tools branch
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         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: ${{ github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing-green' || 'master' }}
-          path: master-branch
+          ref: ${{ inputs.tools_branch_ref != '' && inputs.tools_branch_ref || (github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing-green' || 'master') }}
+          path: tools-branch
 
       # Checkout the PR branch into a subdirectory
       - name: Checkout PR branch
@@ -160,18 +168,18 @@ jobs:
           # Set it as an environment variable for subsequent steps
           echo "LEAN_SRC_PATH=$LEAN_SRC_PATH" >> "$GITHUB_ENV"
 
-      - name: build master-branch tools
-        shell: bash # We're only building the `master` branch version of the tools, so don't need to run inside landrun.
+      - 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 master-branch
+          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
 
       - name: cleanup .cache/mathlib
         # This needs write access to .cache/mathlib, so can't be run inside landrun.
-        # However it is only using the `master` version of `cache`, so is safe to run outside landrun.
+        # However it is only using the `tools` version of `cache`, so is safe to run outside landrun.
         shell: bash
         run: |
           # Define the cache directory path
@@ -190,8 +198,8 @@ jobs:
           # Check if size exceeds 10GB
           if [ "$DIR_SIZE" -gt "10737418240" ]; then
             echo "Cache size exceeds threshold, running lake exe cache clean"
-            # We use the master-branch version of `cache`.
-            cd master-branch
+            # We use the tools-branch version of `cache`.
+            cd tools-branch
             lake exe cache clean
           fi
 
@@ -281,15 +289,15 @@ jobs:
 
       - name: get cache (1/3 - setup and initial fetch)
         id: get_cache_part1_setup
-        shell: bash # only runs `cache get` from `master-branch`, so doesn't need to be inside landrun
+        shell: bash # only runs `cache get` from `tools-branch`, so doesn't need to be inside landrun
         run: |
           cd pr-branch
           echo "Removing old Mathlib build directories prior to cache fetch..."
           rm -rf .lake/build/lib/lean/Mathlib
 
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
           echo "Attempting to fetch olean for Mathlib/Init.lean from cache..."
-          ../master-branch/.lake/build/bin/cache 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
@@ -303,16 +311,16 @@ jobs:
 
       - name: get cache (3/3 - finalize cache operation)
         id: get
-        shell: bash # only runs `cache get` from `master-branch`, so doesn't need to be inside landrun
+        shell: bash # only runs `cache get` from `tools-branch`, so doesn't need to be inside landrun
         run: |
           cd pr-branch
           if [[ "${{ steps.get_cache_part2_test.outcome }}" == "success" ]]; then
             echo "Fetching all remaining cache..."
 
-            ../master-branch/.lake/build/bin/cache get
+            ../tools-branch/.lake/build/bin/cache get
 
             # Run again with --repo, to ensure we actually get the oleans.
-            ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get
+            ../tools-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get
           else
             echo "WARNING: 'lake build --no-build -v Mathlib.Init' failed."
             echo "No cache for 'Mathlib.Init' available or it could not be prepared."
@@ -346,7 +354,7 @@ jobs:
           fi
           echo "::endgroup::"
 
-          ../master-branch/scripts/lake-build-with-retry.sh Mathlib
+          ../tools-branch/scripts/lake-build-with-retry.sh Mathlib
           # results of build at pr-branch/.lake/build_summary_Mathlib.json
       - name: end gh-problem-match-wrap for build step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
@@ -372,15 +380,15 @@ jobs:
           # Trim trailing whitespace from secrets to prevent issues with accidentally added spaces
           export MATHLIB_CACHE_SAS="${MATHLIB_CACHE_SAS_RAW%"${MATHLIB_CACHE_SAS_RAW##*[![:space:]]}"}"
 
-          # Use the trusted cache tool from master-branch
+          # Use the trusted cache tool from tools-branch
           # TODO: this is not doing anything currently, and needs to be integrated with put-unpacked
-          # ../master-branch/.lake/build/bin/cache commit || true
+          # ../tools-branch/.lake/build/bin/cache commit || true
           # run this in CI if it gets an incorrect lake hash for existing cache files somehow
-          # ../master-branch/.lake/build/bin/cache put!
+          # ../tools-branch/.lake/build/bin/cache put!
           # do not try to upload files just downloaded
 
           echo "Uploading cache to Azure..."
-          MATHLIB_CACHE_USE_CLOUDFLARE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
+          MATHLIB_CACHE_USE_CLOUDFLARE=0 ../tools-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
         env:
           MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
 
@@ -396,23 +404,23 @@ jobs:
         shell: bash
         run: |
           cd pr-branch
-          ../master-branch/.lake/build/bin/cache get Archive.lean
-          ../master-branch/.lake/build/bin/cache 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
         continue-on-error: true
         run: |
           cd pr-branch
-          ../master-branch/scripts/lake-build-with-retry.sh Archive
+          ../tools-branch/scripts/lake-build-with-retry.sh Archive
           # results of build at pr-branch/.lake/build_summary_Archive.json
 
       - name: build counterexamples
         id: counterexamples
         continue-on-error: true
         run: |
           cd pr-branch
-          ../master-branch/scripts/lake-build-with-retry.sh Counterexamples
+          ../tools-branch/scripts/lake-build-with-retry.sh Counterexamples
           # results of build at pr-branch/.lake/build_summary_Counterexamples.json
 
       - name: Check if building Archive or Counterexamples failed
@@ -436,8 +444,8 @@ jobs:
           export MATHLIB_CACHE_SAS="${MATHLIB_CACHE_SAS_RAW%"${MATHLIB_CACHE_SAS_RAW##*[![:space:]]}"}"
 
           echo "Uploading Archive and Counterexamples cache to Azure..."
-          MATHLIB_CACHE_USE_CLOUDFLARE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Archive.lean
-          MATHLIB_CACHE_USE_CLOUDFLARE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Counterexamples.lean
+          MATHLIB_CACHE_USE_CLOUDFLARE=0 ../tools-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Archive.lean
+          MATHLIB_CACHE_USE_CLOUDFLARE=0 ../tools-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Counterexamples.lean
         env:
           MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
 
@@ -460,7 +468,7 @@ jobs:
         id: test
         run: |
           cd pr-branch
-          ../master-branch/scripts/lake-build-wrapper.py .lake/build_summary_MathlibTest.json lake --iofail test
+          ../tools-branch/scripts/lake-build-wrapper.py .lake/build_summary_MathlibTest.json lake --iofail test
       - name: end gh-problem-match-wrap for test step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
         with:
@@ -584,8 +592,8 @@ jobs:
           TEST_OUTCOME: ${{ steps.test.outcome }}
           NIGHTLY_TESTING_REPO: leanprover-community/mathlib4-nightly-testing
         run: |
-          master-branch/scripts/lean-pr-testing-comments.sh lean
-          master-branch/scripts/lean-pr-testing-comments.sh batteries
+          tools-branch/scripts/lean-pr-testing-comments.sh lean
+          tools-branch/scripts/lean-pr-testing-comments.sh batteries
 
   post_steps:
     name: Post-Build Step
@@ -678,6 +686,7 @@ jobs:
 
   final:
     name: Post-CI job
+    if: ${{ inputs.run_post_ci }}
     needs: [style_lint, build, post_steps]
     runs-on: ubuntu-latest
     steps:

.github/workflows/ci_dev.yml

@@ -0,0 +1,42 @@
+name: ci dev
+
+on:
+  workflow_dispatch:
+    inputs:
+      tools_branch_ref:
+        description: ref for tools checkout (defaults to 'this commit')
+        required: false
+        type: string
+        default: ''
+      pr_branch_ref:
+        description: ref for building-branch checkout (defaults to 'this commit')
+        required: false
+        type: string
+        default: ''
+      run_post_ci:
+        description: Run the post-CI job?
+        required: false
+        type: boolean
+        default: false # We shouldn't need this job in typical experiments
+
+# Limit permissions for GITHUB_TOKEN for the entire workflow
+permissions:
+  contents: read
+  # By default let's remove this permission (which is present in the other build pipelines)
+  # from the CI experimentation runs to avoid unwitting side effects
+  # pull-requests: write
+
+jobs:
+  build:
+    name: ci (dev branch)
+    # For sanity and intentionality, let's only trigger this from branches ci-dev/*
+    if: ${{ github.repository == 'leanprover-community/mathlib4' && github.ref_type == 'branch' && startsWith(github.ref_name, 'ci-dev/') }}
+    uses: ./.github/workflows/build_template.yml
+    with:
+      concurrency_group: ${{ github.workflow }}-${{ github.ref }}
+      # Use the tools from 'this branch', as our changes in the tools might be relevant for experiments
+      tools_branch_ref: ${{ inputs.tools_branch_ref != '' && inputs.tools_branch_ref || github.sha }}
+      pr_branch_ref: ${{ inputs.pr_branch_ref != '' && inputs.pr_branch_ref || github.sha }}
+      run_post_ci: ${{ inputs.run_post_ci }}
+      runs_on: pr
+    secrets: inherit

.github/workflows/pre-commit.yml

@@ -11,6 +11,7 @@ on:
       # ignore staging and trying branches used by bors, these are handled by bors.yml
       - 'staging'
       - 'trying'
+      - 'ci-dev/**' # ignore branches meant for experiments
       - 'master'
   pull_request:
 

Mathlib.lean

@@ -2012,6 +2012,7 @@ public import Mathlib.Analysis.Normed.Module.Basic
 public import Mathlib.Analysis.Normed.Module.Complemented
 public import Mathlib.Analysis.Normed.Module.Completion
 public import Mathlib.Analysis.Normed.Module.Connected
+public import Mathlib.Analysis.Normed.Module.ContinuousInverse
 public import Mathlib.Analysis.Normed.Module.Convex
 public import Mathlib.Analysis.Normed.Module.Dual
 public import Mathlib.Analysis.Normed.Module.ENormedSpace

Mathlib/Algebra/Group/Finsupp.lean

@@ -153,7 +153,7 @@ lemma support_single_add_single [DecidableEq ι] {f₁ f₂ : ι} {g₁ g₂ : M
     (H : f₁ ≠ f₂) (hg₁ : g₁ ≠ 0) (hg₂ : g₂ ≠ 0) :
     (single f₁ g₁ + single f₂ g₂).support = {f₁, f₂} := by
   rw [support_add_eq, support_single_ne_zero _ hg₁, support_single_ne_zero _ hg₂]
-  · simp [pair_comm f₂ f₁]
+  · simp
   · simp [support_single_ne_zero, *]
 
 lemma support_single_add_single_subset [DecidableEq ι] {f₁ f₂ : ι} {g₁ g₂ : M} :

Mathlib/Algebra/Polynomial/Lifts.lean

@@ -34,7 +34,7 @@ and that a monic polynomial that lifts can be lifted to a monic polynomial (of t
 ## Implementation details
 
 In general `R` and `S` are semirings, so `lifts` is a semiring. In the case of rings, see
-`lifts_iff_lifts_ring`.
+`lifts_iff_liftsRing`.
 
 Since we do not assume `R` to be commutative, we cannot say in general that the set of polynomials
 that lift is a subalgebra. (By `lift_iff` this is true if `R` is commutative.)

Mathlib/Analysis/Analytic/CPolynomialDef.lean

@@ -246,7 +246,7 @@ theorem HasFiniteFPowerSeriesOnBall.bound_zero_of_eq_zero (hf : ∀ y ∈ Metric
     · convert hasSum_zero
       rw [hp, ContinuousMultilinearMap.zero_apply]
     · rwa [Metric.mem_eball, edist_eq_enorm_sub, add_comm, add_sub_cancel_right,
-        ← edist_zero_eq_enorm, ← Metric.mem_eball]
+        ← edist_zero_right, ← Metric.mem_eball]
 
 /-- If `f` has a formal power series at `x` bounded by `0`, then `f` is equal to `0` in a
 neighborhood of `x`. -/

Mathlib/Analysis/Analytic/Composition.lean

@@ -795,7 +795,7 @@ theorem HasFPowerSeriesWithinAt.comp {g : F → G} {f : E → F} {q : FormalMult
         _ ≤ ‖compAlongComposition q p c‖ * (r : ℝ) ^ n := by
           rw [Finset.prod_const, Finset.card_fin]
           gcongr
-          rw [Metric.mem_eball, edist_zero_eq_enorm] at hy
+          rw [Metric.mem_eball, edist_zero_right] at hy
           have := le_trans (le_of_lt hy) (min_le_right _ _)
           rwa [enorm_le_coe, ← NNReal.coe_le_coe, coe_nnnorm] at this
     tendsto_nhds_of_cauchySeq_of_subseq cau compPartialSumTarget_tendsto_atTop C