Merge branch 'leanprover-community:master' into uniqueness-riesz

Author: CoolRmal

.github/workflows/nolints.yml

@@ -11,27 +11,7 @@ jobs:
     runs-on: ubuntu-latest
     if: github.repository == 'leanprover-community/mathlib4'
     steps:
-      - name: cleanup
-        run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
-
-      # The Hoskinson runners may not have jq installed, so do that now.
-      - name: 'Setup jq'
-        uses: dcarbone/install-jq-action@f0e10f46ff84f4d32178b4b76e1ef180b16f82c3 # v3.1.1
-
       - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
-        with:
-          ## fetch the whole repository, as we want to push to it later
-          fetch-depth: 0
-
-      - name: prune ProofWidgets .lake
-        run: |
-          # The ProofWidgets release contains not just the `.js` (which we need in order to build)
-          # but also `.oleans`, which may have been built with the wrong toolchain.
-          # This removes them.
-          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
-          rm -rf .lake/packages/proofwidgets/.lake/build/lib
-          rm -rf .lake/packages/proofwidgets/.lake/build/ir
 
       - name: Configure Lean
         uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
@@ -40,31 +20,22 @@ jobs:
           use-github-cache: false
           use-mathlib-cache: true
 
-      - name: build mathlib
-        id: build
-        uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
-        with:
-          linters: lean
-          run: |
-            bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
-
       - name: update nolints.json
         shell: bash
         run: |
           env LEAN_ABORT_ON_PANIC=1 lake exe runLinter --update Mathlib
 
-      - name: configure git setup
-        run: |
-          git remote add origin-bot "https://leanprover-community-bot:${{ secrets.UPDATE_NOLINTS_TOKEN }}@github.com/leanprover-community/mathlib4.git"
-          git config user.email "leanprover.community@gmail.com"
-          git config user.name "leanprover-community-bot"
-
-          # By default, github actions overrides the credentials used to access any
-          # github url so that it uses the github-actions[bot] user.  We want to access
-          # github using a different username.
-          git config --unset http.https://github.com/.extraheader
-
-      - name: file a new PR to update nolints.json
-        run: ./scripts/update_nolints_CI.sh
-        env:
-          DEPLOY_GITHUB_TOKEN: ${{ secrets.UPDATE_NOLINTS_TOKEN }}
+      - name: Create Pull Request
+        uses: peter-evans/create-pull-request@271a8d0340265f705b14b6d32b9829c1cb33d45e # v7.0.8
+        with:
+          token: "${{ secrets.UPDATE_NOLINTS_TOKEN }}"
+          author: "leanprover-community-bot <leanprover.community@gmail.com>"
+          commit-message: "chore(scripts): update nolints.json"
+          branch: "nolints"
+          base: master
+          title: "chore(scripts): update nolints.json"
+          body: |
+            I am happy to remove some nolints for you!
+
+            [workflow run for this PR](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})
+          labels: "auto-merge-after-CI"

.github/workflows/update_dependencies.yml

@@ -9,6 +9,8 @@ jobs:
   update-dependencies:
     runs-on: ubuntu-latest
     if: github.repository == 'leanprover-community/mathlib4'
+    env:
+      BRANCH_NAME: "update-dependencies-bot-use-only"
     steps:
       - name: Checkout repository
         uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
@@ -23,13 +25,28 @@ jobs:
           use-github-cache: false
           use-mathlib-cache: false
 
+      - name: Get branch SHA if it exists
+        id: get-branch-sha
+        run: |
+          # Check if the branch exists remotely
+          if git fetch origin "$BRANCH_NAME"; then
+            SHA=$(git rev-parse "origin/$BRANCH_NAME")
+            echo "Branch '$BRANCH_NAME' exists with SHA: $SHA"
+            echo "sha=$SHA" >> "${GITHUB_OUTPUT}"
+          else
+            echo "Branch '$BRANCH_NAME' does not exist"
+            echo "sha=" >>" ${GITHUB_OUTPUT}"
+          fi
+
       - name: Get PR and labels
+        if: ${{ steps.get-branch-sha.outputs.sha != '' }}
         id: PR # all the steps below are skipped if 'ready-to-merge' is in the list of labels found here
         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
         with:
           github-token: ${{ secrets.GITHUB_TOKEN }}
+          sha: ${{ steps.get-branch-sha.outputs.sha }}
           # Only return if PR is still open
           filterOutClosed: true
 
@@ -40,12 +57,6 @@ jobs:
           prNumber: ${{ steps.PR.outputs.number }}
           prUrl: ${{ steps.PR.outputs.pr_url }}
 
-      - name: Configure Git User
-        if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}
-        run: |
-          git config user.name "leanprover-community-mathlib4-bot"
-          git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
-
       - name: Update dependencies
         if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}
         run: lake update -v
