Merge branch 'master' into acmepjz_lin_disj_subalg_1

.github/build.in.yml

@@ -33,7 +33,7 @@ jobs:
         uses: credfeto/action-case-checker@v1.3.0
 
       - name: Look for ignored files
-        uses: credfeto/action-no-ignored-files@v1.1.0
+        uses: credfeto/action-no-ignored-files@v1.2.0
 
       - name: "Check for Lean files with the executable bit set"
         shell: bash
@@ -92,7 +92,7 @@ jobs:
 
       # The Hoskinson runners may not have jq installed, so do that now.
       - name: 'Setup jq'
-        uses: dcarbone/install-jq-action@v1.0.1
+        uses: dcarbone/install-jq-action@v2.1.0
 
       - name: install elan
         run: |
@@ -303,7 +303,7 @@ jobs:
       - uses: actions/checkout@v4
 
       - id: PR
-        uses: 8BitJonny/gh-get-current-pr@2.2.0
+        uses: 8BitJonny/gh-get-current-pr@3.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/dependabot.yml

@@ -0,0 +1,9 @@
+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
+    schedule:
+      # Check for updates to GitHub Actions every month
+      interval: "monthly"

.github/workflows/bench_summary_comment.yml

@@ -0,0 +1,35 @@
+name: Bench output summary
+
+on:
+  issue_comment:
+    types: created
+
+jobs:
+  Produce_bench_summary:
+    name: Post summary of benchmarking results
+    if: github.event.issue.pull_request && (startsWith(github.event.comment.body, 'Here are the [benchmark results]'))
+    runs-on: ubuntu-latest
+    steps:
+      - 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}"
+
+      - uses: actions/checkout@v4
+        with:
+          ref: master
+          sparse-checkout: |
+            scripts/bench_summary.lean
+
+      - name: Summarize bench output
+        run: |
+          {
+            cat scripts/bench_summary.lean
+            printf $'run_cmd BenchAction.addBenchSummaryComment %s "leanprover-community/mathlib4"' "${PR}"
+          } |
+            lake env lean --stdin
+        env:
+          PR:  ${{ github.event.issue.number }}
+          GH_TOKEN: ${{secrets.GITHUB_TOKEN}}

.github/workflows/bors.yml

@@ -43,7 +43,7 @@ jobs:
         uses: credfeto/action-case-checker@v1.3.0
 
       - name: Look for ignored files
-        uses: credfeto/action-no-ignored-files@v1.1.0
+        uses: credfeto/action-no-ignored-files@v1.2.0
 
       - name: "Check for Lean files with the executable bit set"
         shell: bash
@@ -102,7 +102,7 @@ jobs:
 
       # The Hoskinson runners may not have jq installed, so do that now.
       - name: 'Setup jq'
-        uses: dcarbone/install-jq-action@v1.0.1
+        uses: dcarbone/install-jq-action@v2.1.0
 
       - name: install elan
         run: |
@@ -313,7 +313,7 @@ jobs:
       - uses: actions/checkout@v4
 
       - id: PR
-        uses: 8BitJonny/gh-get-current-pr@2.2.0
+        uses: 8BitJonny/gh-get-current-pr@3.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/workflows/bot_fix_style_comment.yaml

@@ -41,7 +41,7 @@ jobs:
 
       - name: install Python
         if: steps.user_permission.outputs.require-result == 'true'
-        uses: actions/setup-python@v4
+        uses: actions/setup-python@v5
         with:
           python-version: 3.8
 

.github/workflows/bot_fix_style_review.yaml

@@ -47,7 +47,7 @@ jobs:
 
       - name: install Python
         if: steps.user_permission.outputs.require-result == 'true'
-        uses: actions/setup-python@v4
+        uses: actions/setup-python@v5
         with:
           python-version: 3.8
 

.github/workflows/bot_fix_style_review_comment.yaml

@@ -45,7 +45,7 @@ jobs:
 
       - name: install Python
         if: steps.user_permission.outputs.require-result == 'true'
-        uses: actions/setup-python@v4
+        uses: actions/setup-python@v5
         with:
           python-version: 3.8
 

.github/workflows/build.yml

@@ -50,7 +50,7 @@ jobs:
         uses: credfeto/action-case-checker@v1.3.0
 
       - name: Look for ignored files
-        uses: credfeto/action-no-ignored-files@v1.1.0
+        uses: credfeto/action-no-ignored-files@v1.2.0
 
       - name: "Check for Lean files with the executable bit set"
         shell: bash
