Merge branch 'master' into YK-normed-alternating

.github/build.in.yml

@@ -127,16 +127,6 @@ jobs:
         run: |
           lake build cache
 
-      - name: prune ProofWidgets .lake
-        run: |
-          lake build proofwidgets:release
-          # 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: get cache
         id: get
         run: |
@@ -250,7 +240,7 @@ jobs:
 
       - name: check declarations in db files
         run: |
-          python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
+          python3 scripts/yaml_check.py docs/100.yaml docs/1000.yaml docs/overview.yaml docs/undergrad.yaml
           lake exe check-yaml
 
       - name: generate our import graph

.github/dependabot.yml

@@ -3,7 +3,8 @@ version: 2  # Specifies the version of the Dependabot configuration file format
 updates:
   # Configuration for dependency updates
   - package-ecosystem: "github-actions"  # Specifies the ecosystem to check for updates
-    directory: "/"  # Specifies the directory to check for dependencies; "/" means the root directory
+    directories: 
+      - "/.github/*" # covers `build.in.yml` as well, which is not in `.github/workflows/` because it shouldn't be run in CI.
     schedule:
       # Check for updates to GitHub Actions every month
       interval: "monthly"

.github/workflows/bors.yml

@@ -137,16 +137,6 @@ jobs:
         run: |
           lake build cache
 
-      - name: prune ProofWidgets .lake
-        run: |
-          lake build proofwidgets:release
-          # 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: get cache
         id: get
         run: |
@@ -260,7 +250,7 @@ jobs:
 
       - name: check declarations in db files
         run: |
-          python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
+          python3 scripts/yaml_check.py docs/100.yaml docs/1000.yaml docs/overview.yaml docs/undergrad.yaml
           lake exe check-yaml
 
       - name: generate our import graph

.github/workflows/build.yml

@@ -144,16 +144,6 @@ jobs:
         run: |
           lake build cache
 
-      - name: prune ProofWidgets .lake
-        run: |
-          lake build proofwidgets:release
-          # 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: get cache
         id: get
         run: |
@@ -267,7 +257,7 @@ jobs:
 
       - name: check declarations in db files
         run: |
-          python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
+          python3 scripts/yaml_check.py docs/100.yaml docs/1000.yaml docs/overview.yaml docs/undergrad.yaml
           lake exe check-yaml
 
       - name: generate our import graph

.github/workflows/build_fork.yml

@@ -141,16 +141,6 @@ jobs:
         run: |
           lake build cache
 
-      - name: prune ProofWidgets .lake
-        run: |
-          lake build proofwidgets:release
-          # 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: get cache
         id: get
         run: |
@@ -264,7 +254,7 @@ jobs:
 
       - name: check declarations in db files
         run: |
-          python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
+          python3 scripts/yaml_check.py docs/100.yaml docs/1000.yaml docs/overview.yaml docs/undergrad.yaml
           lake exe check-yaml
 
       - name: generate our import graph

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

@@ -124,6 +124,22 @@ jobs:
           echo "branches_exist=true" >> "$GITHUB_ENV"
         fi
 
+    - name: Prepare Zulip message
+      id: zulip-message
+      run: |
+        BRANCHES="${{ steps.find-branches.outputs.branches }}"
+        {
+          printf "msg<<EOF\n"
+          printf "We will need to merge the following branches into \`nightly-testing\`:\n"
+          printf "\`\`\`bash\n"
+          for BRANCH in $BRANCHES; do
+            PR_NUMBER=$(echo "$BRANCH" | grep -oP '\d+$')
+            printf "scripts/merge-lean-testing-pr.sh %s   # %s\n" "$PR_NUMBER" "$BRANCH"
+          done
+          printf "\`\`\`\n"
+          printf "EOF"
+        } >> "$GITHUB_OUTPUT"
+
     - name: Send message on Zulip
       if: env.branches_exist == 'true'
       uses: zulip/github-actions-zulip/send-message@v1
@@ -133,8 +149,6 @@ jobs:
         organization-url: 'https://leanprover.zulipchat.com'
         to: 'nightly-testing'
         type: 'stream'
-        topic: 'Mathlib status updates'
+        topic: 'Mergeable lean testing PRs'
         content: |
-          We will need to merge the following branches into `nightly-testing`:
-
-          ${{ steps.find-branches.outputs.branches }}
+          ${{ steps.zulip-message.outputs.msg }}

.github/workflows/lean4checker.yml

@@ -1,19 +1,23 @@
-# https://chat.openai.com/share/26102e95-ac9c-4d03-a000-73e4f6cee8cd
 name: lean4checker Workflow
 
 on:
   schedule:
     - cron: '0 0 * * *'   # Runs at 00:00 UTC every day
   workflow_dispatch:
 
+env:
+  DEFAULT_BRANCH: master
+  TAG_PATTERN: '^nightly-testing-[0-9]{4}-[0-9]{2}-[0-9]{2}$'
+
 jobs:
   check-lean4checker:
-    runs-on: pr
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        branch_type: [master, nightly]
     steps:
-
-      - name: cleanup
+      - name: Cleanup
         run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
           # Delete all but the 5 most recent toolchains.
           # Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
           # Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
@@ -23,21 +27,24 @@ jobs:
               : # Do nothing on failure, but suppress errors
           fi
 
-      # The Hoskinson runners may not have jq installed, so do that now.
-      - name: 'Setup jq'
-        uses: dcarbone/[email protected]
-
-      - name: install elan
+      - name: Install elan
         run: |
           set -o pipefail
           curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
-      - name: Checkout master branch
+      - name: Fetch latest tags (if nightly)
+        if: matrix.branch_type == 'nightly'
+        run: |
+          git fetch --tags
+          LATEST_TAG=$(git tag | grep -E "${{ env.TAG_PATTERN }}" | sort -r | head -n 1)
+          echo "LATEST_TAG=${LATEST_TAG}" >> "$GITHUB_ENV"
+
+      - name: Checkout branch or tag
         uses: actions/checkout@v4
         with:
-          ref: 'master'
+          ref: ${{ matrix.branch_type == 'master' && env.DEFAULT_BRANCH || env.LATEST_TAG }}
 
       - name: If using a lean-pr-release toolchain, uninstall
         run: |
@@ -46,7 +53,7 @@ jobs:
             elan toolchain uninstall "$(cat lean-toolchain)"
           fi
 
-      - name: print lean and lake versions
+      - name: Print Lean and Lake versions
         run: |
           lean --version
           lake --version
@@ -55,16 +62,6 @@ jobs:
         run: |
           lake exe cache get
 
-      - 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
-          lake build ProofWidgets
-
       - name: Check environments using lean4checker
         id: lean4checker
         run: |
@@ -100,7 +97,7 @@ jobs:
           type: 'stream'
           topic: 'lean4checker'
           content: |
-            ✅ lean4checker [succeeded](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }}
+            ✅ lean4checker [succeeded](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }} (branch: ${{ matrix.branch_type == 'master' && 'master' || env.LATEST_TAG }})
 
       - name: Post failure message on Zulip
         if: failure()
@@ -113,7 +110,7 @@ jobs:
           type: 'stream'
           topic: 'lean4checker failure'
           content: |
-            ❌ lean4checker [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }}
+            ❌ lean4checker [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }} (branch: ${{ matrix.branch_type == 'master' && 'master' || env.LATEST_TAG }})
         continue-on-error: true
 
       - name: Post failure message on Zulip main topic
@@ -127,5 +124,5 @@ jobs:
           type: 'stream'
           topic: 'lean4checker'
           content: |
-            ❌ lean4checker [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }}
+            ❌ lean4checker [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }} (branch: ${{ matrix.branch_type == 'master' && 'master' || env.LATEST_TAG }})
         continue-on-error: true

.github/workflows/nightly_detect_failure.yml

@@ -51,7 +51,7 @@ jobs:
               git tag "nightly-testing-${version}"
               git push origin "nightly-testing-${version}"
               hash="$(git rev-parse "nightly-testing-${version}")"
-              curl -X POST "http://speed.lean-fro.org/mathlib4/api/queue/commit/e7b27246-a3e6-496a-b552-ff4b45c7236e/$hash" -u "admin:${{ secrets.SPEED }}"
+              curl -X POST "https://speed.lean-lang.org/mathlib4/api/queue/commit/e7b27246-a3e6-496a-b552-ff4b45c7236e/$hash" -u "admin:${{ secrets.SPEED }}"
           fi
           hash="$(git rev-parse "nightly-testing-${version}")"
           printf 'SHA=%s\n' "${hash}" >> "${GITHUB_ENV}"

.github/workflows/zulip_emoji_awaiting_author.yaml

@@ -0,0 +1,34 @@
+on:
+  pull_request:
+    types: [labeled, unlabeled]
+jobs:
+  set_pr_emoji:
+    if: github.event.label.name == 'awaiting-author'
+    runs-on: ubuntu-latest
+    steps:
+    - name: Checkout mathlib repository
+      uses: actions/checkout@v4
+      with:
+          sparse-checkout: |
+            scripts/zulip_emoji_merge_delegate.py
+
+    - name: Set up Python
+      uses: actions/setup-python@v5
+      with:
+        python-version: '3.x'
+
+    - name: Install dependencies
+      run: |
+        python -m pip install --upgrade pip
+        pip install zulip
+
+    - name: Add or remove emoji
+      env:
+        ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
+        ZULIP_EMAIL: [email protected]
+        ZULIP_SITE: https://leanprover.zulipchat.com
+        PR_NUMBER: ${{ github.event.number}}
+        LABEL_STATUS: ${{ github.event.action }}
+      run: |
+        printf $'Running the python script with pr "%s"\n' "$PR_NUMBER"
+        python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "$LABEL_STATUS" "$PR_NUMBER"

