Merge branch 'master' into MR-remove-lintstyle.sh

.github/workflows/lean4checker.yml

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

.github/workflows/lint_and_suggest_pr.yml

@@ -21,8 +21,15 @@ jobs:
         with:
           python-version: 3.8
 
+      - 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: lint
-        continue-on-error: true
+        continue-on-error: true  # allows the following `reviewdog` step to add GitHub suggestions
         run: |
           lake exe lint-style --fix
 
@@ -37,7 +44,7 @@ jobs:
           sudo apt-get install -y bibtool
 
       - name: lint references.bib
-        continue-on-error: true
+        continue-on-error: true  # allows the following `reviewdog` step to add GitHub suggestions
         run: |
           ./scripts/lint-bib.sh
 
@@ -65,6 +72,7 @@ jobs:
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
+        continue-on-error: true  # allows the following `reviewdog` step to add GitHub suggestions
         run: lake exe mk_all
 
       - name: suggester / import list

.github/workflows/nightly_bump_toolchain.yml

@@ -1,8 +1,9 @@
 name: Bump lean-toolchain on nightly-testing
 
 on:
+  workflow_dispatch:
   schedule:
-    - cron: '0 10 * * *'  # 11AM CET/2AM PT, 3 hours after lean4 starts building the nightly.
+    - cron: '0 10/3 * * *'  # Run every three hours, starting at 11AM CET/2AM PT.
 
 jobs:
   update-toolchain:
@@ -30,5 +31,6 @@ jobs:
         git config user.name "leanprover-community-mathlib4-bot"
         git config user.email "[email protected]"
         git add lean-toolchain
-        git commit -m "chore: bump to ${RELEASE_TAG}"
+        # Don't fail if there's nothing to commit
+        git commit -m "chore: bump to ${RELEASE_TAG}" || true
         git push origin nightly-testing

.github/workflows/nightly_detect_failure.yml

@@ -22,7 +22,7 @@ jobs:
         type: 'stream'
         topic: 'Mathlib status updates'
         content: |
-          ❌ The latest CI for Mathlib's branch#nightly-testing has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}).
+          ❌ The latest CI for Mathlib's branch#nightly-testing has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}) ([${{ github.sha }}](https://github.com/${{ github.repository }}/commit/${{ github.sha }})).
 
   handle_success:
     if: ${{ github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.head_branch == 'nightly-testing' }}
@@ -50,6 +50,7 @@ jobs:
               git tag "nightly-testing-${version}"
               git push origin "nightly-testing-${version}"
               hash="$(git rev-parse "nightly-testing-${version}")"
+              printf 'SHA=%s\n' "${hash}" >> "${GITHUB_ENV}"
               curl -X POST "http://speed.lean-fro.org/mathlib4/api/queue/commit/e7b27246-a3e6-496a-b552-ff4b45c7236e/$hash" -u "admin:${{ secrets.SPEED }}"
           fi
         else
@@ -83,9 +84,15 @@ jobs:
       run: pip install zulip
 
     - name: Check last message and post if necessary
+      env:
+        ZULIP_EMAIL: '[email protected]'
+        ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
+        ZULIP_SITE: 'https://leanprover.zulipchat.com'
+        SHA: ${{ env.SHA }}
       run: |
+        import os
         import zulip
-        client = zulip.Client(email='[email protected]', api_key='${{ secrets.ZULIP_API_KEY }}', site='https://leanprover.zulipchat.com')
+        client = zulip.Client(email=os.getenv('ZULIP_EMAIL'), api_key=os.getenv('ZULIP_API_KEY'), site=os.getenv('ZULIP_SITE'))
 
         # Get the last message in the 'status updates' topic
         request = {
@@ -97,20 +104,19 @@ jobs:
         }
         response = client.get_messages(request)
         messages = response['messages']
