Merge branch 'leanprover-community:master' into main

Author: CoolRmal

.github/build.in.yml

@@ -671,16 +671,6 @@ jobs:
           lint-bib-file: true
           ref: ${{ PR_BRANCH_REF }}
 
-  build_and_lint:
-    name: CI Success
-    if: FORK_CONDITION
-    needs: [style_lint, post_steps]
-    runs-on: ubuntu-latest
-    steps:
-      - name: succeed
-        run: |
-          echo "Success: Required build and lint checks completed!"
-
   final:
     name: Post-CI jobJOB_NAME
     if: FORK_CONDITION

.github/workflows/bors.yml

@@ -681,16 +681,6 @@ jobs:
           lint-bib-file: true
           ref: ${{ github.sha }}
 
-  build_and_lint:
-    name: CI Success
-    if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
-    needs: [style_lint, post_steps]
-    runs-on: ubuntu-latest
-    steps:
-      - name: succeed
-        run: |
-          echo "Success: Required build and lint checks completed!"
-
   final:
     name: Post-CI job
     if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'

.github/workflows/build.yml

@@ -688,16 +688,6 @@ jobs:
           lint-bib-file: true
           ref: ${{ github.sha }}
 
-  build_and_lint:
-    name: CI Success
-    if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
-    needs: [style_lint, post_steps]
-    runs-on: ubuntu-latest
-    steps:
-      - name: succeed
-        run: |
-          echo "Success: Required build and lint checks completed!"
-
   final:
     name: Post-CI job
     if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'

.github/workflows/build_fork.yml

@@ -685,16 +685,6 @@ jobs:
           lint-bib-file: true
           ref: ${{ github.event.pull_request.head.sha }}
 
-  build_and_lint:
-    name: CI Success
-    if: github.event.pull_request.head.repo.fork
-    needs: [style_lint, post_steps]
-    runs-on: ubuntu-latest
-    steps:
-      - name: succeed
-        run: |
-          echo "Success: Required build and lint checks completed!"
-
   final:
     name: Post-CI job (fork)
     if: github.event.pull_request.head.repo.fork

.github/workflows/label_new_contributor.yml

@@ -2,7 +2,10 @@ name: Label New Contributors
 
 # Written with ChatGPT: https://chat.openai.com/share/3777ceb1-d722-4705-bacd-ba3f04b387be
 
-on: pull_request_target
+on: 
+  pull_request_target:
+    types:
+      - opened
 
 # Limit permissions for GITHUB_TOKEN for the entire workflow
 permissions:
@@ -36,6 +39,10 @@ jobs:
             const issues = await github.paginate(opts)
             const pullRequestCount = issues.length;
 
+            // We could filter out bot users here, with:
+            // const isBot = (github.rest.users.getByUsername(creator).type === "Bot");
+            // But we choose to label PRs by new bot contributors as well.
+
             // Determine if the creator has 5 or fewer pull requests
             if (pullRequestCount <= 5) {
               // Add the "new-contributor" label to the current pull request

.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 "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/Imo/Imo2019Q2.lean

@@ -34,7 +34,7 @@ as `(2 : ℤ) • ∡ _ _ _ = (2 : ℤ) • ∡ _ _ _`.
 -/
 
 
-library_note "IMO geometry formalization conventions"/--
+library_note2 «IMO geometry formalization conventions» /--
 We apply the following conventions for formalizing IMO geometry problems. A problem is assumed
 to take place in the plane unless that is clearly not intended, so it is not required to prove
 that the points are coplanar (whether or not that in fact follows from the other conditions).