@@ -109,7 +109,7 @@ jobs:
 
       # The Hoskinson runners may not have jq installed, so do that now.
       - name: 'Setup jq'
-        uses: dcarbone/install-jq-action@v1.0.1
+        uses: dcarbone/install-jq-action@v2.1.0
 
       - name: install elan
         run: |
@@ -320,7 +320,7 @@ jobs:
       - uses: actions/checkout@v4
 
       - id: PR
-        uses: 8BitJonny/gh-get-current-pr@2.2.0
+        uses: 8BitJonny/gh-get-current-pr@3.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/workflows/build_fork.yml

@@ -47,7 +47,7 @@ jobs:
         uses: credfeto/action-case-checker@v1.3.0
 
       - name: Look for ignored files
-        uses: credfeto/action-no-ignored-files@v1.1.0
+        uses: credfeto/action-no-ignored-files@v1.2.0
 
       - name: "Check for Lean files with the executable bit set"
         shell: bash
@@ -106,7 +106,7 @@ jobs:
 
       # The Hoskinson runners may not have jq installed, so do that now.
       - name: 'Setup jq'
-        uses: dcarbone/install-jq-action@v1.0.1
+        uses: dcarbone/install-jq-action@v2.1.0
 
       - name: install elan
         run: |
@@ -317,7 +317,7 @@ jobs:
       - uses: actions/checkout@v4
 
       - id: PR
-        uses: 8BitJonny/gh-get-current-pr@2.2.0
+        uses: 8BitJonny/gh-get-current-pr@3.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/workflows/dependent-issues.yml

@@ -11,7 +11,7 @@ jobs:
     runs-on: ubuntu-latest
     # timeout-minutes: 3
     steps:
-      - uses: styfle/cancel-workflow-action@0.11.0
+      - uses: styfle/cancel-workflow-action@0.12.1
         with:
           all_but_latest: true
           access_token: ${{ github.token }}

.github/workflows/labels_from_comment.yml

@@ -15,7 +15,7 @@ jobs:
 
     steps:
     - name: Add label based on comment
-      uses: actions/github-script@v6
+      uses: actions/github-script@v7
       with:
         github-token: ${{ secrets.GITHUB_TOKEN }}
         script: |

.github/workflows/lean4checker.yml

@@ -25,7 +25,7 @@ jobs:
 
       # The Hoskinson runners may not have jq installed, so do that now.
       - name: 'Setup jq'
-        uses: dcarbone/install-jq-action@v1.0.1
+        uses: dcarbone/install-jq-action@v2.1.0
 
       - name: install elan
         run: |

.github/workflows/lint_and_suggest_pr.yml

@@ -17,7 +17,7 @@ jobs:
       - uses: actions/checkout@v4
 
       - name: install Python
-        uses: actions/setup-python@v4
+        uses: actions/setup-python@v5
         with:
           python-version: 3.8
 

.github/workflows/maintainer_merge_comment.yml

@@ -52,7 +52,7 @@ jobs:
           body: |
             🚀 Pull request has been placed on the maintainer queue by ${{ github.event.comment.user.login }}.
       - name: Add label to PR
-        uses: actions/github-script@v6
+        uses: actions/github-script@v7
         with:
           github-token: ${{secrets.GITHUB_TOKEN}}
           script: |

.github/workflows/maintainer_merge_review.yml

@@ -51,7 +51,7 @@ jobs:
           body: |
             🚀 Pull request has been placed on the maintainer queue by ${{ github.event.review.user.login }}.
       - name: Add label to PR
-        uses: actions/github-script@v6
+        uses: actions/github-script@v7
         with:
           github-token: ${{secrets.GITHUB_TOKEN}}
           script: |

.github/workflows/maintainer_merge_review_comment.yml

@@ -50,7 +50,7 @@ jobs:
           body: |
             🚀 Pull request has been placed on the maintainer queue by ${{ github.event.comment.user.login }}.
       - name: Add label to PR
-        uses: actions/github-script@v6
+        uses: actions/github-script@v7
         with:
           github-token: ${{secrets.GITHUB_TOKEN}}
           script: |

.github/workflows/nolints.yml

@@ -16,7 +16,7 @@ jobs:
 
       # The Hoskinson runners may not have jq installed, so do that now.
       - name: 'Setup jq'
