Merge branch 'leanprover-community:master' into yoh

.github/PULL_REQUEST_TEMPLATE.md

@@ -4,11 +4,29 @@
 PR is merged. Please leave a blank newline before the `---`, otherwise
 GitHub will format the text above it as a title.
 
+For details on the "pull request lifecycle" in mathlib, please see:
+https://leanprover-community.github.io/contribute/index.html
+
+In particular, note that most reviewers will only notice your PR
+if it passes the continuous integration checks.
+Please ask for help on https://leanprover.zulipchat.com if needed.
+
 To indicate co-authors, include lines at the bottom of the commit message
 (that is, before the `---`) using the following format:
 
 Co-authored-by: Author Name <author@email.com>
 
+If you are moving or deleting declarations, please include these lines at the bottom of the commit message
+(that is, before the `---`) using the following format:
+
+Moves:
+- Vector.* -> Mathlib.Vector.*
+- ...
+
+Deletions:
+- Nat.bit1_add_bit1
+- ...
+
 Any other comments you want to keep out of the PR commit should go
 below the `---`, and placed outside this HTML comment, or else they
 will be invisible to reviewers.
@@ -17,6 +35,7 @@ If this PR depends on other PRs, please list them below this comment,
 using the following format:
 - [ ] depends on: #abc [optional extra text]
 - [ ] depends on: #xyz [optional extra text]
+
 -->
 
 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

.github/workflows/PR_summary.yml

@@ -56,12 +56,16 @@ jobs:
         title="### PR summary"
 
         ## Import count comment
-        importCount=$(python ./scripts/import-graph-report.py base.json head.json changed_files.txt)
+        importCount=$(
+          python ./scripts/import-graph-report.py base.json head.json changed_files.txt
+          ./scripts/import_trans_difference.sh
+        )
+
         if [ "$(printf '%s' "${importCount}" | wc -l)" -gt 12 ]
         then
-          importCount="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Import changes" "${importCount}")"
+          importCount="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Import changes for modified files" "${importCount}")"
         else
-          importCount="$(printf '#### Import changes\n\n%s\n' "${importCount}")"
+          importCount="$(printf '#### Import changes for modified files\n\n%s\n' "${importCount}")"
         fi
 
         ## Declarations' diff comment

.github/workflows/lean4checker.yml

@@ -69,7 +69,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout v4.8.0
+          git checkout v4.9.0
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .

.github/workflows/nightly_detect_failure.yml

@@ -181,19 +181,33 @@ jobs:
       run: |
         import os
         import zulip
-        client = zulip.Client(email='github-mathlib4-bot@leanprover.zulipchat.com', api_key=os.getenv('ZULIP_API_KEY'), site='https://leanprover.zulipchat.com')
+        client = zulip.Client(email='github-mathlib4-bot@leanprover.zulipchat.com', api_key='${{ secrets.ZULIP_API_KEY }}', site='https://leanprover.zulipchat.com')
         current_version = os.getenv('NIGHTLY')
         bump_version = os.getenv('BUMP_VERSION')
         bump_branch = os.getenv('BUMP_BRANCH')
         print(f'Current version: {current_version}, Bump version: {bump_version}')
         if current_version > bump_version:
             print('Lean toolchain in `nightly-testing` is ahead of the bump branch.')
+            # Get the last message in the 'Mathlib bump branch reminders' topic
             request = {
-                'type': 'stream',
-                'to': 'nightly-testing',
-                'topic': 'Mathlib bump branch reminders',
-                'content': f"🛠️: it looks like it's time to create a new bump/nightly-{current_version} branch from nightly-testing, and then PR that to {bump_branch}."
+              'anchor': 'newest',
+              'num_before': 1,
+              'num_after': 0,
+              'narrow': [{'operator': 'stream', 'operand': 'nightly-testing'}, {'operator': 'topic', 'operand': 'Mathlib bump branch reminders'}],
+              'apply_markdown': False    # Otherwise the content test below fails.
             }
-            result = client.send_message(request)
+            response = client.get_messages(request)
+            messages = response['messages']
+            payload = f"🛠️: it looks like it's time to create a new bump/nightly-{current_version} branch from nightly-testing, and then PR that to {bump_branch}."
+            if not messages or messages[0]['content'] != payload:
+                # Post the reminder message
+                request = {
+                    'type': 'stream',
+                    'to': 'nightly-testing',
+                    'topic': 'Mathlib bump branch reminders',
+                    'content': payload
+                }
+                result = client.send_message(request)
+                print(result)
         else:
             print('No action needed.')

.github/workflows/update_dependencies_zulip.yml

@@ -7,39 +7,44 @@ on:
     workflows: ["continuous integration"]
     types:
       - completed
