Merge remote-tracking branch 'origin/master' into bump/v4.30.0

Author: kim-em

.github/workflows/build_template.yml

@@ -816,17 +816,7 @@ jobs:
     needs: [style_lint, build, post_steps]
     runs-on: ubuntu-latest
     steps:
-      - name: Generate auto merge app token
-        id: auto-merge-app-token
-        uses: leanprover-community/mathlib-ci/.github/actions/azure-create-github-app-token@3bb576208589a435eeaeac9b144a1b7c3e948760
-        with:
-          app-id: ${{ secrets.MATHLIB_AUTO_MERGE_APP_ID }}
-          key-vault-name: ${{ vars.MATHLIB_AZ_KEY_VAULT_NAME }}
-          key-name: mathlib-auto-merge-app-pk
-          azure-client-id: ${{ vars.GH_APP_AZURE_CLIENT_ID_CI_AUTO_MERGE }}
-          azure-tenant-id: ${{ secrets.LPC_AZ_TENANT_ID }}
-
-      - id: PR_from_push
+      - id: PR
         uses: 8BitJonny/gh-get-current-pr@4056877062a1f3b624d5d4c2bedefa9cf51435c9 # 4.0.0
         # TODO: this may not work properly if the same commit is pushed to multiple branches:
         # https://github.com/8BitJonny/gh-get-current-pr/issues/8
@@ -835,16 +825,6 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
-      # TODO: delete this step and rename `PR_from_push` to `PR` if the above step seems to work properly
-      # Combine the output from the previous action with the metadata supplied by GitHub itself.
-      # Note that if we fall back to github.event.pull_request data, the list of labels is generated when this workflow is triggered
-      # and not updated afterwards!
-      - id: PR
-        shell: bash
-        run: |
-          echo "number=${{ steps.PR_from_push.outputs.number || github.event.pull_request.number }}" | tee -a "$GITHUB_OUTPUT"
-          echo "pr_labels=${{ steps.PR_from_push.outputs.pr_labels || join(github.event.pull_request.labels.*.name, ',') }}" | tee -a "$GITHUB_OUTPUT"
-
       - id: remove_labels
         name: Remove "awaiting-CI"
         # we use curl rather than octokit/request-action so that the job won't fail
@@ -854,6 +834,17 @@ jobs:
             --url https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.PR.outputs.number }}/labels/awaiting-CI \
             --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
 
+      - if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
+        name: Generate auto merge app token
+        id: auto-merge-app-token
+        uses: leanprover-community/mathlib-ci/.github/actions/azure-create-github-app-token@3bb576208589a435eeaeac9b144a1b7c3e948760
+        with:
+          app-id: ${{ secrets.MATHLIB_AUTO_MERGE_APP_ID }}
+          key-vault-name: ${{ vars.MATHLIB_AZ_KEY_VAULT_NAME }}
+          key-name: mathlib-auto-merge-app-pk
+          azure-client-id: ${{ vars.GH_APP_AZURE_CLIENT_ID_CI_AUTO_MERGE }}
+          azure-tenant-id: ${{ secrets.LPC_AZ_TENANT_ID }}
+
       - if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
         name: Get PR label timeline data
         # 'auto-merge-after-CI' must be within the last 100 labels added (could be increased to 250 if needed)

.github/workflows/commit_verification.yml

@@ -3,7 +3,7 @@
 #
 # - Transient commits (prefix: "transient: ") must have zero net effect
 # - Automated commits (prefix: "x: <command>") must match command output
-# - Posts a summary comment categorizing commits for reviewers
+# - Uploads a workflow artifact with verification status and a comment to be posted on the PR
 
 name: Commit Verification
 
@@ -18,7 +18,6 @@ concurrency:
 
 permissions:
   contents: read
-  pull-requests: write
 
 env:
   TRANSIENT_PREFIX: "transient: "
@@ -67,6 +66,7 @@ jobs:
           else
             echo "has_special=false" >> "$GITHUB_OUTPUT"
             echo "No transient or automated commits found"
+            echo "No transient or automated commits found; this comment should never be posted" > comment_body.md
           fi
 
       - name: Verify commits