@@ -61,22 +72,44 @@ jobs:
             echo "toolchain_modified=false" >> "$GITHUB_OUTPUT"
           fi
 
-      - name: Generate PR title
+      - name: Check if lake-manifest.json was modified
         if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') && steps.check_toolchain.outputs.toolchain_modified != 'true' }}
+        id: check_manifest
+        run: |
+          if [ -n "${{ steps.get-branch-sha.outputs.sha }}" ]; then
+            # Branch exists, compare the file
+            if git diff --quiet HEAD "origin/$BRANCH_NAME" -- lake-manifest.json; then
+              echo "has_diff=false" >> "${GITHUB_OUTPUT}"
+              echo "No differences in lake-manifest.json"
+            else
+              echo "has_diff=true" >> "${GITHUB_OUTPUT}"
+              echo "Differences found in lake-manifest.json"
+            fi
+          else
+            # Branch doesn't exist, consider it as different
+            echo "has_diff=true" >> "${GITHUB_OUTPUT}"
+            echo "Branch does not exist, treating as different"
+          fi
+
+      - name: Generate PR title
+        if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') && steps.check_manifest.outputs.has_diff == 'true' }}
         run: |
           echo "timestamp=$(date -u +"%Y-%m-%d-%H-%M")" >> "$GITHUB_ENV"
           echo "pr_title=chore: update Mathlib dependencies $(date -u +"%Y-%m-%d")" >> "$GITHUB_ENV"
 
       - name: Create Pull Request
-        if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') && steps.check_toolchain.outputs.toolchain_modified != 'true' }}
+        if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') && steps.check_manifest.outputs.has_diff == 'true' }}
         uses: peter-evans/create-pull-request@271a8d0340265f705b14b6d32b9829c1cb33d45e # v7.0.8
         with:
           token: "${{ secrets.UPDATE_DEPENDENCIES_TOKEN }}"
           author: "leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>"
           commit-message: "chore: update Mathlib dependencies ${{ env.timestamp }}"
           # this branch is referenced in update_dependencies_zulip.yml
-          branch: "update-dependencies-bot-use-only"
+          branch: ${{ env.BRANCH_NAME }}
           base: master
           title: "${{ env.pr_title }}"
-          body: "This PR updates the Mathlib dependencies."
+          body: |
+            This PR updates the Mathlib dependencies.
+
+            [workflow run for this PR](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})
           labels: "auto-merge-after-CI"

Archive/Arithcc.lean

@@ -209,13 +209,13 @@ protected theorem StateEq.refl (t : Register) (ζ : State) : ζ ≃[t] ζ := by
 
 @[symm]
 protected theorem StateEq.symm {t : Register} (ζ₁ ζ₂ : State) : ζ₁ ≃[t] ζ₂ → ζ₂ ≃[t] ζ₁ := by
-  simp [StateEq]; intros
+  simp only [StateEq, and_imp]; intros
   constructor <;> (symm; assumption)
 
 @[trans]
 protected theorem StateEq.trans {t : Register} (ζ₁ ζ₂ ζ₃ : State) :
     ζ₁ ≃[t] ζ₂ → ζ₂ ≃[t] ζ₃ → ζ₁ ≃[t] ζ₃ := by
-  simp [StateEq]; intros
+  simp only [StateEq, and_imp]; intros
   constructor
   · simp_all only
   · trans ζ₂ <;> assumption
