Merge remote-tracking branch 'origin/master' into nat-ideal-eq-top

* origin/master: (189 commits)
  chore(Algebra): make more names consistent (#20449)
  feat: Polynomial FLT (#18882)
  feat: A disjoint union is finite iff all sets are finite, and all but finitely many are empty (#20457)
  fix: linkfix in 100.yaml (#20517)
  feat(1000): fill in more entries (#20470)
  feat(Combinatorics/SimpleGraph/Walk): add `penultimate` and `snd` (#16769)
  feat(ContinuousMultilinearMap): add lemmas about `.prod` (#20462)
  feat(RingTheory): classification of etale algebras over fields (#20324)
  fix: Allow multiple builds on staging branch (#20515)
  feat(CategoryTheory/Shift/Adjunction): properties of `Adjunction.CommShift` (#20337)
  chore(Data/Multiset/Basic): move the `sub`, `union`, `inter` sections lower (#19863)
  chore(Topology/UniformSpace/Completion): make coe' argument implicit (#20514)
  refactor(Algebra/Category/Grp/Colimits): change the construction of colimits in `AddCommGrp` (#20474)
  feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems (#16544)
  chore(RingTheory/Finiteness): rename Module.Finite.out (#20506)
  refactor(CategoryTheory/Limits/Preserves/Ulift): simplify the proof that the universe lifting functor for types preserves all colimits (#20508)
  feat(CategoryTheory): products in the category of Ind-objects (#20507)
  chore: remove >9 month old deprecations (#20505)
  chore(FieldTheory/Galois): small cleanup (#20217)
  chore(LinearIndependent): generalize to semirings (#20480)
  chore(NumberTheory/NumberField/AdeleRing): refactor adele rings (#20500)
  chore: replace `aesop` with `simp` where possible (#20483)
  chore(1000): remove nonexistent fields (#20493)
  chore(CategoryTheory/Adjunction.Basic, CategoryTheory/Equivalence): change definition of `Adjunction.comp` and `Equivalence.trans` (#20490)
  feat(Asymptotics): add `Asymptotics.*.*Prod` lemmas (#20458)
  feat: a conditional kernel is almost everywhere a probability measure (#20430)
  feat: if `f` is a measurable group hom, then every point has a neighborhood `s` such that `f '' s` is bounded (#20304)
  feat: `Ico`, `Ioc`, and `Ioo` are not closed or compact (#20479)
  chore: drop redundant hypothesis in `Module.Dual.eq_of_preReflection_mapsTo` (#20492)
  feat(FaaDiBruno): derive `DecidableEq` (#20482)
  chore(SetTheory/Ordinal/Basic): `{x // x < y}` → `Iio y` (#20413)
  chore: generalize `FormalMultilinearSeries.ofScalars_norm` to `Seminormed` (#20351)
  chore(MvPolynomial/Localization): golf using TensorProduct (#20309)
  chore(Combinatorics/Enumerative/Partition): auto-derive DecidableEq (#20277)
  chore(CategoryTheory): make relevant parameters explicit in `Arrow.homMk`. (#20259)
  feat: add `IsStarNormal (↑x⁻¹ : R)` instance for `x : Rˣ` (#20091)
  fix: Stop cancelling builds of master (#20435)
  chore: update Mathlib dependencies 2025-01-05 (#20485)
  feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas (#18933)
  chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464)
  chore: bot validates lean-toolchain on bump/v4.X.0 branches (#20478)
  feat: shorthand lemmas for the L1 norm (#20383)
  chore: remove unnecessary adaptation notes (#20467)
  chore(Algebra/Category/MonCat/Colimits): remove smallness condition (#20473)
  chore(SetTheory/Ordinal/Arithmetic): `IsLeftCancelAdd Ordinal` (#19888)
  feat(Algebra): more on `OrthogonalIdempotents` (#18195)
  feat(Radical): `(radical a).natDegree ≤ a.natDegree` (#20468)
  feat(Polynomial): `(a^n)' = 0` iff `a' = 0` when `n` doesn't divide the characteristic (#20190)
  feat(Algebra/Lie): add Lie's theorem (#13480)
  chore(RingTheory/Generators): make algebra instance a def (#14265)
  ...

.github/build.in.yml

@@ -12,19 +12,15 @@ env:
   # not necessarily satisfy this property.
   LAKE_NO_CACHE: true
 
-jobs:
-  # Cancels previous runs of jobs in this file
-  cancel:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: 'Cancel Previous Runs (CI)'
-    runs-on: ubuntu-latest
-    # timeout-minutes: 3
-    steps:
-      - uses: styfle/[email protected]
-        with:
-          all_but_latest: true
-          access_token: ${{ github.token }}
+concurrency:
+  # label each workflow run; only the latest with each label will run
+  # workflows on master get more expressive labels
+  group: ${{ github.workflow }}-${{ github.ref }}.
+    ${{ ( contains(fromJSON( '["refs/heads/master", "refs/heads/staging"]'), github.ref ) && github.run_id) || ''}}
+  # cancel any running workflow with the same label
+  cancel-in-progress: true
 
+jobs:
   style_lint:
     if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
     name: Lint styleJOB_NAME

.github/workflows/bors.yml

@@ -22,19 +22,15 @@ env:
   # not necessarily satisfy this property.
   LAKE_NO_CACHE: true
 
-jobs:
-  # Cancels previous runs of jobs in this file
-  cancel:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: 'Cancel Previous Runs (CI)'
-    runs-on: ubuntu-latest
-    # timeout-minutes: 3
-    steps:
-      - uses: styfle/[email protected]
-        with:
-          all_but_latest: true
-          access_token: ${{ github.token }}
+concurrency:
+  # label each workflow run; only the latest with each label will run
+  # workflows on master get more expressive labels
+  group: ${{ github.workflow }}-${{ github.ref }}.
+    ${{ ( contains(fromJSON( '["refs/heads/master", "refs/heads/staging"]'), github.ref ) && github.run_id) || ''}}
+  # cancel any running workflow with the same label
+  cancel-in-progress: true
 
+jobs:
   style_lint:
     if: github.repository == 'leanprover-community/mathlib4'
     name: Lint style

.github/workflows/build.yml

@@ -29,19 +29,15 @@ env:
   # not necessarily satisfy this property.
   LAKE_NO_CACHE: true
 
-jobs:
-  # Cancels previous runs of jobs in this file
-  cancel:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: 'Cancel Previous Runs (CI)'
-    runs-on: ubuntu-latest
-    # timeout-minutes: 3
-    steps:
-      - uses: styfle/[email protected]
-        with:
-          all_but_latest: true
-          access_token: ${{ github.token }}
+concurrency:
+  # label each workflow run; only the latest with each label will run
+  # workflows on master get more expressive labels
+  group: ${{ github.workflow }}-${{ github.ref }}.
+    ${{ ( contains(fromJSON( '["refs/heads/master", "refs/heads/staging"]'), github.ref ) && github.run_id) || ''}}
+  # cancel any running workflow with the same label
+  cancel-in-progress: true
 
+jobs:
   style_lint:
     if: github.repository == 'leanprover-community/mathlib4'
     name: Lint style

.github/workflows/build_fork.yml

@@ -26,19 +26,15 @@ env:
   # not necessarily satisfy this property.
   LAKE_NO_CACHE: true
 
-jobs:
-  # Cancels previous runs of jobs in this file
-  cancel:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: 'Cancel Previous Runs (CI)'
-    runs-on: ubuntu-latest
-    # timeout-minutes: 3
-    steps:
-      - uses: styfle/[email protected]
-        with:
-          all_but_latest: true
-          access_token: ${{ github.token }}
+concurrency:
+  # label each workflow run; only the latest with each label will run
+  # workflows on master get more expressive labels
+  group: ${{ github.workflow }}-${{ github.ref }}.
+    ${{ ( contains(fromJSON( '["refs/heads/master", "refs/heads/staging"]'), github.ref ) && github.run_id) || ''}}
+  # cancel any running workflow with the same label
+  cancel-in-progress: true
 
+jobs:
   style_lint:
     if: github.repository != 'leanprover-community/mathlib4'
     name: Lint style (fork)

.github/workflows/nightly_detect_failure.yml

@@ -170,15 +170,40 @@ jobs:
       uses: actions/github-script@v7
       with:
         script: |
-          const response = await github.rest.repos.getContent({
-            owner: context.repo.owner,
-            repo: context.repo.repo,
-            path: 'lean-toolchain',
-            ref: ${{ steps.latest_bump_branch.outputs.result }}
-          });
-          const content = Buffer.from(response.data.content, 'base64').toString();
-          const version = content.match(/leanprover\/lean4:nightly-(\d{4}-\d{2}-\d{2})/)[1];
-          return version;
+          try {
+            const response = await github.rest.repos.getContent({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              path: 'lean-toolchain',
+              ref: ${{ steps.latest_bump_branch.outputs.result }}
+            });
+            const content = Buffer.from(response.data.content, 'base64').toString();
+            const match = content.match(/leanprover\/lean4:nightly-(\d{4}-\d{2}-\d{2})/);
+            if (!match) {
+              core.setFailed('Toolchain pattern did not match');
+              core.setOutput('toolchain_content', content);
+              return null;
+            }
+            return match[1];
+          } catch (error) {
+            core.setFailed(error.message);
+            return null;
+          }
+
+    - name: Send warning message on Zulip if pattern doesn't match
+      if: failure()
+      uses: zulip/github-actions-zulip/send-message@v1
+      with:
+        api-key: ${{ secrets.ZULIP_API_KEY }}
+        email: '[email protected]'
+        organization-url: 'https://leanprover.zulipchat.com'
+        to: 'nightly-testing'
+        type: 'stream'
+        topic: 'Mathlib status updates'
+        content: |
+          ⚠️ Warning: The lean-toolchain file in the latest bump branch does not match the expected pattern 'leanprover/lean4:nightly-YYYY-MM-DD'.
+          Current content: ${{ steps.bump_version.outputs.toolchain_content }}
+          This needs to be fixed for the nightly testing process to work correctly.
 
     - name: Compare versions and post a reminder.
       env:

Archive/Imo/Imo2024Q5.lean

@@ -302,7 +302,7 @@ lemma Path.tail_induction {motive : Path N → Prop} (ind : ∀ p, motive p.tail
   case cons head tail hi =>
     by_cases h : (p'.cells[1]'p'.one_lt_length_cells).1 = 0
     · refine ind p' ?_
-      simp_rw [Path.tail, if_pos h, List.tail_cons]
+      simp_rw [Path.tail, if_pos h, p', List.tail_cons]
       exact hi _ _ _ _
     · exact base p' h
 

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -165,9 +165,9 @@ theorem disjoint_bits (p q : ℕ) :
 
 open MeasureTheory.Measure
 
-private def measureableSpace_list_int : MeasurableSpace (List ℤ) := ⊤
+private def measurableSpace_list_int : MeasurableSpace (List ℤ) := ⊤
 
-attribute [local instance] measureableSpace_list_int
+attribute [local instance] measurableSpace_list_int
 
 private theorem measurableSingletonClass_list_int : MeasurableSingletonClass (List ℤ) :=
   { measurableSet_singleton := fun _ => trivial }

Counterexamples/Cyclotomic105.lean

@@ -94,7 +94,10 @@ theorem cyclotomic_105 :
   repeat' norm_num
 
 theorem coeff_cyclotomic_105 : coeff (cyclotomic 105 ℤ) 7 = -2 := by
-  simp [cyclotomic_105, coeff_one, coeff_X_of_ne_one]
+  rw [cyclotomic_105]
+  -- `Int.reduceNeg` produces an invalid proof that incorrectly transforms this goal into `False`,
+  -- c.f. https://github.com/leanprover/lean4/issues/6467.
+  simp [coeff_X_of_ne_one, coeff_one, -Int.reduceNeg]
 
 theorem not_forall_coeff_cyclotomic_neg_one_zero_one :
     ¬∀ n i, coeff (cyclotomic n ℤ) i ∈ ({-1, 0, 1} : Set ℤ) := by

Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean

@@ -20,7 +20,7 @@ element of the lattice of uniformities on a type (see `bot_uniformity`).
 
 The theorem `discreteTopology_of_discrete_uniformity` shows that the topology induced by the
 discrete uniformity is the discrete one, but it is well-known that the converse might not hold in
-general, along the lines of the above discussion. We explicitely produce a metric and a uniform
+general, along the lines of the above discussion. We explicitly produce a metric and a uniform
 structure on a space (on `ℕ`, actually) that are not discrete, yet induce the discrete topology.
 
 To check that a certain uniformity is not discrete, recall that once a type `α` is endowed with a
@@ -31,7 +31,7 @@ declaration `UniformSpace.DiscreteUnif.eq_const_of_cauchy` in Mathlib.
 
 A special case of this result is the intuitive observation that a sequence `a : ℕ → ℕ` can be a
 Cauchy sequence if and only if it is eventually constant: when claiming this equivalence, one is
-implicitely endowing `ℕ` with the metric inherited from `ℝ`, that induces the discrete uniformity
+implicitly endowing `ℕ` with the metric inherited from `ℝ`, that induces the discrete uniformity
 on `ℕ`. Hence, the intuition suggesting that a Cauchy sequence, whose
 terms are "closer and closer to each other", valued in `ℕ` must be eventually constant for
 *topological* reasons, namely the fact that `ℕ` is a discrete topological space, is *wrong* in the
@@ -41,7 +41,7 @@ the identity `id : ℕ → ℕ` is Cauchy, then the uniformity is certainly *not
 ## The counterexamples
 
 We produce two counterexamples: in the first section `Metric` we construct a metric and in the
-second section `SetPointUniformity` we construct a uniformity, explicitely as a filter on `ℕ × ℕ`.
+second section `SetPointUniformity` we construct a uniformity, explicitly as a filter on `ℕ × ℕ`.
 They basically coincide, and the difference of the examples lies in their flavours.
 
 ### The metric
@@ -232,7 +232,7 @@ lemma mem_counterBasis_iff (S : Set (ℕ × ℕ)) :
 
 /-- The "crude" uniform structure, without topology, simply as a the filter generated by `Basis`
 and satisfying the axioms for being a uniformity. We later extract the topology `counterTopology`
-generated by it and bundle `counterCoreUniformity` and `counterTopology` in a uniform strucutre
+generated by it and bundle `counterCoreUniformity` and `counterTopology` in a uniform structure
 on `ℕ`, proving in passing that `counterTopology = ⊥`-/
 def counterCoreUniformity : UniformSpace.Core ℕ := by
   apply UniformSpace.Core.mkOfBasis counterBasis <;>