-        uses: dcarbone/install-jq-action@v1.0.1
+        uses: dcarbone/install-jq-action@v2.1.0
 
       - name: install elan
         run: |

.github/workflows/stale.yml

@@ -0,0 +1,25 @@
+name: 'Close stale issues and PRs'
+on:
+  schedule:
+    - cron: '30 1 * * *' # every day at 01:30 UTC
+  workflow_dispatch:
+
+jobs:
+  stale:
+    runs-on: ubuntu-latest
+    steps:
+      # until https://github.com/actions/stale/pull/1145 is merged
+      - uses: asterisk/github-actions-stale@main-only-matching-filter
+        with:
+          debug-only: 'true' # TODO: remove in follow-up PR after testing is done!
+          stale-pr-label: 'stale'
+          stale-pr-message: 'Message to comment on stale PRs.'
+          close-pr-label: 'closed-due-to-inactivity'
+          close-pr-message: 'Comment on the staled PRs while closed'
+          days-before-stale: 60
+          days-before-close: 120
+          # search string from the Zulip #queue link at https://bit.ly/4eo6brN
+          # "is:open is:pr -is:draft base:master sort:updated-asc status:success -label:blocked-by-other-PR -label:merge-conflict -label:awaiting-CI -label:WIP -label:awaiting-author -label:delegated -label:auto-merge-after-CI -label:ready-to-merge -label:please-adopt -label:help-wanted -label:awaiting-zulip"
+          # We want PRs _not_ on the queue, so we keep "is:pr -is:draft base:master" (is:open is added by the action by default) as a prefix for all queries and then negate the rest of the params in separate queries to simulate boolean OR (see https://github.com/actions/stale/pull/1145)
+          # except for label:auto-merge-after-CI and label:ready-to-merge which presumably will be noticed before they go stale
+          only-matching-filter: '[ "is:pr -is:draft base:master -status:success", "is:pr -is:draft base:master label:blocked-by-other-PR", "is:pr -is:draft base:master label:merge-conflict", "is:pr -is:draft base:master label:awaiting-CI", "is:pr -is:draft base:master label:WIP", "is:pr -is:draft base:master label:awaiting-author", "is:pr -is:draft base:master label:delegated", "is:pr -is:draft base:master label:please-adopt", "is:pr -is:draft base:master label:help-wanted", "is:pr -is:draft base:master label:awaiting-zulip" ]'

.github/workflows/update_dependencies.yml

@@ -57,7 +57,7 @@ jobs:
 
       - name: Create Pull Request
         if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}
-        uses: peter-evans/create-pull-request@v6
+        uses: peter-evans/create-pull-request@v7
         with:
           token: "${{ secrets.UPDATE_DEPENDENCIES_TOKEN }}"
           commit-message: "chore: update Mathlib dependencies ${{ env.timestamp }}"

Archive/Examples/MersennePrimes.lean

@@ -80,8 +80,22 @@ example : (mersenne 4253).Prime :=
 example : (mersenne 4423).Prime :=
   lucas_lehmer_sufficiency _ (by norm_num) (by norm_num)
 
--- First failure ("deep recursion detected")
 /-
-example : (mersenne 9689).Prime :=
-  lucas_lehmer_sufficiency _ (by norm_num) (by norm_num)
+`mersenne 9689` seems to be system dependent:
+locally it works fine, but in CI it fails with `(kernel) deep recursion detected`
+-/
+-- example : (mersenne 9689).Prime :=
+--   lucas_lehmer_sufficiency _ (by norm_num) (by norm_num)
+
+/-
+`mersenne 9941` seems to be system dependent:
+locally it works fine, but in CI it fails with `(kernel) deep recursion detected`
+-/
+-- example : (mersenne 9941).Prime :=
+--   lucas_lehmer_sufficiency _ (by norm_num) (by norm_num)
+
+/-
+`mersenne 11213` fails with `(kernel) deep recursion detected` locally as well.
 -/
+-- example : (mersenne 11213).Prime :=
+--   lucas_lehmer_sufficiency _ (by norm_num) (by norm_num)

Archive/Imo/Imo1986Q5.lean

