Merge branch 'master' into LL/KernelFst'Snd'

.github/workflows/bors.yml

@@ -44,6 +44,17 @@ jobs:
       - name: Look for ignored files
         uses: credfeto/[email protected]
 
+      - name: "Check for Lean files with the executable bit set"
+        shell: bash
+        run: |
+          executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))"
+          if [[ -n "$executable_files" ]]
+          then
+            echo "ERROR: The following Lean files have the executable bit set."
+            echo "$executable_files"
+            exit 1
+          fi
+
       - name: install Python
         if: ${{ 'bors' == 'ubuntu-latest' }}
         uses: actions/setup-python@v5
@@ -57,9 +68,9 @@ jobs:
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
-      - name: "run style linters: Python ones and their Lean rewrite"
+      - name: "run style linters"
         run: |
-          ./scripts/lint-style.sh
+          lake exe lint-style
 
       - name: Install bibtool
         if: ${{ 'bors' == 'ubuntu-latest' }}

.github/workflows/build.yml

@@ -51,6 +51,17 @@ jobs:
       - name: Look for ignored files
         uses: credfeto/[email protected]
 
+      - name: "Check for Lean files with the executable bit set"
+        shell: bash
+        run: |
+          executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))"
+          if [[ -n "$executable_files" ]]
+          then
+            echo "ERROR: The following Lean files have the executable bit set."
+            echo "$executable_files"
+            exit 1
+          fi
+
       - name: install Python
         if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
         uses: actions/setup-python@v5
@@ -64,9 +75,9 @@ jobs:
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
-      - name: "run style linters: Python ones and their Lean rewrite"
+      - name: "run style linters"
         run: |
-          ./scripts/lint-style.sh
+          lake exe lint-style
 
       - name: Install bibtool
         if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}

.github/workflows/build.yml.in

@@ -30,6 +30,17 @@ jobs:
       - name: Look for ignored files
         uses: credfeto/[email protected]
 
+      - name: "Check for Lean files with the executable bit set"
+        shell: bash
+        run: |
+          executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))"
+          if [[ -n "$executable_files" ]]
+          then
+            echo "ERROR: The following Lean files have the executable bit set."
+            echo "$executable_files"
+            exit 1
+          fi
+
       - name: install Python
         if: ${{ 'STYLE_LINT_RUNNER' == 'ubuntu-latest' }}
         uses: actions/setup-python@v5
@@ -43,9 +54,9 @@ jobs:
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
-      - name: "run style linters: Python ones and their Lean rewrite"
+      - name: "run style linters"
         run: |
-          ./scripts/lint-style.sh
+          lake exe lint-style
 
       - name: Install bibtool
         if: ${{ 'STYLE_LINT_RUNNER' == 'ubuntu-latest' }}

.github/workflows/build_fork.yml

@@ -48,6 +48,17 @@ jobs:
       - name: Look for ignored files
         uses: credfeto/[email protected]
 
+      - name: "Check for Lean files with the executable bit set"
+        shell: bash
+        run: |
+          executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))"
+          if [[ -n "$executable_files" ]]
+          then
+            echo "ERROR: The following Lean files have the executable bit set."
+            echo "$executable_files"
+            exit 1
+          fi
+
       - name: install Python
         if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
         uses: actions/setup-python@v5
@@ -61,9 +72,9 @@ jobs:
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
-      - name: "run style linters: Python ones and their Lean rewrite"
+      - name: "run style linters"
         run: |
-          ./scripts/lint-style.sh
+          lake exe lint-style
 
       - name: Install bibtool
         if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}

.github/workflows/lean4checker.yml

@@ -69,7 +69,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout v4.10.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

@@ -31,7 +31,7 @@ jobs:
       - name: lint
         continue-on-error: true  # allows the following `reviewdog` step to add GitHub suggestions
         run: |
-          ./scripts/lint-style.sh --fix
+          lake exe lint-style --fix
 
       - name: suggester / lint-style
         uses: reviewdog/action-suggester@v1

.github/workflows/nightly_detect_failure.yml

@@ -50,9 +50,10 @@ 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
+          hash="$(git rev-parse "nightly-testing-${version}")"
+          printf 'SHA=%s\n' "${hash}" >> "${GITHUB_ENV}"
         else
           echo "Error: The file lean-toolchain does not contain the expected pattern."
           exit 1

.github/workflows/nolints.yml

@@ -57,7 +57,7 @@ jobs:
         shell: bash
         run: |
           env LEAN_ABORT_ON_PANIC=1 lake exe runLinter --update Mathlib
-          lake exe lint_style --update
+          lake exe lint-style --update
 
       - name: configure git setup
         run: |

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/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/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)

Archive/Imo/Imo2024Q1.lean

@@ -60,6 +60,7 @@ lemma condition_toIcoMod_iff {α : ℝ} :
 namespace Condition
 
 variable {α : ℝ} (hc : Condition α)
+include hc
 
 lemma mem_Ico_one_of_mem_Ioo (h : α ∈ Set.Ioo 0 2) : α ∈ Set.Ico 1 2 := by
   rcases h with ⟨h0, h2⟩

Archive/Imo/Imo2024Q2.lean

@@ -47,6 +47,9 @@ namespace Condition
 
 variable {a b : ℕ} (h : Condition a b)
 
+section
+include h
+
 lemma a_pos : 0 < a := h.1
 
 lemma b_pos : 0 < b := h.2.1