@@ -227,7 +227,7 @@ instance (t : Register) : Trans (StateEq (t + 1)) (StateEq (t + 1)) (StateEq (t
 @[trans]
 protected theorem StateEqStateEqRs.trans (t : Register) (ζ₁ ζ₂ ζ₃ : State) :
     ζ₁ ≃[t] ζ₂ → ζ₂ ≃[t]/ac ζ₃ → ζ₁ ≃[t]/ac ζ₃ := by
-  simp [StateEq]; intros
+  simp only [StateEq, and_imp]; intros
   trans ζ₂ <;> assumption
 
 instance (t : Register) : Trans (StateEq (t + 1)) (StateEqRs (t + 1)) (StateEqRs (t + 1)) :=
@@ -236,7 +236,7 @@ instance (t : Register) : Trans (StateEq (t + 1)) (StateEqRs (t + 1)) (StateEqRs
 /-- Writing the same value to register `t` gives `≃[t + 1]` from `≃[t]`. -/
 theorem stateEq_implies_write_eq {t : Register} {ζ₁ ζ₂ : State} (h : ζ₁ ≃[t] ζ₂) (v : Word) :
     write t v ζ₁ ≃[t + 1] write t v ζ₂ := by
-  simp [StateEq, StateEqRs] at *
+  simp only [StateEq, StateEqRs, write] at *
   constructor; · exact h.1
   intro r hr
   have hr : r ≤ t := Register.le_of_lt_succ hr
@@ -249,15 +249,15 @@ theorem stateEq_implies_write_eq {t : Register} {ζ₁ ζ₂ : State} (h : ζ₁
 /-- Writing the same value to any register preserves `≃[t]/ac`. -/
 theorem stateEqRs_implies_write_eq_rs {t : Register} {ζ₁ ζ₂ : State} (h : ζ₁ ≃[t]/ac ζ₂)
     (r : Register) (v : Word) : write r v ζ₁ ≃[t]/ac write r v ζ₂ := by
-  simp [StateEqRs] at *
+  simp only [StateEqRs, write] at *
   intro r' hr'
   specialize h r' hr'
   congr
 
 /-- `≃[t + 1]` with writing to register `t` implies `≃[t]`. -/
 theorem write_eq_implies_stateEq {t : Register} {v : Word} {ζ₁ ζ₂ : State}
     (h : ζ₁ ≃[t + 1] write t v ζ₂) : ζ₁ ≃[t] ζ₂ := by
-  simp [StateEq, StateEqRs] at *
+  simp only [StateEq, write, StateEqRs] at *
   constructor; · exact h.1
   intro r hr
   obtain ⟨_, h⟩ := h
@@ -313,10 +313,10 @@ theorem compiler_correctness
     have hζ₃ : ζ₃ ≃[t + 1] { write t ν₁ η with ac := ν₂ } := calc
       ζ₃ = outcome (compile map e_s₂ (t + 1)) ζ₂ := by simp_all
       _ ≃[t + 1] { ζ₂ with ac := ν₂ } := by apply e_ih_s₂ <;> assumption
-      _ ≃[t + 1] { write t ν₁ η with ac := ν₂ } := by simp [StateEq]; apply hζ₂
+      _ ≃[t + 1] { write t ν₁ η with ac := ν₂ } := by simpa [StateEq]
     have hζ₃_ν₂ : ζ₃.ac = ν₂ := by simp_all [StateEq]
     have hζ₃_ν₁ : read t ζ₃ = ν₁ := by
-      simp [StateEq, StateEqRs] at hζ₃ ⊢
+      simp only [StateEq, StateEqRs, write, read] at hζ₃ ⊢
       obtain ⟨_, hζ₃⟩ := hζ₃
       specialize hζ₃ t (Register.lt_succ_self _)
       simp_all

Archive/Imo/Imo2008Q2.lean

@@ -46,8 +46,8 @@ theorem imo2008_q2a (x y z : ℝ) (h : x * y * z = 1) (hx : x ≠ 1) (hy : y ≠
     x ^ 2 / (x - 1) ^ 2 + y ^ 2 / (y - 1) ^ 2 + z ^ 2 / (z - 1) ^ 2 ≥ 1 := by
   obtain ⟨a, b, c, ha, hb, hc, rfl, rfl, rfl⟩ := subst_abc h
   obtain ⟨m, n, rfl, rfl⟩ : ∃ m n, b = c - m ∧ a = c - m - n := by use c - b, b - a; simp
-  have hm_ne_zero : m ≠ 0 := by contrapose! hy; simp [field]; assumption
-  have hn_ne_zero : n ≠ 0 := by contrapose! hx; simp [field]; assumption
+  have hm_ne_zero : m ≠ 0 := by contrapose! hy; simpa [field]
+  have hn_ne_zero : n ≠ 0 := by contrapose! hx; simpa [field]
   have hmn_ne_zero : m + n ≠ 0 := by contrapose! hz; field_simp; linarith
   have hc_sub_sub : c - (c - m - n) = m + n := by abel
   rw [ge_iff_le, ← sub_nonneg]

Archive/Wiedijk100Theorems/CubingACube.lean

@@ -401,7 +401,7 @@ theorem mi_not_onBoundary (j : Fin n) : ¬OnBoundary (mi_mem_bcubes : mi h v ∈
     suffices ∀ j : Fin n, ite (j = j') x' ((cs i).b j.succ) ∈ c.side j.succ by
       simpa [p', bottom, toSet, tail, side_tail]
     intro j₂
-    by_cases hj₂ : j₂ = j'; · simp [hj₂]; apply tail_sub h2i'; apply hx'.1
+    by_cases hj₂ : j₂ = j'; · simpa [hj₂] using tail_sub h2i' _ hx'.1
     simp only [if_false, hj₂]; apply tail_sub hi; apply b_mem_side
   rcases v.1 hp' with ⟨_, ⟨i'', rfl⟩, hi''⟩
   have h2i'' : i'' ∈ bcubes cs c := ⟨hi''.1.symm, v.2.1 i'' hi''.1.symm ⟨tail p', hi''.2, hp'.2⟩⟩

Counterexamples.lean

@@ -15,6 +15,7 @@ import Counterexamples.MonicNonRegular
 import Counterexamples.Motzkin
 import Counterexamples.OrderedCancelAddCommMonoidWithBounds
 import Counterexamples.Phillips
+import Counterexamples.PolynomialIsDomain
 import Counterexamples.Pseudoelement
 import Counterexamples.QuadraticForm
 import Counterexamples.SeminormLatticeNotDistrib

Counterexamples/Phillips.lean

@@ -360,7 +360,7 @@ theorem discretePart_apply (f : BoundedAdditiveMeasure α) (s : Set α) :
 
 theorem continuousPart_apply_eq_zero_of_countable (f : BoundedAdditiveMeasure α) (s : Set α)
     (hs : s.Countable) : f.continuousPart s = 0 := by
-  simp [continuousPart]
+  simp only [continuousPart, restrict_apply]
   convert f.apply_countable s hs using 2
   ext x
   simp [and_comm]

Counterexamples/PolynomialIsDomain.lean

@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2025 Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Junyan Xu
+-/
+import Mathlib.Algebra.GroupWithZero.TransferInstance
+import Mathlib.Algebra.Order.Ring.Nat
+import Mathlib.Algebra.Ring.Equiv
+import Mathlib.RingTheory.Polynomial.Opposites
+
+/-!
+# A commutative semiring that is a domain whose polynomial semiring is not a domain
+
+`NatMaxAdd` is the natural numbers equipped with the usual multiplication but with maximum as
+addition. Under these operations it is a commutative semiring that is a domain, but
+`1 + 1 = 1 + 0 = 1` in this semiring so addition is not cancellative.
+As a consequence, the polynomial semiring `NatMaxAdd[X]` is not a domain,
+even though it has no zero-divisors other than 0.
+-/
+
+/-- A type synonym for ℕ equipped with maximum as addition. -/
+def NatMaxAdd := ℕ
+
+open scoped Polynomial
+
+namespace NatMaxAdd
+
+/-- Identification of `NatMaxAdd` with `ℕ`. -/
+protected abbrev mk : ℕ ≃ NatMaxAdd := Equiv.refl _
+
+attribute [irreducible] NatMaxAdd
+
+open NatMaxAdd (mk)
+
+instance : AddCommSemigroup NatMaxAdd where
+  add a b := mk (mk.symm a ⊔ mk.symm b)
+  add_assoc _ _ _ := mk.symm.injective (sup_assoc ..)
+  add_comm _ _ := mk.symm.injective (sup_comm ..)
+
+instance : AddZeroClass NatMaxAdd where
+  zero := mk 0
+  zero_add _ := mk.symm.injective (bot_sup_eq _)
+  add_zero _ := mk.symm.injective (sup_bot_eq _)
+
+instance : CommMonoidWithZero NatMaxAdd := mk.symm.commMonoidWithZero
+
+/-- `NatMaxAdd` is isomorphic to `ℕ` multiplicatively. -/
+protected def mulEquiv : NatMaxAdd ≃* ℕ where
+  __ := mk.symm
+  map_mul' _ _ := rfl
+
+instance : CommSemiring NatMaxAdd where
+  nsmul := nsmulRec
+  left_distrib _ _ _ := mk.symm.injective (Nat.mul_max_mul_left ..).symm
+  right_distrib _ _ _ := mk.symm.injective (Nat.mul_max_mul_right ..).symm
+
+instance : IsDomain NatMaxAdd := NatMaxAdd.mulEquiv.isDomain
+
+theorem natCast_eq_one (n : ℕ) : ∀ [NeZero n], (n : NatMaxAdd) = 1 := by
+  induction n with
+  | zero => intro; exact (NeZero.ne 0 rfl).elim
+  | succ n ih =>
+    obtain _ | n := n
+    · intro; rfl
+    · rw [Nat.cast_succ, ih]; intro; rfl
+
+theorem not_isCancelAdd : ¬ IsCancelAdd NatMaxAdd := fun h ↦ by cases @h.1.1 1 0 1 rfl
+
+theorem not_isDomain_polynomial : ¬ IsDomain NatMaxAdd[X] :=
+  Polynomial.isDomain_iff.not.mpr fun h ↦ not_isCancelAdd h.2
+
+theorem noZeroDivisors_polynomial : NoZeroDivisors NatMaxAdd[X] := inferInstance
+
+end NatMaxAdd
+
+theorem not_isDomain_commSemiring_imp_isDomain_polynomial :
+    ¬ ∀ (R : Type) [CommSemiring R] [IsDomain R], IsDomain R[X] :=
+  fun h ↦ NatMaxAdd.not_isDomain_polynomial (h _)