+    branches:
+      - 'update-dependencies-**'
 
 jobs:
   monitor-failures:
     runs-on: ubuntu-latest
-    if: ${{ github.event.workflow_run.conclusion == 'failure' && startsWith(github.event.workflow_run.head_branch, 'update-dependencies-') }}
+    if: ${{ github.event.workflow_run.conclusion == 'failure' }}
 
     steps:
-      - name: Checkout repository
-        uses: actions/checkout@v4
+      - name: Construct message
+        uses: actions/github-script@v7
+        id: construct_message
         with:
-          fetch-depth: 0
-          token: ${{ secrets.NIGHTLY_TESTING }}
-
-      - name: Set GH_TOKEN
-        run: echo "GH_TOKEN=${{ secrets.NIGHTLY_TESTING }}" >> "$GITHUB_ENV"
-
-      - name: Get PR number
-        id: get_pr
-        run: |
-          pr_number=$(gh pr list --state open --head "leanprover-community/mathlib4:${{ github.event.workflow_run.head_branch }}" --json number -q '.[0].number')
-          echo "pr_number=$pr_number" >> "$GITHUB_ENV"
-
-      - name: Update PR labels
-        if: env.pr_number
-        run: |
-          gh pr edit "${{ env.pr_number }}" --remove-label "auto-merge-after-CI" --add-label "awaiting-CI,awaiting-review"
-
-      - name: Get CI URL
-        id: ci_url
-        run: |
-          url="https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}"
-          curl -s "$url" |
-            awk -v url="$url" -F'/' '/^ *href/ {gsub(/"/, "", $NF); printf("summary<<EOF\n%s/job/%s\nEOF", url, $NF)}' >> "$GITHUB_OUTPUT"
+          github-token: ${{ secrets.NIGHTLY_TESTING }}
+          result-encoding: string
+          script: |
+            const owner = context.repo.owner, repo = context.repo.repo;
+            let output = "❌ `lake update` [failed](" + context.payload.workflow_run.html_url + "). "
+            let prs = context.payload.workflow_run.pull_requests
+            if (prs.length) {
+              for (let pr of prs) {
+                const { data: pullRequest } = await github.rest.pulls.get({
+                  owner,
+                  repo,
+                  pull_number: pr.number,
+                });
+                output += "Found [PR " + pr.number + "](" + pullRequest.html_url + "). "
+                await github.rest.issues.removeLabel({
+                  owner,
+                  repo,
+                  issue_number: pr.number,
+                  name: "auto-merge-after-CI",
+                });
+              }
+            } else {
+              output += "No PR found for this run!";
+            }
+            return output;
 
       - name: Send Zulip message
         uses: zulip/github-actions-zulip/send-message@v1
@@ -51,4 +56,4 @@ jobs:
           type: 'stream'
           topic: 'Mathlib `lake update` failure'
           content: |
-            ❌ `lake update` [failed](${{ steps.ci_url.outputs.summary }}) on ${{ github.sha }}
+            ${{ steps.construct_message.outputs.result }}

Archive/Examples/IfNormalization/Result.lean

@@ -28,6 +28,8 @@ We add some local simp lemmas so we can unfold the definitions of the normalizat
 attribute [local simp] normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars
   List.disjoint
 
+attribute [local simp] apply_ite ite_eq_iff'
+
 /-!
 Simp lemmas for `eval`.
 We don't want a `simp` lemma for `(ite i t e).eval` in general, only once we know the shape of `i`.
@@ -71,7 +73,7 @@ def normalize (l : AList (fun _ : ℕ => Bool)) :
       ⟨if t' = e' then t' else .ite (var v) t' e', by
         refine ⟨fun f => ?_, ?_, fun w b => ?_⟩
         · -- eval = eval