@@ -79,6 +82,8 @@ lemma dvd_g_of_le_N_of_dvd {n : ℕ} (hn : h.N ≤ n) {d : ℕ} (hab : d ∣ a ^
   rw [← h.gcd_eq_g hn, Nat.dvd_gcd_iff]
   exact ⟨hab, hba⟩
 
+end
+
 lemma a_coprime_ab_add_one : a.Coprime (a * b + 1) := by
   simp
 
@@ -132,7 +137,7 @@ lemma ab_add_one_dvd_a_pow_large_n_add_b : a * b + 1 ∣ a ^ h.large_n + b := by
       (IsUnit.mul_right_eq_zero (ZMod.unitOfCoprime _ a_coprime_ab_add_one).isUnit).1 this
   rw [mul_add]
   norm_cast
-  simp only [mul_right_inv, Units.val_one, ZMod.coe_unitOfCoprime]
+  simp only [mul_inv_cancel, Units.val_one, ZMod.coe_unitOfCoprime]
   norm_cast
   convert ZMod.natCast_self (a * b + 1) using 2
   exact add_comm _ _
@@ -151,6 +156,8 @@ lemma ab_add_one_dvd_a_pow_large_n_0_add_b : a * b + 1 ∣ a ^ h.large_n_0 + b :
   rw [← h.gcd_eq_g h.N_le_large_n_0]
   exact Nat.gcd_dvd_left _ _
 
+include h
+
 lemma ab_add_one_dvd_b_add_one : a * b + 1 ∣ b + 1 := by
   rw [add_comm b]
   suffices a * b + 1 ∣ a ^ h.large_n_0 + b by

Archive/Imo/Imo2024Q6.lean

@@ -39,6 +39,7 @@ symmetric form). -/
 def Aquaesulian (f : G → G) : Prop := ∀ x y, f (f y + x) = f x + y ∨ f (f x + y) = f y + x
 
 variable {f : G → G} (h : Aquaesulian f)
+include h
 
 lemma Aquaesulian.apply_apply_add (x : G) : f (f x + x) = f x + x := by
   rcases h x x with hx | hx <;> exact hx
@@ -62,9 +63,9 @@ lemma Aquaesulian.apply_zero : f 0 = 0 := by
 @[simp]
 lemma Aquaesulian.apply_neg_apply_add (x : G) : f (-(f x)) + x = 0 := by
   rcases h x (-(f x)) with hc | hc
-  · rw [add_right_neg, ← h.apply_zero] at hc
+  · rw [add_neg_cancel, ← h.apply_zero] at hc
     exact h.injective hc
-  · rw [add_right_neg, h.apply_zero] at hc
+  · rw [add_neg_cancel, h.apply_zero] at hc
     exact hc.symm
 
 @[simp]

Archive/MiuLanguage/DecisionNec.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 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
@@ -71,9 +72,10 @@ theorem count_equiv_one_or_two_mod3_of_derivable (en : Miustr) :
   any_goals apply mod3_eq_1_or_mod3_eq_2 h_ih
   -- Porting note: `simp_rw [count_append]` usually doesn't work
   · left; rw [count_append, count_append]; rfl
-  · right; simp_rw [count_append, count_cons, if_false, two_mul]; simp
+  · right; simp_rw [count_append, count_cons, beq_iff_eq, ite_false, add_zero, two_mul]
   · left; rw [count_append, count_append, count_append]
-    simp_rw [count_cons_self, count_nil, count_cons, ite_false, add_right_comm, add_mod_right]
+    simp_rw [count_cons_self, count_nil, count_cons, beq_iff_eq, ite_false, add_right_comm,
+      add_mod_right]
     simp
   · left; rw [count_append, count_append, count_append]
     simp only [ne_eq, not_false_eq_true, count_cons_of_ne, count_nil, add_zero]
@@ -127,7 +129,7 @@ theorem goodm_of_rule1 (xs : Miustr) (h₁ : Derivable (xs ++ ↑[I])) (h₂ : G
   · change ¬M ∈ tail (xs ++ ↑([I] ++ [U]))
     rw [← append_assoc, tail_append_singleton_of_ne_nil]
     · simp_rw [mem_append, mem_singleton, or_false]; exact nmtail
-    · exact append_ne_nil_of_ne_nil_left _ _ this
+    · exact append_ne_nil_of_left_ne_nil this _
 
 theorem goodm_of_rule2 (xs : Miustr) (_ : Derivable (M :: xs)) (h₂ : Goodm (M :: xs)) :
     Goodm (↑(M :: xs) ++ xs) := by

Archive/MiuLanguage/DecisionSuf.lean

@@ -251,7 +251,7 @@ theorem count_I_eq_length_of_count_U_zero_and_neg_mem {ys : Miustr} (hu : count
     · -- case `x = M` gives a contradiction.
       exfalso; exact hm (mem_cons_self M xs)
     · -- case `x = I`
-      rw [count_cons, if_pos rfl, length, succ_inj']
+      rw [count_cons, beq_self_eq_true, if_pos rfl, length, succ_inj']
       apply hxs
       · simpa only [count]
       · rw [mem_cons, not_or] at hm; exact hm.2
@@ -307,7 +307,9 @@ theorem ind_hyp_suf (k : ℕ) (ys : Miustr) (hu : count U ys = succ k) (hdec : D
   use as, bs
   refine ⟨rfl, ?_, ?_, ?_⟩
   · -- Porting note: `simp_rw [count_append]` didn't work
-    rw [count_append] at hu; simp_rw [count_cons, if_true, add_succ, succ_inj'] at hu
+    rw [count_append] at hu
+    simp_rw [count_cons, beq_self_eq_true, if_true, add_succ, beq_iff_eq, reduceIte, add_zero,
+      succ_inj'] at hu
     rwa [count_append, count_append]
   · apply And.intro rfl
     rw [cons_append, cons_append]