Merge branch 'master' into ScottCarnahan/RootHomAPI

.github/build.in.yml

@@ -33,7 +33,7 @@ jobs:
         uses: credfeto/[email protected]
 
       - 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/[email protected]
 
       - 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/[email protected]
 
       - 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/[email protected]
 
       - 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/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/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/Sensitivity.lean

@@ -41,7 +41,7 @@ noncomputable section
 
 local notation "√" => Real.sqrt
 
-open Function Bool LinearMap Fintype Module Module.DualBases
+open Bool Finset Fintype Function LinearMap Module Module.DualBases
 
 /-!
 ### The hypercube
@@ -357,7 +357,7 @@ local notation "Span" => Submodule.span ℝ
 natural number. -/
 
 
-local notation "Card " X:70 => Finset.card (Set.toFinset X)
+local notation "Card " X:70 => #(Set.toFinset X)
 
 /-! In the following, `⊓` and `⊔` will denote intersection and sums of ℝ-subspaces,
 equipped with their subspace structures. The notations come from the general
@@ -431,20 +431,19 @@ theorem huang_degree_theorem (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :
       (norm_sum_le _ fun p => coeffs y p * _)
     _ = ∑ p ∈ (coeffs y).support, |coeffs y p| * ite (p ∈ q.adjacent) 1 0 := by
       simp only [abs_mul, f_matrix]
-    _ = ∑ p ∈ (coeffs y).support.filter q.adjacent, |coeffs y p| := by
-      simp [Finset.sum_filter]; rfl
-    _ ≤ ∑ _p ∈ (coeffs y).support.filter q.adjacent, |coeffs y q| :=
-      (Finset.sum_le_sum fun p _ => H_max p)
-    _ = (((coeffs y).support.filter q.adjacent).card : ℝ) * |coeffs y q| := by
-      rw [Finset.sum_const, nsmul_eq_mul]
-    _ = (((coeffs y).support ∩ q.adjacent.toFinset).card : ℝ) * |coeffs y q| := by
+    _ = ∑ p ∈ (coeffs y).support with q.adjacent p, |coeffs y p| := by
+      simp [sum_filter]; rfl
+    _ ≤ ∑ p ∈ (coeffs y).support with q.adjacent p, |coeffs y q| := sum_le_sum fun p _ ↦ H_max p
+    _ = #{p ∈ (coeffs y).support | q.adjacent p} * |coeffs y q| := by
+      rw [sum_const, nsmul_eq_mul]
+    _ = #((coeffs y).support ∩ q.adjacent.toFinset) * |coeffs y q| := by
       congr with x; simp; rfl
-    _ ≤ Finset.card (H ∩ q.adjacent).toFinset * |ε q y| := by
+    _ ≤ #(H ∩ q.adjacent).toFinset * |ε q y| := by
       refine (mul_le_mul_right H_q_pos).2 ?_
       norm_cast
-      apply Finset.card_le_card
+      apply card_le_card
       rw [Set.toFinset_inter]
-      convert Finset.inter_subset_inter_right coeffs_support
+      convert inter_subset_inter_right coeffs_support
 
 end
 

Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

@@ -39,8 +39,8 @@ We then show the pair of labels must be unique. Now if there is no increasing se
 which is a contradiction if there are more than `r * s` elements.
 -/
 theorem erdos_szekeres {r s n : ℕ} {f : Fin n → α} (hn : r * s < n) (hf : Injective f) :
-    (∃ t : Finset (Fin n), r < t.card ∧ StrictMonoOn f ↑t) ∨
-      ∃ t : Finset (Fin n), s < t.card ∧ StrictAntiOn f ↑t := by
+    (∃ t : Finset (Fin n), r < #t ∧ StrictMonoOn f ↑t) ∨
+      ∃ t : Finset (Fin n), s < #t ∧ StrictAntiOn f ↑t := by
   -- Given an index `i`, produce the set of increasing (resp., decreasing) subsequences which ends
   -- at `i`.
   let inc_sequences_ending_in : Fin n → Finset (Finset (Fin n)) := fun i =>