@@ -100,26 +100,22 @@ jobs:
           # Save to file (GitHub Actions has issues with multiline outputs)
           echo "$COMMENT" > comment_body.md
 
-      - name: Find existing comment
-        if: steps.check.outputs.has_special == 'true'
-        uses: peter-evans/find-comment@b30e6a3c0ed37e7c023ccd3f1db5c6c0b0c23aad # v4
-        id: find-comment
-        with:
-          issue-number: ${{ github.event.pull_request.number }}
-          comment-author: 'github-actions[bot]'
-          body-includes: 'Commit Verification Summary'
-
-      - name: Post or update comment
-        if: steps.check.outputs.has_special == 'true'
-        uses: peter-evans/create-or-update-comment@e8674b075228eee787fea43ef493e45ece1004c9 # v4
-        with:
-          comment-id: ${{ steps.find-comment.outputs.comment-id }}
-          issue-number: ${{ github.event.pull_request.number }}
-          body-path: comment_body.md
-          edit-mode: replace
-
-      - name: Set job status
-        if: steps.check.outputs.has_special == 'true' && steps.verify.outputs.success == 'false'
+      - name: Prepare bridge outputs
         run: |
-          echo "::error::Commit verification failed. See PR comment for details."
-          exit 1
+          jq -n \
+            --arg has_special "${{ steps.check.outputs.has_special }}" \
+            --arg success "${{ steps.verify.outputs.success }}" \
+            '{
+              has_special: $has_special,
+              success: $success,
+            }' > bridge-outputs.json
+
+      - name: Emit bridge artifact
+        uses: leanprover-community/privilege-escalation-bridge/emit@d3bd99c50a4cf8c5350a211e8e3ba07ac19067d8 # v1.1.0
+        with:
+          artifact: workflow-data
+          outputs_file: bridge-outputs.json
+          include_event: minimal
+          files: |
+            comment_body.md
+          retention_days: 5

.github/workflows/commit_verification_wf_run.yml

@@ -0,0 +1,62 @@
+# Commit Verification CI (workflow run)
+# Verifies transient and automated commits in PRs
+#
+# - Downloads the workflow artifact uploaded by commit_verification.yml
+# - Posts a summary comment categorizing commits for reviewers
+
+name: Commit Verification (workflow_run)
+
+on:
+  workflow_run:
+    workflows: ["Commit Verification"]
+    types:
+      - completed
+
+permissions:
+  actions: read
+  contents: read
+  pull-requests: write
+
+jobs:
+  verify:
+    name: Verify Transient and Automated Commits
+    runs-on: ubuntu-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' }}
+    steps:
+      - name: Consume bridge artifact
+        id: bridge
+        uses: leanprover-community/privilege-escalation-bridge/consume@d3bd99c50a4cf8c5350a211e8e3ba07ac19067d8 # v1.1.0
+        with:
+          token: ${{ github.token }}
+          artifact: workflow-data
+          source_workflow: Commit Verification
+          require_event: pull_request
+          fail_on_missing: false
+          extract: |
+            pr_number=meta.pr_number
+            has_special=outputs.has_special
+            success=outputs.success
+
+      - name: Find existing comment
+        if: steps.bridge.outputs.has_special == 'true'
+        uses: peter-evans/find-comment@b30e6a3c0ed37e7c023ccd3f1db5c6c0b0c23aad # v4
+        id: find-comment
+        with:
+          issue-number: ${{ steps.bridge.outputs.pr_number }}
+          comment-author: 'github-actions[bot]'
+          body-includes: 'Commit Verification Summary'
+
+      - name: Post or update comment
+        if: steps.bridge.outputs.has_special == 'true'
+        uses: peter-evans/create-or-update-comment@e8674b075228eee787fea43ef493e45ece1004c9 # v4
+        with:
+          comment-id: ${{ steps.find-comment.outputs.comment-id }}
+          issue-number: ${{ steps.bridge.outputs.pr_number }}
+          body-path: .bridge/comment_body.md
+          edit-mode: replace
+
+      - name: Set job status
+        if: steps.bridge.outputs.has_special == 'true' && steps.bridge.outputs.success == 'false'
+        run: |
+          echo "::error::Commit verification failed. See PR comment for details."
+          exit 1

