Merge branch 'GdeltaLCH' of https://github.com/CoolRmal/mathlib4 into GdeltaLCH

Author: CoolRmal

.github/workflows/daily.yml

@@ -25,33 +25,14 @@ jobs:
     runs-on: ubuntu-latest
     if: github.repository == 'leanprover-community/mathlib4'
     strategy:
+      fail-fast: false
       matrix:
         branch_type: [master, nightly]
     steps:
       # Checkout repository, so that we can fetch tags to decide which branch we want.
       - name: Checkout branch or tag
         uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
 
-      # this step needs to be run here while we have `mathlib4` checked out,
-      # or else `gh run view` will try to look for runs in `mathlib4-nightly-testing`
-      - name: Get URLs
-        id: urls
-        env:
-          GH_TOKEN: ${{ github.token }}
-        run: |
-          # adapted from https://cmbuckley.co.uk/blog/2024/04/09/deep-links-to-github-actions-job-logs/
-          lean4checker_url=$(gh run view ${{ github.run_id }} --json jobs --jq '
-            .jobs[] | select(.name == "check-lean4checker (${{ matrix.branch_type }})")
-            | (.url + (.steps[] | select(.name == "Check environments using lean4checker")
-              | "#step:\(.number):1"))')
-          echo "lean4checker_url=$lean4checker_url" | tee -a "$GITHUB_OUTPUT"
-
-          mathlib_test_executable_url=$(gh run view ${{ github.run_id }} --json jobs --jq '
-            .jobs[] | select(.name == "check-lean4checker (${{ matrix.branch_type }})")
-            | (.url + (.steps[] | select(.name == "Run mathlib_test_executable")
-              | "#step:\(.number):1"))')
-          echo "mathlib_test_executable_url=$mathlib_test_executable_url" | tee -a "$GITHUB_OUTPUT"
-
       - name: Fetch latest tags (if nightly)
         if: matrix.branch_type == 'nightly'
         run: |
@@ -84,7 +65,7 @@ jobs:
           use-mathlib-cache: true
           reinstall-transient-toolchain: true
 
-      - name: Check environments using lean4checker # make sure this name is consistent with "Get URLs"
+      - name: Check environments using lean4checker # make sure this name is consistent with "Get job status and URLs" in the notify job
         id: lean4checker
         continue-on-error: true
         run: |
@@ -115,14 +96,51 @@ jobs:
           # so we explicitly check Batteries as well here.
           lake env lean4checker/.lake/build/bin/lean4checker Batteries Mathlib
 
-      - name: Run mathlib_test_executable # make sure this name is consistent with "Get URLs"
-        id: mathlib-test
-        continue-on-error: true
+  notify-lean4checker:
+    runs-on: ubuntu-latest
+    needs: check-lean4checker
+    if: github.repository == 'leanprover-community/mathlib4' && always()
+    strategy:
+      fail-fast: false
+      matrix:
+        branch_type: [master, nightly]
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
+
+      - name: Get job status and URLs
+        id: get-status
+        env:
+          GH_TOKEN: ${{ github.token }}
         run: |
-          lake exe mathlib_test_executable
+          JOB_NAME="check-lean4checker (${{ matrix.branch_type }})"
+          
+          # Get URL to the specific step
+          LEAN4CHECKER_URL=$(gh run view ${{ github.run_id }} --json jobs --jq \
+            ".jobs[] | select(.name == \"$JOB_NAME\") \
+            | (.url + (.steps[] | select(.name == \"Check environments using lean4checker\") \
+              | \"#step:\(.number):1\"))")
+          
+          echo "lean4checker_url=${LEAN4CHECKER_URL}" | tee -a "$GITHUB_OUTPUT"
+
+      - name: Fetch latest tags (if nightly)
+        if: matrix.branch_type == 'nightly'
+        run: |
+          git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git
+          git fetch nightly-testing --tags
+          LATEST_TAG=$(git tag | grep -E "${{ env.TAG_PATTERN }}" | sort -r | head -n 1)
+          echo "LATEST_TAG=${LATEST_TAG}" | tee -a "$GITHUB_ENV"
+
+      - name: Set branch ref
+        run: |
+          if [ "${{ matrix.branch_type }}" == "master" ]; then
+            echo "BRANCH_REF=${{ env.DEFAULT_BRANCH }}" >> "$GITHUB_ENV"
+          else
+            echo "BRANCH_REF=${{ env.LATEST_TAG }}" >> "$GITHUB_ENV"
+          fi
 
       - name: Post success message for lean4checker on Zulip
-        if: steps.lean4checker.outcome == 'success'
+        if: needs.check-lean4checker.result == 'success'
         uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
         with:
           api-key: ${{ secrets.ZULIP_API_KEY }}
@@ -132,37 +150,129 @@ jobs:
           type: 'stream'
           topic: 'lean4checker'
           content: |
-            ✅ lean4checker [succeeded](${{ steps.urls.outputs.lean4checker_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
+            ✅ lean4checker [succeeded](${{ steps.get-status.outputs.lean4checker_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
 
-      - name: Post success message for mathlib_test_executable on Zulip
-        if: steps.mathlib-test.outcome == 'success'
+      - name: Post failure / cancelled message for lean4checker on Zulip
+        if: needs.check-lean4checker.result != 'success'
         uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
         with:
           api-key: ${{ secrets.ZULIP_API_KEY }}
           email: 'github-mathlib4-bot@leanprover.zulipchat.com'
           organization-url: 'https://leanprover.zulipchat.com'
           to: 'nightly-testing'
           type: 'stream'
-          topic: 'mathlib test executable'
+          topic: 'lean4checker failure'
           content: |
-            ✅ mathlib_test_executable [succeeded](${{ steps.urls.outputs.mathlib_test_executable_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
+            ❌ lean4checker [${{ needs.check-lean4checker.result }}](${{ steps.get-status.outputs.lean4checker_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
+
+  check-mathlib_test_executable:
+    runs-on: ubuntu-latest
+    if: github.repository == 'leanprover-community/mathlib4'
+    strategy:
+      fail-fast: false
+      matrix:
+        branch_type: [master, nightly]
+    steps:
+      # Checkout repository, so that we can fetch tags to decide which branch we want.
+      - name: Checkout branch or tag
+        uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
+
+      - name: Fetch latest tags (if nightly)
+        if: matrix.branch_type == 'nightly'
+        run: |
+          # When in nightly mode, fetch tags from the nightly-testing repository
+          git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git
+          git fetch nightly-testing --tags
+          LATEST_TAG=$(git tag | grep -E "${{ env.TAG_PATTERN }}" | sort -r | head -n 1)
+          echo "LATEST_TAG=${LATEST_TAG}" >> "$GITHUB_ENV"
+
+      - name: Set branch ref
+        run: |
+          if [ "${{ matrix.branch_type }}" == "master" ]; then
+            echo "BRANCH_REF=${{ env.DEFAULT_BRANCH }}" >> "$GITHUB_ENV"
+          else
+            echo "BRANCH_REF=${{ env.LATEST_TAG }}" >> "$GITHUB_ENV"
+          fi
+
+      # Checkout the branch or tag we want to test.
+      - name: Checkout branch or tag
+        uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
+        with:
+          repository: ${{ matrix.branch_type == 'nightly' && 'leanprover-community/mathlib4-nightly-testing' || github.repository }}
+          ref: ${{ env.BRANCH_REF }}
+
+      - name: Configure Lean
+        uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # v1.3.0
+        with:
+          auto-config: false
+          use-github-cache: false
+          use-mathlib-cache: true
+          reinstall-transient-toolchain: true
+
+      - name: Run mathlib_test_executable # make sure this name is consistent with "Get job status and URLs" in the notify job
+        id: mathlib-test
+        continue-on-error: true
+        run: |
+          lake exe mathlib_test_executable
+
+  notify-mathlib_test_executable:
+    runs-on: ubuntu-latest
+    needs: check-mathlib_test_executable
+    if: github.repository == 'leanprover-community/mathlib4' && always()
+    strategy:
+      fail-fast: false
+      matrix:
+        branch_type: [master, nightly]
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
+
+      - name: Get job status and URLs
+        id: get-status
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          JOB_NAME="check-mathlib_test_executable (${{ matrix.branch_type }})"
+          
+          # Get URL to the specific step
+          MATHLIB_TEST_EXECUTABLE_URL=$(gh run view ${{ github.run_id }} --json jobs --jq \
+            ".jobs[] | select(.name == \"$JOB_NAME\") \
+            | (.url + (.steps[] | select(.name == \"Run mathlib_test_executable\") \
+              | \"#step:\(.number):1\"))")
+          
+          echo "mathlib_test_executable_url=${MATHLIB_TEST_EXECUTABLE_URL}" | tee -a "$GITHUB_OUTPUT"
+
+      - name: Fetch latest tags (if nightly)
+        if: matrix.branch_type == 'nightly'
+        run: |
+          git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git
+          git fetch nightly-testing --tags
+          LATEST_TAG=$(git tag | grep -E "${{ env.TAG_PATTERN }}" | sort -r | head -n 1)
+          echo "LATEST_TAG=${LATEST_TAG}" | tee -a "$GITHUB_ENV"
+
+      - name: Set branch ref
+        run: |
+          if [ "${{ matrix.branch_type }}" == "master" ]; then
+            echo "BRANCH_REF=${{ env.DEFAULT_BRANCH }}" >> "$GITHUB_ENV"
+          else
+            echo "BRANCH_REF=${{ env.LATEST_TAG }}" >> "$GITHUB_ENV"
+          fi
 
-      - name: Post failure message for lean4checker on Zulip
-        if: steps.lean4checker.outcome == 'failure'
+      - name: Post success message for mathlib_test_executable on Zulip
+        if: needs.check-mathlib_test_executable.result == 'success'
         uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
         with:
           api-key: ${{ secrets.ZULIP_API_KEY }}
           email: 'github-mathlib4-bot@leanprover.zulipchat.com'
           organization-url: 'https://leanprover.zulipchat.com'
           to: 'nightly-testing'
           type: 'stream'
-          topic: 'lean4checker failure'
+          topic: 'mathlib test executable'
           content: |
-            ❌ lean4checker [failed](${{ steps.urls.outputs.lean4checker_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
-        continue-on-error: true
+            ✅ mathlib_test_executable [succeeded](${{ steps.get-status.outputs.mathlib_test_executable_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
 
-      - name: Post failure message for mathlib_test_executable on Zulip
-        if: steps.mathlib-test.outcome == 'failure'
+      - name: Post failure / cancelled message for mathlib_test_executable on Zulip
+        if: needs.check-mathlib_test_executable.result != 'success'
         uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
         with:
           api-key: ${{ secrets.ZULIP_API_KEY }}
@@ -172,5 +282,4 @@ jobs:
           type: 'stream'
           topic: 'mathlib test executable failure'
           content: |
-            ❌ mathlib_test_executable [failed](${{ steps.urls.outputs.mathlib_test_executable_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
-        continue-on-error: true
+            ❌ mathlib_test_executable [${{ needs.check-mathlib_test_executable.result }}](${{ steps.get-status.outputs.mathlib_test_executable_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})

.github/workflows/discover-lean-pr-testing.yml

@@ -18,11 +18,12 @@ jobs:
       with:
         ref: nightly-testing
         fetch-depth: 0  # Fetch all branches
+        token: ${{ secrets.NIGHTLY_TESTING }}
 
     - name: Set up Git
       run: |
-        git config --global user.name "github-actions"
-        git config --global user.email "github-actions@github.com"
+        git config --global user.name "leanprover-community-mathlib4-bot"
+        git config --global user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
 
     - name: Configure Lean
       uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # v1.3.0

.github/workflows/maintainer_merge.yml

@@ -29,7 +29,12 @@ jobs:
       EVENT_NAME: ${{ github.event_name }}
     name: Ping maintainers on Zulip
     runs-on: ubuntu-latest
-    if: github.repository == 'leanprover-community/mathlib4'
+    if: >- # crude check to skip running this on most reviews / comments
+      github.repository == 'leanprover-community/mathlib4' && 
+      (
+        contains(format('{0}{1}', github.event.comment.body, github.event.review.body), 'maintainer merge') || 
+        contains(format('{0}{1}', github.event.comment.body, github.event.review.body), 'maintainer delegate')
+      )
     steps:
       - name: Find maintainer merge/delegate
         id: merge_or_delegate

Archive.lean

@@ -57,6 +57,7 @@ import Archive.Imo.Imo2024Q2
 import Archive.Imo.Imo2024Q3
 import Archive.Imo.Imo2024Q5
 import Archive.Imo.Imo2024Q6
+import Archive.Imo.Imo2025Q3
 import Archive.Kuratowski
 import Archive.MiuLanguage.Basic
 import Archive.MiuLanguage.DecisionNec
@@ -74,7 +75,6 @@ import Archive.Wiedijk100Theorems.FriendshipGraphs
 import Archive.Wiedijk100Theorems.HeronsFormula
 import Archive.Wiedijk100Theorems.InverseTriangleSum
 import Archive.Wiedijk100Theorems.Konigsberg
-import Archive.Wiedijk100Theorems.Partition
 import Archive.Wiedijk100Theorems.PerfectNumbers
 import Archive.Wiedijk100Theorems.SolutionOfCubicQuartic
 import Archive.Wiedijk100Theorems.SumOfPrimeReciprocalsDiverges

Archive/Examples/MersennePrimes.lean

@@ -10,7 +10,7 @@ import Mathlib.NumberTheory.LucasLehmer
 
 We run some Lucas-Lehmer tests to prove the first Mersenne primes are prime.
 
-See the discussion at the end of [Mathlib/NumberTheory/LucasLehmer.lean]
+See the discussion at the end of `Mathlib/NumberTheory/LucasLehmer.lean`
 for ideas about extending this to larger Mersenne primes.
 -/
 

Archive/Imo/Imo1960Q1.lean

@@ -45,14 +45,14 @@ theorem ge_100 {n : ℕ} (h1 : ProblemPredicate n) : 100 ≤ n := by
     rw [← h1.left]
     refine Nat.base_pow_length_digits_le 10 n ?_ (not_zero h1)
     simp
-  omega
+  lia
 
 theorem lt_1000 {n : ℕ} (h1 : ProblemPredicate n) : n < 1000 := by
   have h2 : n < 10 ^ 3 := by
     rw [← h1.left]
     refine Nat.lt_base_pow_length_digits ?_
     simp
-  omega
+  lia
 
 /-
 We do an exhaustive search to show that all results are covered by `SolutionPredicate`.
@@ -70,7 +70,7 @@ theorem searchUpTo_step {c n} (H : SearchUpTo c n) {c' n'} (ec : c + 1 = c') (en
   refine ⟨by ring, fun m l p => ?_⟩
   obtain ⟨h₁, ⟨m, rfl⟩, h₂⟩ := id p
   by_cases h : 11 * m < c * 11; · exact H _ h p
-  obtain rfl : m = c := by omega
+  obtain rfl : m = c := by lia
   rw [Nat.mul_div_cancel_left _ (by simp : 11 > 0), mul_comm] at h₂
   refine (H' h₂).imp ?_ ?_ <;> · rintro rfl; norm_num
 

Archive/Imo/Imo1962Q1.lean

@@ -53,31 +53,31 @@ Now we can eliminate possibilities for `(digits 10 c).length` until we get to th
 lemma case_0_digits {c n : ℕ} (hc : (digits 10 c).length = 0) : ¬ProblemPredicate' c n := by
   intro hpp
   have hpow : 6 * 10 ^ 0 = 6 * 10 ^ (digits 10 c).length := by rw [hc]
-  omega
+  lia
 
 lemma case_1_digits {c n : ℕ} (hc : (digits 10 c).length = 1) : ¬ProblemPredicate' c n := by
   intro hpp
   have hpow : 6 * 10 ^ 1 = 6 * 10 ^ (digits 10 c).length := by rw [hc]
-  omega
+  lia
 
 lemma case_2_digits {c n : ℕ} (hc : (digits 10 c).length = 2) : ¬ProblemPredicate' c n := by
   intro hpp
   have hpow : 6 * 10 ^ 2 = 6 * 10 ^ (digits 10 c).length := by rw [hc]
-  omega
+  lia
 
 lemma case_3_digits {c n : ℕ} (hc : (digits 10 c).length = 3) : ¬ProblemPredicate' c n := by
   intro hpp
   have hpow : 6 * 10 ^ 3 = 6 * 10 ^ (digits 10 c).length := by rw [hc]
-  omega
+  lia
 
 lemma case_4_digits {c n : ℕ} (hc : (digits 10 c).length = 4) : ¬ProblemPredicate' c n := by
   intro hpp
   have hpow : 6 * 10 ^ 4 = 6 * 10 ^ (digits 10 c).length := by rw [hc]
-  omega
+  lia
 
 /-- Putting this inline causes a deep recursion error, so we separate it out. -/
 private lemma helper_5_digits {c : ℤ} (hc : 6 * 10 ^ 5 + c = 4 * (10 * c + 6)) : c = 15384 := by
-  omega
+  lia
 
 lemma case_5_digits {c n : ℕ} (hc : (digits 10 c).length = 5) (hpp : ProblemPredicate' c n) :
     c = 15384 := by