-        if not messages or messages[0]['content'] != "✅ The latest CI for Mathlib's branch#nightly-testing has succeeded!":
+        if not messages or messages[0]['content'] != f"✅ The latest CI for Mathlib's branch#nightly-testing has succeeded! ([{os.getenv('SHA')}](https://github.com/${{ github.repository }}/commit/{os.getenv('SHA')}))":
             # Post the success message
             request = {
                 'type': 'stream',
                 'to': 'nightly-testing',
                 'topic': 'Mathlib status updates',
-                'content': "✅ The latest CI for Mathlib's branch#nightly-testing has succeeded!"
+                'content': f"✅ The latest CI for Mathlib's branch#nightly-testing has succeeded! ([{os.getenv('SHA')}](https://github.com/${{ github.repository }}/commit/{os.getenv('SHA')}))"
             }
             result = client.send_message(request)
             print(result)
       shell: python
 
     # Next, determine if we should remind the humans to create a new PR to the `bump/v4.X.0` branch.
-    # https://chat.openai.com/share/504882f9-9d98-4d8d-ad19-5161c4a24fe1
 
     - name: Check for matching bump/nightly-YYYY-MM-DD branch
       id: check_branch
@@ -176,16 +182,18 @@ jobs:
       env:
         BUMP_VERSION: ${{ steps.bump_version.outputs.result }}
         BUMP_BRANCH: ${{ steps.latest_bump_branch.outputs.result }}
+        SHA: ${{ env.SHA }}
         ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
       shell: python
       run: |
         import os
         import zulip
-        client = zulip.Client(email='[email protected]', api_key='${{ secrets.ZULIP_API_KEY }}', site='https://leanprover.zulipchat.com')
+        client = zulip.Client(email='[email protected]', api_key=os.getenv('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}')
+        sha = os.getenv('SHA')
+        print(f'Current version: {current_version}, Bump version: {bump_version}, SHA: {sha}')
         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
@@ -199,7 +207,7 @@ jobs:
             response = client.get_messages(request)
             messages = response['messages']
             bump_branch_suffix = bump_branch.replace('bump/', '')
-            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}. "
+            payload = f"🛠️: it looks like it's time to create a new bump/nightly-{current_version} branch from nightly-testing (specifically {sha}), and then PR that to {bump_branch}. "
             payload += "To do so semi-automatically, run the following script from mathlib root:\n\n"
             payload += f"```bash\n./scripts/create-adaptation-pr.sh {bump_branch_suffix} {current_version}\n```\n"
             # Only post if the message is different

Archive.lean

@@ -40,6 +40,8 @@ import Archive.Imo.Imo2019Q2
 import Archive.Imo.Imo2019Q4
 import Archive.Imo.Imo2020Q2
 import Archive.Imo.Imo2021Q1
+import Archive.Imo.Imo2024Q1
+import Archive.Imo.Imo2024Q2
 import Archive.Imo.Imo2024Q6
 import Archive.MiuLanguage.Basic
 import Archive.MiuLanguage.DecisionNec

Archive/Hairer.lean

@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2023 Floris Van Doorn. All rights reserved.
+Copyright (c) 2023 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johan Commelin, Sébastien Gouëzel, Patrick Massot, Ruben Van de Velde, Floris Van Doorn,
+Authors: Johan Commelin, Sébastien Gouëzel, Patrick Massot, Ruben Van de Velde, Floris van Doorn,
 Junyan Xu
 -/
 import Mathlib.Algebra.MvPolynomial.Funext

Archive/Imo/Imo1972Q5.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ruben Van de Velde, Stanislas Polu
 -/
 import Mathlib.Data.Real.Basic
-import Mathlib.Analysis.NormedSpace.Basic
+import Mathlib.Analysis.Normed.Module.Basic
 
 /-!
 # IMO 1972 Q5

Archive/Imo/Imo1975Q1.lean

@@ -25,11 +25,10 @@ by the Rearrangement Inequality
 
 /- Let `n` be a natural number, `x` and `y` be as in the problem statement and `σ` be the
 permutation of natural numbers such that `z = y ∘ σ` -/
-variable (n : ℕ) (σ : Equiv.Perm ℕ) (hσ : {x | σ x ≠ x} ⊆ Finset.Icc 1 n) (x y : ℕ → ℝ)
-variable (hx : AntitoneOn x (Finset.Icc 1 n))
-variable (hy : AntitoneOn y (Finset.Icc 1 n))
+variable (n : ℕ) (σ : Equiv.Perm ℕ) (x y : ℕ → ℝ)
 