Archive/Hairer.lean

@@ -6,9 +6,8 @@ Junyan Xu
 -/
 import Mathlib.Algebra.MvPolynomial.Funext
 import Mathlib.Analysis.Analytic.Polynomial
-import Mathlib.Analysis.Analytic.Uniqueness
 import Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
-import Mathlib.LinearAlgebra.Dual.Lemmas
+import Mathlib.RingTheory.Algebraic.Integral
 import Mathlib.RingTheory.MvPolynomial.Basic
 import Mathlib.Topology.Algebra.MvPolynomial
 

Archive/Sensitivity.lean

@@ -54,14 +54,9 @@ Notations:
 
 
 /-- The hypercube in dimension `n`. -/
-def Q (n : ℕ) :=
+abbrev Q (n : ℕ) :=
   Fin n → Bool
 
-instance (n) : Inhabited (Q n) := inferInstanceAs (Inhabited (Fin n → Bool))
-
-set_option backward.inferInstanceAs.wrap false in
-instance (n) : Fintype (Q n) := inferInstanceAs (Fintype (Fin n → Bool))
-
 /-- The projection from `Q n.succ` to `Q n` forgetting the first value
 (i.e. the image of zero). -/
 def π {n : ℕ} : Q n.succ → Q n := fun p => p ∘ Fin.succ
@@ -80,7 +75,7 @@ instance : Unique (Q 0) :=
   ⟨⟨fun _ => true⟩, by intro; ext x; fin_cases x⟩
 
 /-- `Q n` has 2^n elements. -/
-theorem card : card (Q n) = 2 ^ n := by simp [Q]
+theorem card : card (Q n) = 2 ^ n := by simp
 
 /-! Until the end of this namespace, `n` will be an implicit argument (still
 a natural number). -/
@@ -210,7 +205,7 @@ theorem duality (p q : Q n) : ε p (e q) = if p = q then 1 else 0 := by
     all_goals
       simp only [Bool.cond_true, Bool.cond_false, LinearMap.fst_apply, LinearMap.snd_apply,
         LinearMap.comp_apply, IH]
-      congr 1; rw [Q.succ_n_eq]; simp [hp, hq]
+      congr 1; simp [Q.succ_n_eq, hp, hq]
 
 /-- Any vector in `V n` annihilated by all `ε p`'s is zero. -/
 theorem epsilon_total {v : V n} (h : ∀ p : Q n, (ε p) v = 0) : v = 0 := by

Mathlib.lean

@@ -1952,6 +1952,7 @@ public import Mathlib.Analysis.InnerProductSpace.Projection.Submodule
 public import Mathlib.Analysis.InnerProductSpace.Rayleigh
 public import Mathlib.Analysis.InnerProductSpace.Reproducing
 public import Mathlib.Analysis.InnerProductSpace.Semisimple
+public import Mathlib.Analysis.InnerProductSpace.SingularValues
 public import Mathlib.Analysis.InnerProductSpace.Spectrum
 public import Mathlib.Analysis.InnerProductSpace.StandardSubspace
 public import Mathlib.Analysis.InnerProductSpace.StarOrder
@@ -2156,40 +2157,22 @@ public import Mathlib.Analysis.Normed.Unbundled.SpectralNorm
 public import Mathlib.Analysis.NormedSpace.Alternating.Basic
 public import Mathlib.Analysis.NormedSpace.Alternating.Curry
 public import Mathlib.Analysis.NormedSpace.Alternating.Uncurry.Fin
-public import Mathlib.Analysis.NormedSpace.BallAction
 public import Mathlib.Analysis.NormedSpace.ConformalLinearMap
 public import Mathlib.Analysis.NormedSpace.Connected
-public import Mathlib.Analysis.NormedSpace.DualNumber
 public import Mathlib.Analysis.NormedSpace.ENormedSpace
 public import Mathlib.Analysis.NormedSpace.Extend
 public import Mathlib.Analysis.NormedSpace.Extr
-public import Mathlib.Analysis.NormedSpace.FunctionSeries
 public import Mathlib.Analysis.NormedSpace.HahnBanach.Extension
 public import Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual
 public import Mathlib.Analysis.NormedSpace.HahnBanach.Separation