@@ -71,7 +71,7 @@ theorem isGood_iff {f : ℝ≥0 → ℝ≥0} : IsGood f ↔ f = fun x ↦ 2 / (2
   refine ⟨fun hf ↦ funext hf.map_eq, ?_⟩
   rintro rfl
   constructor
-  case map_two => simp
+  case map_two => simp [tsub_self]
   case map_ne_zero => intro x hx; simpa [tsub_eq_zero_iff_le]
   case map_add_rev =>
     intro x y

Archive/Imo/Imo1994Q1.lean

@@ -43,7 +43,7 @@ end Imo1994Q1
 
 open Imo1994Q1
 
-theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : Finset ℕ) (hm : A.card = m + 1)
+theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : Finset ℕ) (hm : #A = m + 1)
     (hrange : ∀ a ∈ A, 0 < a ∧ a ≤ n)
     (hadd : ∀ a ∈ A, ∀ b ∈ A, a + b ≤ n → a + b ∈ A) :
     (m + 1) * (n + 1) ≤ 2 * ∑ x ∈ A, x := by

Archive/Imo/Imo1998Q2.lean

@@ -5,7 +5,7 @@ Authors: Oliver Nash
 -/
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Algebra.Order.Field.Basic
-import Mathlib.Algebra.Ring.Int
+import Mathlib.Algebra.Order.Field.Rat
 import Mathlib.GroupTheory.GroupAction.Ring
 import Mathlib.Tactic.NoncommRing
 import Mathlib.Tactic.Ring

Archive/Imo/Imo2013Q1.lean

@@ -3,12 +3,11 @@ Copyright (c) 2021 David Renshaw. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Renshaw
 -/
-import Mathlib.Algebra.BigOperators.Pi
-import Mathlib.Algebra.Order.Ring.Abs
-import Mathlib.Data.PNat.Basic
-import Mathlib.Tactic.Ring
+import Mathlib.Algebra.BigOperators.Group.Finset
+import Mathlib.Algebra.Order.Field.Rat
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.Positivity.Basic
+import Mathlib.Tactic.Ring
 
 /-!
 # IMO 2013 Q1

Archive/Imo/Imo2019Q4.lean

@@ -5,7 +5,7 @@ Authors: Floris van Doorn
 -/
 import Mathlib.Data.Nat.Factorial.BigOperators
 import Mathlib.Data.Nat.Multiplicity
-import Mathlib.Data.Nat.Prime.Basic
+import Mathlib.Data.Nat.Prime.Int
 import Mathlib.Tactic.IntervalCases
 import Mathlib.Tactic.GCongr
 

Archive/Imo/Imo2021Q1.lean

@@ -76,7 +76,7 @@ lemma exists_triplet_summing_to_squares {n : ℕ} (hn : 100 ≤ n) :
 -- pair of pairwise unequal elements of B sums to a perfect square.
 lemma exists_finset_3_le_card_with_pairs_summing_to_squares {n : ℕ} (hn : 100 ≤ n) :
     ∃ B : Finset ℕ,
-      2 * 1 + 1 ≤ B.card ∧
+      2 * 1 + 1 ≤ #B ∧
       (∀ a ∈ B, ∀ b ∈ B, a ≠ b → IsSquare (a + b)) ∧
       ∀ c ∈ B, n ≤ c ∧ c ≤ 2 * n := by
   obtain ⟨a, b, c, hna, hab, hbc, hcn, h₁, h₂, h₃⟩ := exists_triplet_summing_to_squares hn
@@ -115,7 +115,7 @@ theorem imo2021_q1 :
   obtain ⟨B, hB, h₁, h₂⟩ := exists_finset_3_le_card_with_pairs_summing_to_squares hn
   have hBsub : B ⊆ Finset.Icc n (2 * n) := by
     intro c hcB; simpa only [Finset.mem_Icc] using h₂ c hcB
-  have hB' : 2 * 1 < (B ∩ (Finset.Icc n (2 * n) \ A) ∪ B ∩ A).card := by
+  have hB' : 2 * 1 < #(B ∩ (Icc n (2 * n) \ A) ∪ B ∩ A) := by
     rwa [← inter_union_distrib_left, sdiff_union_self_eq_union, union_eq_left.2 hA,
       inter_eq_left.2 hBsub, ← Nat.succ_le_iff]
   -- Since B has cardinality greater or equal to 3, there must exist a subset C ⊆ B such that

Archive/MiuLanguage/DecisionNec.lean

@@ -5,9 +5,7 @@ Authors: Gihan Marasingha
 -/
 import Archive.MiuLanguage.Basic
 import Mathlib.Data.List.Basic
-import Mathlib.Data.List.Count
 import Mathlib.Data.Nat.ModEq
-import Mathlib.Tactic.Ring
 
 /-!
 # Decision procedure: necessary condition