-theorem imo1975_q1 :
+theorem imo1975_q1 (hσ : {x | σ x ≠ x} ⊆ Finset.Icc 1 n)
+    (hx : AntitoneOn x (Finset.Icc 1 n)) (hy : AntitoneOn y (Finset.Icc 1 n)) :
     ∑ i ∈ Finset.Icc 1 n, (x i - y i) ^ 2 ≤ ∑ i ∈ Finset.Icc 1 n, (x i - y (σ i)) ^ 2 := by
   simp only [sub_sq, Finset.sum_add_distrib, Finset.sum_sub_distrib]
   -- a finite sum is invariant if we permute the order of summation

Archive/Imo/Imo1981Q3.lean

@@ -130,6 +130,7 @@ satisfying `NatPredicate m n N` are `fib K` and `fib (K+1)`, respectively.
 -/
 variable {K : ℕ} (HK : N < fib K + fib (K + 1)) {N}
 
+include HK in
 theorem m_n_bounds {m n : ℕ} (h1 : NatPredicate N m n) : m ≤ fib K ∧ n ≤ fib (K + 1) := by
   obtain ⟨k : ℕ, hm : m = fib k, hn : n = fib (k + 1)⟩ := h1.imp_fib m
   by_cases h2 : k < K + 1
@@ -156,6 +157,7 @@ theorem m_n_bounds {m n : ℕ} (h1 : NatPredicate N m n) : m ≤ fib K ∧ n ≤
 We spell out the consequences of this result for `specifiedSet N` here.
 -/
 variable {M : ℕ} (HM : M = fib K ^ 2 + fib (K + 1) ^ 2)
+include HK HM
 
 theorem k_bound {m n : ℤ} (h1 : ProblemPredicate N m n) : m ^ 2 + n ^ 2 ≤ M := by
   have h2 : 0 ≤ m := h1.m_range.left.le

Archive/Imo/Imo1986Q5.lean

@@ -38,6 +38,7 @@ structure IsGood (f : ℝ≥0 → ℝ≥0) : Prop where
 namespace IsGood
 
 variable {f : ℝ≥0 → ℝ≥0} (hf : IsGood f) {x y : ℝ≥0}
+include hf
 
 theorem map_add (x y : ℝ≥0) : f (x + y) = f (x * f y) * f y :=
   (hf.map_add_rev x y).symm

Archive/Imo/Imo1998Q2.lean

@@ -116,7 +116,7 @@ theorem A_fibre_over_contestant_card (c : C) :
   apply Finset.card_image_of_injOn
   unfold Set.InjOn
   rintro ⟨a, p⟩ h ⟨a', p'⟩ h' rfl
-  aesop
+  aesop (add simp AgreedTriple.contestant)
 
 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

Archive/Imo/Imo2008Q3.lean

@@ -43,7 +43,7 @@ theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4])
     simp only [n, Int.natAbs_sq, Int.natCast_pow, Int.ofNat_succ, Int.natCast_dvd_natCast.mp]
     refine (ZMod.intCast_zmod_eq_zero_iff_dvd (m ^ 2 + 1) p).mp ?_
     simp only [m, Int.cast_pow, Int.cast_add, Int.cast_one, ZMod.coe_valMinAbs]
-    rw [pow_two, ← hy]; exact add_left_neg 1
+    rw [pow_two, ← hy]; exact neg_add_cancel 1
   have hnat₂ : n ≤ p / 2 := ZMod.natAbs_valMinAbs_le y
   have hnat₃ : p ≥ 2 * n := by linarith [Nat.div_mul_le_self p 2]
   set k : ℕ := p - 2 * n with hnat₄

Archive/Imo/Imo2019Q2.lean

@@ -66,7 +66,7 @@ attribute [local instance] FiniteDimensional.of_fact_finrank_eq_two
 
 variable (V : Type*) (Pt : Type*)
 variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt]