-public import Mathlib.Analysis.NormedSpace.HomeomorphBall
-public import Mathlib.Analysis.NormedSpace.IndicatorFunction
-public import Mathlib.Analysis.NormedSpace.Int
 public import Mathlib.Analysis.NormedSpace.MStructure
 public import Mathlib.Analysis.NormedSpace.Multilinear.Basic
 public import Mathlib.Analysis.NormedSpace.Multilinear.Curry
 public import Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn
 public import Mathlib.Analysis.NormedSpace.Normalize
-public import Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics
-public import Mathlib.Analysis.NormedSpace.OperatorNorm.Basic
-public import Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear
-public import Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness
-public import Mathlib.Analysis.NormedSpace.OperatorNorm.Mul
-public import Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm
-public import Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace
-public import Mathlib.Analysis.NormedSpace.OperatorNorm.Prod
 public import Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm
 public import Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm
-public import Mathlib.Analysis.NormedSpace.Pointwise
-public import Mathlib.Analysis.NormedSpace.RCLike
-public import Mathlib.Analysis.NormedSpace.Real
 public import Mathlib.Analysis.NormedSpace.RieszLemma
-public import Mathlib.Analysis.NormedSpace.SphereNormEquiv
 public import Mathlib.Analysis.ODE.Basic
 public import Mathlib.Analysis.ODE.Gronwall
 public import Mathlib.Analysis.ODE.PicardLindelof
@@ -3266,6 +3249,7 @@ public import Mathlib.CategoryTheory.Sites.Point.Skyscraper
 public import Mathlib.CategoryTheory.Sites.Precoverage
 public import Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
 public import Mathlib.CategoryTheory.Sites.Preserves
+public import Mathlib.CategoryTheory.Sites.PreservesLimits
 public import Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
 public import Mathlib.CategoryTheory.Sites.PreservesSheafification
 public import Mathlib.CategoryTheory.Sites.Pretopology
@@ -4054,7 +4038,6 @@ public import Mathlib.Data.Nat.NthRoot.Defs
 public import Mathlib.Data.Nat.Order.Lemmas
 public import Mathlib.Data.Nat.PSub
 public import Mathlib.Data.Nat.Pairing
-public import Mathlib.Data.Nat.PartENat
 public import Mathlib.Data.Nat.Periodic
 public import Mathlib.Data.Nat.PowModTotient
 public import Mathlib.Data.Nat.Prime.Basic
@@ -4275,10 +4258,6 @@ public import Mathlib.Data.ZMod.QuotientRing
 public import Mathlib.Data.ZMod.Units
 public import Mathlib.Data.ZMod.ValMinAbs
 public import Mathlib.Deprecated.Aliases
-public import Mathlib.Deprecated.Estimator
-public import Mathlib.Deprecated.MLList.BestFirst
-public import Mathlib.Deprecated.Order
-public import Mathlib.Deprecated.RingHom
 public import Mathlib.Deprecated.Sort
 public import Mathlib.Dynamics.BirkhoffSum.Average
 public import Mathlib.Dynamics.BirkhoffSum.Basic
@@ -4658,6 +4637,7 @@ public import Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
 public import Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
 public import Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
 public import Mathlib.GroupTheory.SpecificGroups.Cyclic
+public import Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
 public import Mathlib.GroupTheory.SpecificGroups.Dihedral
 public import Mathlib.GroupTheory.SpecificGroups.KleinFour
 public import Mathlib.GroupTheory.SpecificGroups.Quaternion
@@ -6774,7 +6754,6 @@ public import Mathlib.RingTheory.Valuation.Extension
 public import Mathlib.RingTheory.Valuation.FiniteField
 public import Mathlib.RingTheory.Valuation.Integers
 public import Mathlib.RingTheory.Valuation.Integral
-public import Mathlib.RingTheory.Valuation.IntegrallyClosed
 public import Mathlib.RingTheory.Valuation.LocalSubring
 public import Mathlib.RingTheory.Valuation.Minpoly
 public import Mathlib.RingTheory.Valuation.PrimeMultiplicity