Archive/Imo/Imo1964Q1.lean

@@ -5,25 +5,17 @@ Authors: Kevin Buzzard
 -/
 import Mathlib.Tactic.IntervalCases
 import Mathlib.Data.Nat.ModEq
-import Mathlib.Tactic.Ring
 
 /-!
 # IMO 1964 Q1
 
 (a) Find all positive integers $n$ for which $2^n-1$ is divisible by $7$.
-
 (b) Prove that there is no positive integer $n$ for which $2^n+1$ is divisible by $7$.
 
-We define a predicate for the solutions in (a), and prove that it is the set of positive
-integers which are a multiple of 3.
--/
-
-
-/-!
-## Intermediate lemmas
+For (a), we find that the order of $2$ mod $7$ is $3$. Therefore for (b), it suffices to check
+$n = 0, 1, 2$.
 -/
 
-
 open Nat
 
 namespace Imo1964Q1
@@ -33,17 +25,13 @@ theorem two_pow_mod_seven (n : ℕ) : 2 ^ n ≡ 2 ^ (n % 3) [MOD 7] :=
   calc 2 ^ n = 2 ^ (3 * (n / 3) + t) := by rw [Nat.div_add_mod]
     _ = (2 ^ 3) ^ (n / 3) * 2 ^ t := by rw [pow_add, pow_mul]
     _ ≡ 1 ^ (n / 3) * 2 ^ t [MOD 7] := by gcongr; decide
-    _ = 2 ^ t := by ring
-
-/-!
-## The question
--/
+    _ = 2 ^ t := by rw [one_pow, one_mul]
 
+end Imo1964Q1
 
-def ProblemPredicate (n : ℕ) : Prop :=
-  7 ∣ 2 ^ n - 1
+open Imo1964Q1
 
-theorem imo1964_q1a (n : ℕ) (_ : 0 < n) : ProblemPredicate n ↔ 3 ∣ n := by
+theorem imo1964_q1a (n : ℕ) (_ : 0 < n) : 7 ∣ 2 ^ n - 1 ↔ 3 ∣ n := by
   let t := n % 3
   have : t < 3 := Nat.mod_lt _ (by decide)
   calc 7 ∣ 2 ^ n - 1 ↔ 2 ^ n ≡ 1 [MOD 7] := by
@@ -53,15 +41,11 @@ theorem imo1964_q1a (n : ℕ) (_ : 0 < n) : ProblemPredicate n ↔ 3 ∣ n := by
     _ ↔ t = 0 := by interval_cases t <;> decide
     _ ↔ 3 ∣ n := by rw [dvd_iff_mod_eq_zero]
 
-end Imo1964Q1
-
-open Imo1964Q1
-
 theorem imo1964_q1b (n : ℕ) : ¬7 ∣ 2 ^ n + 1 := by
   intro h
   let t := n % 3
   have : t < 3 := Nat.mod_lt _ (by decide)
   have H : 2 ^ t + 1 ≡ 0 [MOD 7] := calc
-    2 ^ t + 1 ≡ 2 ^ n + 1 [MOD 7 ] := by gcongr ?_ + 1; exact (two_pow_mod_seven n).symm
+    2 ^ t + 1 ≡ 2 ^ n + 1 [MOD 7] := by gcongr ?_ + 1; exact (two_pow_mod_seven n).symm
       _ ≡ 0 [MOD 7] := h.modEq_zero_nat
   interval_cases t <;> contradiction

Archive/Imo/Imo1972Q5.lean

@@ -80,11 +80,10 @@ This is a more concise version of the proof proposed by Ruben Van de Velde.
 -/
 theorem imo1972_q5' (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y) = 2 * f x * g y)
     (hf2 : BddAbove (Set.range fun x => ‖f x‖)) (hf3 : ∃ x, f x ≠ 0) (y : ℝ) : ‖g y‖ ≤ 1 := by
-  -- Porting note: moved `by_contra!` up to avoid a bug
-  by_contra! H
   obtain ⟨x, hx⟩ := hf3
   set k := ⨆ x, ‖f x‖
   have h : ∀ x, ‖f x‖ ≤ k := le_ciSup hf2
+  by_contra! H
   have hgy : 0 < ‖g y‖ := by linarith
   have k_pos : 0 < k := lt_of_lt_of_le (norm_pos_iff.mpr hx) (h x)
   have : k / ‖g y‖ < k := (div_lt_iff₀ hgy).mpr (lt_mul_of_one_lt_right k_pos H)

Archive/Imo/Imo2013Q1.lean

@@ -27,7 +27,6 @@ We prove a slightly more general version where k does not need to be strictly po
 
 namespace Imo2013Q1
 
--- Porting note: simplified proof using `positivity`
 theorem arith_lemma (k n : ℕ) : 0 < 2 * n + 2 ^ k.succ := by positivity
 
 theorem prod_lemma (m : ℕ → ℕ+) (k : ℕ) (nm : ℕ+) :