-variable [NormedAddTorsor V Pt] [hd2 : Fact (finrank ℝ V = 2)]
+variable [NormedAddTorsor V Pt]
 
 namespace Imo2019Q2
 
@@ -96,7 +96,7 @@ structure Imo2019q2Cfg where
   C_ne_Q₁ : C ≠ Q₁
 
 /-- A default choice of orientation, for lemmas that need to pick one. -/
-def someOrientation : Module.Oriented ℝ V (Fin 2) :=
+def someOrientation [hd2 : Fact (finrank ℝ V = 2)] : Module.Oriented ℝ V (Fin 2) :=
   ⟨Basis.orientation (finBasisOfFinrankEq _ _ hd2.out)⟩
 
 variable {V Pt}
@@ -249,7 +249,7 @@ section Oriented
 
 variable [Module.Oriented ℝ V (Fin 2)]
 
-theorem oangle_CQ₁Q_sign_eq_oangle_CBA_sign :
+theorem oangle_CQ₁Q_sign_eq_oangle_CBA_sign [Fact (finrank ℝ V = 2)] :
     (∡ cfg.C cfg.Q₁ cfg.Q).sign = (∡ cfg.C cfg.B cfg.A).sign := by
   rw [← cfg.sbtw_Q_A₁_Q₁.symm.oangle_eq_right,
     cfg.sOppSide_CB_Q_Q₁.oangle_sign_eq_neg (left_mem_affineSpan_pair ℝ cfg.C cfg.B)
@@ -259,14 +259,18 @@ theorem oangle_CQ₁Q_sign_eq_oangle_CBA_sign :
     cfg.wbtw_B_Q_B₁.oangle_eq_right cfg.Q_ne_B,
     cfg.wbtw_A_B₁_C.symm.oangle_sign_eq_of_ne_left cfg.B cfg.B₁_ne_C.symm]
 
-theorem oangle_CQ₁Q_eq_oangle_CBA : ∡ cfg.C cfg.Q₁ cfg.Q = ∡ cfg.C cfg.B cfg.A :=
+theorem oangle_CQ₁Q_eq_oangle_CBA [Fact (finrank ℝ V = 2)] :
+    ∡ cfg.C cfg.Q₁ cfg.Q = ∡ cfg.C cfg.B cfg.A :=
   oangle_eq_of_angle_eq_of_sign_eq cfg.angle_CQ₁Q_eq_angle_CBA
     cfg.oangle_CQ₁Q_sign_eq_oangle_CBA_sign
 
 end Oriented
 
 /-! ### More obvious configuration properties -/
 
+section
+
+variable [hd2 : Fact (finrank ℝ V = 2)]
 
 theorem A₁_ne_B : cfg.A₁ ≠ cfg.B := by
   intro h
@@ -568,6 +572,8 @@ theorem result : Concyclic ({cfg.P, cfg.Q, cfg.P₁, cfg.Q₁} : Set Pt) := by
   simp only [Set.insert_subset_iff, Set.singleton_subset_iff]
   exact ⟨cfg.P_mem_ω, cfg.Q_mem_ω, cfg.P₁_mem_ω, cfg.Q₁_mem_ω⟩
 
+end
+
 end Imo2019q2Cfg
 
 end
@@ -576,7 +582,7 @@ end Imo2019Q2
 
 open Imo2019Q2
 
-theorem imo2019_q2 (A B C A₁ B₁ P Q P₁ Q₁ : Pt)
+theorem imo2019_q2 [Fact (finrank ℝ V = 2)] (A B C A₁ B₁ P Q P₁ Q₁ : Pt)
     (affine_independent_ABC : AffineIndependent ℝ ![A, B, C]) (wbtw_B_A₁_C : Wbtw ℝ B A₁ C)
     (wbtw_A_B₁_C : Wbtw ℝ A B₁ C) (wbtw_A_P_A₁ : Wbtw ℝ A P A₁) (wbtw_B_Q_B₁ : Wbtw ℝ B Q B₁)
     (PQ_parallel_AB : line[ℝ, P, Q] ∥ line[ℝ, A, B]) (P_ne_Q : P ≠ Q)