@@ -7216,6 +7195,7 @@ public import Mathlib.Topology.Algebra.Group.CompactOpen
 public import Mathlib.Topology.Algebra.Group.Defs
 public import Mathlib.Topology.Algebra.Group.Extension
 public import Mathlib.Topology.Algebra.Group.GroupTopology
+public import Mathlib.Topology.Algebra.Group.Matrix
 public import Mathlib.Topology.Algebra.Group.OpenMapping
 public import Mathlib.Topology.Algebra.Group.Pointwise
 public import Mathlib.Topology.Algebra.Group.Quotient
@@ -7277,7 +7257,6 @@ public import Mathlib.Topology.Algebra.Module.PerfectSpace
 public import Mathlib.Topology.Algebra.Module.PointwiseConvergence
 public import Mathlib.Topology.Algebra.Module.Simple
 public import Mathlib.Topology.Algebra.Module.Star
-public import Mathlib.Topology.Algebra.Module.StrongDual
 public import Mathlib.Topology.Algebra.Module.StrongTopology
 public import Mathlib.Topology.Algebra.Module.TransferInstance
 public import Mathlib.Topology.Algebra.Module.UniformConvergence
@@ -7738,8 +7717,10 @@ public import Mathlib.Topology.Sets.Opens
 public import Mathlib.Topology.Sets.Order
 public import Mathlib.Topology.Sets.VietorisTopology
 public import Mathlib.Topology.Sheaves.Abelian
+public import Mathlib.Topology.Sheaves.AddCommGrpCat
 public import Mathlib.Topology.Sheaves.Alexandrov
 public import Mathlib.Topology.Sheaves.CommRingCat
+public import Mathlib.Topology.Sheaves.Flasque
 public import Mathlib.Topology.Sheaves.Forget
 public import Mathlib.Topology.Sheaves.Functors
 public import Mathlib.Topology.Sheaves.Init

Mathlib/Algebra/DirectSum/Basic.lean

@@ -136,13 +136,15 @@ lemma of_apply {i : ι} (j : ι) (x : β i) : of β i x j = if h : i = j then Eq
 
 theorem mk_apply_of_mem {s : Finset ι} {f : ∀ i : (↑s : Set ι), β i.val} {n : ι} (hn : n ∈ s) :
     mk β s f n = f ⟨n, hn⟩ := by
-  dsimp only [Finset.coe_sort_coe, mk, AddMonoidHom.coe_mk, ZeroHom.coe_mk, DFinsupp.mk_apply]
-  rw [dif_pos hn]
+  dsimp only [Finset.coe_sort_coe, mk, AddMonoidHom.coe_mk, ZeroHom.coe_mk]
+  -- Previously, `DFinsupp.mk_apply` was in the `dsimp only`
+  rw [DFinsupp.mk_apply, dif_pos hn]
 
 theorem mk_apply_of_notMem {s : Finset ι} {f : ∀ i : (↑s : Set ι), β i.val} {n : ι} (hn : n ∉ s) :
     mk β s f n = 0 := by
-  dsimp only [Finset.coe_sort_coe, mk, AddMonoidHom.coe_mk, ZeroHom.coe_mk, DFinsupp.mk_apply]
-  rw [dif_neg hn]
+  dsimp only [Finset.coe_sort_coe, mk, AddMonoidHom.coe_mk, ZeroHom.coe_mk]
+  -- Previously, `DFinsupp.mk_apply` was in the `dsimp only`
+  rw [DFinsupp.mk_apply, dif_neg hn]
 
 @[simp]
 theorem support_zero [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] : (0 : ⨁ i, β i).support = ∅ :=

Mathlib/Algebra/Field/Basic.lean

@@ -178,7 +178,7 @@ instance (priority := 100) Field.toGrindField : Lean.Grind.Field K :=
       · rw [← Int.natCast_add_one, zpow_natCast, zpow_natCast, pow_succ]
       · rw [zpow_add_one₀ h]
     zpow_neg a n := by simp
-    zero_ne_one := zero_ne_one' K }
+    zero_ne_one := zero_ne_one }
 
 attribute [local simp] mul_assoc mul_comm mul_left_comm