-          simp only [apply_ite, eval_ite_var]
+          simp? says simp only [apply_ite, eval_ite_var, ite_eq_iff']
           cases hfv : f v
           · simp_all
             congr
@@ -104,3 +106,5 @@ recall IfNormalization :=
 
 example : IfNormalization :=
   ⟨_, fun e => ⟨(IfExpr.normalize ∅ e).2.2.1, by simp [(IfExpr.normalize ∅ e).2.1]⟩⟩
+
+end IfExpr

Archive/Examples/IfNormalization/WithoutAesop.lean

@@ -94,8 +94,8 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
               · simp_all
         · have := ht₃ v
           have := he₃ v
-          simp_all? says simp_all only [Option.elim, normalized, Bool.and_eq_true,
-              Bool.not_eq_true', AList.lookup_insert_eq_none, ne_eq, AList.lookup_insert, imp_false]
+          simp_all? says simp_all only [normalized, Bool.and_eq_true, Bool.not_eq_true',
+            AList.lookup_insert_eq_none, ne_eq, AList.lookup_insert, imp_false]
           obtain ⟨⟨⟨tn, tc⟩, tr⟩, td⟩ := ht₂
           split <;> rename_i h'
           · subst h'
@@ -107,9 +107,9 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
           have := he₃ w
           by_cases h : w = v
           · subst h; simp_all
-          · simp_all? says simp_all only [Option.elim, normalized, Bool.and_eq_true,
-              Bool.not_eq_true', AList.lookup_insert_eq_none, ne_eq, not_false_eq_true,
-              AList.lookup_insert_ne, implies_true]
+          · simp_all? says simp_all only [normalized, Bool.and_eq_true, Bool.not_eq_true',
+              AList.lookup_insert_eq_none, ne_eq, not_false_eq_true, AList.lookup_insert_ne,
+              implies_true]
             obtain ⟨⟨⟨en, ec⟩, er⟩, ed⟩ := he₂
             split at b <;> rename_i h'
             · subst h'; simp_all
@@ -124,3 +124,5 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
 example : IfNormalization :=
   ⟨fun e => (normalize' ∅ e).1,
    fun e => ⟨(normalize' ∅ e).2.2.1, by simp [(normalize' ∅ e).2.1]⟩⟩
+
+end IfExpr

Archive/Imo/Imo1959Q1.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Lacker
 -/
 import Mathlib.Tactic.Ring
-import Mathlib.Data.Nat.Prime
+import Mathlib.Data.Nat.Prime.Basic
 
 #align_import imo.imo1959_q1 from "leanprover-community/mathlib"@"5f25c089cb34db4db112556f23c50d12da81b297"
 

Archive/Imo/Imo1959Q2.lean

@@ -110,3 +110,5 @@ theorem not_isGood_one : ¬IsGood x 1 := fun h ↦
 
 theorem isGood_two_iff : IsGood x 2 ↔ x = 3 / 2 :=
   (isGood_iff_of_sqrt_two_lt <| (sqrt_lt' two_pos).2 (by norm_num)).trans <| by norm_num
+
+end Imo1959Q2

Archive/Imo/Imo1960Q1.lean

@@ -42,7 +42,7 @@ def SolutionPredicate (n : ℕ) : Prop :=
 Proving that three digit numbers are the ones in [100, 1000).
 -/
 theorem not_zero {n : ℕ} (h1 : ProblemPredicate n) : n ≠ 0 :=
-  have h2 : Nat.digits 10 n ≠ List.nil := List.ne_nil_of_length_eq_succ h1.left
+  have h2 : Nat.digits 10 n ≠ List.nil := List.ne_nil_of_length_eq_add_one h1.left
   digits_ne_nil_iff_ne_zero.mp h2
 #align imo1960_q1.not_zero Imo1960Q1.not_zero
 

Archive/Imo/Imo1960Q2.lean

@@ -66,3 +66,5 @@ theorem isGood_iff {x} : IsGood x ↔ x ∈ Ico (-1/2) (45/8) \ {0} := by
       _ ↔ 2 * x + 1 < (7 / 2) ^ 2 := sqrt_lt' <| by positivity
       _ ↔ x < 45 / 8 := by constructor <;> intro <;> linarith
       _ ↔ x ∈ Ico (-1/2) (45/8) \ {0} := by simp [*]
+
+end Imo1960Q2

Archive/Imo/Imo1986Q5.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Data.Real.NNReal
+import Mathlib.Data.NNReal.Basic
 
 /-!
 # IMO 1986 Q5
@@ -82,3 +82,5 @@ theorem isGood_iff {f : ℝ≥0 → ℝ≥0} : IsGood f ↔ f = fun x ↦ 2 / (2
     | inr hy =>
       have : 2 ≤ x + y := le_add_left hy
       simp [tsub_eq_zero_of_le, *]
+
+end Imo1986Q5

Archive/Imo/Imo1988Q6.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
-import Mathlib.Data.Nat.Prime
+import Mathlib.Data.Nat.Prime.Defs
 import Mathlib.Data.Rat.Defs
 import Mathlib.Order.WellFounded
 import Mathlib.Tactic.Linarith

Archive/Imo/Imo1994Q1.lean

@@ -33,14 +33,13 @@ open Finset
 
 namespace Imo1994Q1
 
-theorem tedious (m : ℕ) (k : Fin (m + 1)) : m - (m + (m + 1 - ↑k)) % (m + 1) = ↑k := by
+theorem tedious (m : ℕ) (k : Fin (m + 1)) : m - ((m + 1 - ↑k) + m) % (m + 1) = ↑k := by
   cases' k with k hk
   rw [Nat.lt_succ_iff, le_iff_exists_add] at hk
   rcases hk with ⟨c, rfl⟩
-  have : k + c + (k + c + 1 - k) = c + (k + c + 1) := by
-    simp only [add_assoc, add_tsub_cancel_left, add_left_comm]
+  have : (k + c + 1 - k) + (k + c) = c + (k + c + 1) := by omega
   rw [Fin.val_mk, this, Nat.add_mod_right, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
-  linarith
+  omega
 #align imo1994_q1.tedious Imo1994Q1.tedious
 
 end Imo1994Q1

Archive/Imo/Imo1998Q2.lean

@@ -130,19 +130,16 @@ theorem A_fibre_over_contestant_card (c : C) :
       ((A r).filter fun a : AgreedTriple C J => a.contestant = c).card := by
   rw [A_fibre_over_contestant r]
   apply Finset.card_image_of_injOn
-  -- Porting note (#10936): used to be `tidy`. TODO: remove `ext` after `extCore` to `aesop`.
-  unfold Set.InjOn; intros; ext; all_goals aesop
+  unfold Set.InjOn
+  aesop
 #align imo1998_q2.A_fibre_over_contestant_card Imo1998Q2.A_fibre_over_contestant_card
 
 theorem A_fibre_over_judgePair {p : JudgePair J} (h : p.Distinct) :
     agreedContestants r p = ((A r).filter fun a : AgreedTriple C J => a.judgePair = p).image
     AgreedTriple.contestant := by
   dsimp only [A, agreedContestants]; ext c; constructor <;> intro h
   · rw [Finset.mem_image]; refine ⟨⟨c, p⟩, ?_⟩; aesop
-  -- Porting note: this used to be `finish`
-  · simp only [Finset.mem_filter, Finset.mem_image, Prod.exists] at h
-    rcases h with ⟨_, ⟨_, ⟨_, ⟨h, _⟩⟩⟩⟩
-    cases h; aesop
+  · aesop
 #align imo1998_q2.A_fibre_over_judge_pair Imo1998Q2.A_fibre_over_judgePair
 
 theorem A_fibre_over_judgePair_card {p : JudgePair J} (h : p.Distinct) :

Archive/Imo/Imo2005Q3.lean

@@ -7,6 +7,7 @@ import Mathlib.Data.Real.Basic
 import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Ring
 
 #align_import imo.imo2005_q3 from "leanprover-community/mathlib"@"308826471968962c6b59c7ff82a22757386603e3"
 

Archive/Imo/Imo2008Q2.lean

@@ -8,6 +8,7 @@ import Mathlib.Data.Set.Finite
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.Abel
 import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Ring
 
 #align_import imo.imo2008_q2 from "leanprover-community/mathlib"@"5f25c089cb34db4db112556f23c50d12da81b297"
 

Archive/Imo/Imo2008Q3.lean

@@ -5,7 +5,7 @@ Authors: Manuel Candales
 -/
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Real.Sqrt
-import Mathlib.Data.Nat.Prime
+import Mathlib.Data.Nat.Prime.Defs
 import Mathlib.NumberTheory.PrimesCongruentOne
 import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
 import Mathlib.Tactic.LinearCombination

Archive/Imo/Imo2008Q4.lean

@@ -5,7 +5,7 @@ Authors: Manuel Candales
 -/
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Real.Sqrt
-import Mathlib.Data.Real.NNReal
+import Mathlib.Data.NNReal.Basic
 import Mathlib.Tactic.LinearCombination
 
 #align_import imo.imo2008_q4 from "leanprover-community/mathlib"@"308826471968962c6b59c7ff82a22757386603e3"

Archive/Imo/Imo2019Q4.lean

@@ -5,6 +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.Tactic.IntervalCases
 import Mathlib.Tactic.GCongr
 

Archive/OxfordInvariants/Summer2021/Week3P1.lean

@@ -6,6 +6,7 @@ Authors: Yaël Dillies, Bhavik Mehta
 import Mathlib.Algebra.BigOperators.Ring
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Data.Nat.Cast.Field
+import Mathlib.Data.Nat.Cast.Order.Field
 
 #align_import oxford_invariants.«2021summer».week3_p1 from "leanprover-community/mathlib"@"328375597f2c0dd00522d9c2e5a33b6a6128feeb"
 

Archive/Wiedijk100Theorems/InverseTriangleSum.lean

@@ -6,6 +6,7 @@ Authors: Jalex Stark, Yury Kudryashov
 import Mathlib.Algebra.BigOperators.Group.Finset
 import Mathlib.Data.Real.Basic
 import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Ring
 
 #align_import wiedijk_100_theorems.inverse_triangle_sum from "leanprover-community/mathlib"@"5563b1b49e86e135e8c7b556da5ad2f5ff881cad"