Merge branch 'master' into MR-rewrite-more-style-linters

.github/workflows/bors.yml

@@ -224,12 +224,6 @@ jobs:
             lake build --no-build
           fi
 
-      - name: find `#`-commands
-        id: hash_commands
-        run: |
-          chmod u+x scripts/lint_hash_commands.sh
-          ./scripts/lint_hash_commands.sh
-
       - name: build archive
         id: archive
         run: |

.github/workflows/build.yml

@@ -231,12 +231,6 @@ jobs:
             lake build --no-build
           fi
 
-      - name: find `#`-commands
-        id: hash_commands
-        run: |
-          chmod u+x scripts/lint_hash_commands.sh
-          ./scripts/lint_hash_commands.sh
-
       - name: build archive
         id: archive
         run: |

.github/workflows/build.yml.in

@@ -210,12 +210,6 @@ jobs:
             lake build --no-build
           fi
 
-      - name: find `#`-commands
-        id: hash_commands
-        run: |
-          chmod u+x scripts/lint_hash_commands.sh
-          ./scripts/lint_hash_commands.sh
-
       - name: build archive
         id: archive
         run: |

.github/workflows/build_fork.yml

@@ -228,12 +228,6 @@ jobs:
             lake build --no-build
           fi
 
-      - name: find `#`-commands
-        id: hash_commands
-        run: |
-          chmod u+x scripts/lint_hash_commands.sh
-          ./scripts/lint_hash_commands.sh
-
       - name: build archive
         id: archive
         run: |

.github/workflows/label_new_contributor.yml

@@ -42,7 +42,7 @@ jobs:
             }
 
             // Create a check run with a message about the PR count by this author
-            const message = `Found ${pullRequestCount} PRs by this author.`;
+            const message = `Found ${pullRequestCount} PRs by ${creator}.`;
             await github.rest.checks.create({
               owner,
               repo,

.vscode/deprecated-alias.code-snippets

@@ -0,0 +1,9 @@
+{
+	"Deprecated alias for mathlib": {
+		"scope": "lean4",
+		"prefix": "deprecated alias",
+		"body": [
+			"@[deprecated (since := \"${CURRENT_YEAR}-${CURRENT_MONTH}-${CURRENT_DATE}\")] alias $1 := $2"
+		]
+	}
+}

Archive/Wiedijk100Theorems/Partition.lean

@@ -201,8 +201,8 @@ theorem partialGF_prop (α : Type*) [CommSemiring α] (n : ℕ) (s : Finset ℕ)
         simp only [smul_eq_mul, ne_eq, mul_eq_zero, Multiset.count_eq_zero]
         rw [not_or, not_not]
         simp only [Multiset.mem_toFinset, not_not, mem_filter] }
-  refine Finset.card_congr φ ?_ ?_ ?_
-  · intro a  ha
+  refine Finset.card_bij φ ?_ ?_ ?_
+  · intro a ha
     simp only [φ, not_forall, not_exists, not_and, exists_prop, mem_filter]
     rw [mem_piAntidiagonal']
     dsimp only [ne_eq, smul_eq_mul, id_eq, eq_mpr_eq_cast, le_eq_subset, Finsupp.coe_mk]
@@ -221,7 +221,7 @@ theorem partialGF_prop (α : Type*) [CommSemiring α] (n : ℕ) (s : Finset ℕ)
         apply ha.2
     · exact fun i _ => ⟨Multiset.count i a.parts, ha.1 i, rfl⟩
   · dsimp only
-    intro p₁ p₂ hp₁ hp₂ h
+    intro p₁ hp₁ p₂ hp₂ h
     apply Nat.Partition.ext
     simp only [true_and_iff, mem_univ, mem_filter] at hp₁ hp₂
     ext i

Mathlib.lean

@@ -265,6 +265,7 @@ import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import Mathlib.Algebra.GroupWithZero.Pi
 import Mathlib.Algebra.GroupWithZero.Prod
 import Mathlib.Algebra.GroupWithZero.Semiconj
+import Mathlib.Algebra.GroupWithZero.ULift
 import Mathlib.Algebra.GroupWithZero.Units.Basic
 import Mathlib.Algebra.GroupWithZero.Units.Equiv
 import Mathlib.Algebra.GroupWithZero.Units.Lemmas
@@ -1079,6 +1080,7 @@ import Mathlib.Analysis.NormedSpace.Star.Spectrum
 import Mathlib.Analysis.NormedSpace.Star.Unitization
 import Mathlib.Analysis.NormedSpace.TrivSqZeroExt
 import Mathlib.Analysis.NormedSpace.Unitization
+import Mathlib.Analysis.NormedSpace.UnitizationL1
 import Mathlib.Analysis.NormedSpace.Units
 import Mathlib.Analysis.NormedSpace.WeakDual
 import Mathlib.Analysis.NormedSpace.WithLp
@@ -1975,6 +1977,7 @@ import Mathlib.Data.List.Indexes
 import Mathlib.Data.List.Infix
 import Mathlib.Data.List.InsertNth
 import Mathlib.Data.List.Intervals
+import Mathlib.Data.List.Iterate
 import Mathlib.Data.List.Join
 import Mathlib.Data.List.Lattice
 import Mathlib.Data.List.Lemmas
@@ -3081,6 +3084,7 @@ import Mathlib.NumberTheory.LSeries.Convergence
 import Mathlib.NumberTheory.LSeries.Convolution
 import Mathlib.NumberTheory.LSeries.Deriv
 import Mathlib.NumberTheory.LSeries.Dirichlet
+import Mathlib.NumberTheory.LSeries.HurwitzZeta
 import Mathlib.NumberTheory.LSeries.HurwitzZetaEven
 import Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
 import Mathlib.NumberTheory.LSeries.Linearity
@@ -3780,6 +3784,7 @@ import Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithm
 import Mathlib.Tactic.Linarith.Verification
 import Mathlib.Tactic.LinearCombination
 import Mathlib.Tactic.Linter
+import Mathlib.Tactic.Linter.AttributeInstanceIn
 import Mathlib.Tactic.Linter.HashCommandLinter
 import Mathlib.Tactic.Linter.Lint
 import Mathlib.Tactic.Linter.TextBased

Mathlib/Algebra/BigOperators/Finsupp.lean

@@ -166,7 +166,7 @@ theorem onFinset_prod {s : Finset α} {f : α → M} {g : α → M → N} (hf :
 /-- Taking a product over `f : α →₀ M` is the same as multiplying the value on a single element
 `y ∈ f.support` by the product over `erase y f`. -/
 @[to_additive
-      " Taking a sum over over `f : α →₀ M` is the same as adding the value on a
+      " Taking a sum over `f : α →₀ M` is the same as adding the value on a
       single element `y ∈ f.support` to the sum over `erase y f`. "]
 theorem mul_prod_erase (f : α →₀ M) (y : α) (g : α → M → N) (hyf : y ∈ f.support) :
     g y (f y) * (erase y f).prod g = f.prod g := by

Mathlib/Algebra/BigOperators/Intervals.lean

@@ -146,6 +146,11 @@ theorem prod_Ioc_succ_top {a b : ℕ} (hab : a ≤ b) (f : ℕ → M) :
 #align finset.prod_Ioc_succ_top Finset.prod_Ioc_succ_top
 #align finset.sum_Ioc_succ_top Finset.sum_Ioc_succ_top
 
+@[to_additive]
+theorem prod_Icc_succ_top {a b : ℕ} (hab : a ≤ b + 1) (f : ℕ → M) :
+    (∏ k in Icc a (b + 1), f k) = (∏ k in Icc a b, f k) * f (b + 1) := by
+  rw [← Nat.Ico_succ_right, prod_Ico_succ_top hab, Nat.Ico_succ_right]
+
 @[to_additive]
 theorem prod_range_mul_prod_Ico (f : ℕ → M) {m n : ℕ} (h : m ≤ n) :
     ((∏ k in range m, f k) * ∏ k in Ico m n, f k) = ∏ k in range n, f k :=

Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

@@ -95,9 +95,9 @@ theorem nth_stream_fr_lt_one {ifp_n : IntFractPair K}
 theorem one_le_succ_nth_stream_b {ifp_succ_n : IntFractPair K}
     (succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n) : 1 ≤ ifp_succ_n.b := by
   obtain ⟨ifp_n, nth_stream_eq, stream_nth_fr_ne_zero, ⟨-⟩⟩ :
-    ∃ ifp_n,
-      IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
-  · exact succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq
+      ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0
+        ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n :=
+    succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq
   suffices 1 ≤ ifp_n.fr⁻¹ by rwa [IntFractPair.of, le_floor, cast_one]
   suffices ifp_n.fr ≤ 1 by
     have h : 0 < ifp_n.fr :=
@@ -473,9 +473,9 @@ theorem abs_sub_convergents_le (not_terminated_at_n : ¬(of v).TerminatedAt n) :
       ∃ ifp_succ_n, IntFractPair.stream v (n + 1) = some ifp_succ_n ∧ (ifp_succ_n.b : K) = gp.b :=
     IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some s_nth_eq
   obtain ⟨ifp_n, stream_nth_eq, stream_nth_fr_ne_zero, if_of_eq_ifp_succ_n⟩ :
-    ∃ ifp_n,
-      IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
-  · exact IntFractPair.succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq
+    ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0
+      ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n :=
+    IntFractPair.succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq
   let denom' := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
   -- now we can use `sub_convergents_eq` to simplify our goal
   suffices |(-1) ^ n / denom'| ≤ 1 / denom by

Mathlib/Algebra/Field/ULift.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Algebra.Field.Basic
-import Mathlib.Algebra.Group.ULift
+import Mathlib.Algebra.GroupWithZero.ULift
 
 #align_import algebra.field.ulift from "leanprover-community/mathlib"@"13e18cfa070ea337ea960176414f5ae3a1534aae"
 

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -925,9 +925,9 @@ theorem lcm_eq_of_associated_right [NormalizedGCDMonoid α] {m n : α} (h : Asso
 
 end LCM
 
-@[deprecated] alias GCDMonoid.prime_of_irreducible := Irreducible.prime
+@[deprecated (since := "2024-02-12")] alias GCDMonoid.prime_of_irreducible := Irreducible.prime
 #align gcd_monoid.prime_of_irreducible Irreducible.prime
-@[deprecated] alias GCDMonoid.irreducible_iff_prime := irreducible_iff_prime
+@[deprecated (since := "2024-02-12")] alias GCDMonoid.irreducible_iff_prime := irreducible_iff_prime
 #align gcd_monoid.irreducible_iff_prime irreducible_iff_prime
 
 end GCDMonoid

Mathlib/Algebra/Group/Aut.lean

@@ -27,6 +27,9 @@ equivalences (and other files that use them) before the group structure is defin
 MulAut, AddAut
 -/
 
+-- TODO after #13161
+-- assert_not_exists MonoidWithZero
+assert_not_exists Ring
 
 variable {A : Type*} {M : Type*} {G : Type*}
 

Mathlib/Algebra/Group/Basic.lean

@@ -22,6 +22,8 @@ one-liners from the corresponding axioms. For the definitions of semigroups, mon
 `Algebra/Group/Defs.lean`.
 -/
 
+assert_not_exists MonoidWithZero
+assert_not_exists DenselyOrdered
 
 open Function
 
@@ -1134,14 +1136,14 @@ theorem leftInverse_inv_mul_mul_right (c : G) :
 lemma pow_natAbs_eq_one : a ^ n.natAbs = 1 ↔ a ^ n = 1 := by cases n <;> simp
 
 set_option linter.existingAttributeWarning false in
-@[to_additive, deprecated pow_natAbs_eq_one]
+@[to_additive, deprecated pow_natAbs_eq_one (since := "2024-02-14")]
 lemma exists_pow_eq_one_of_zpow_eq_one (hn : n ≠ 0) (h : a ^ n = 1) :
     ∃ n : ℕ, 0 < n ∧ a ^ n = 1 := ⟨_, Int.natAbs_pos.2 hn, pow_natAbs_eq_one.2 h⟩
 #align exists_npow_eq_one_of_zpow_eq_one exists_pow_eq_one_of_zpow_eq_one
 #align exists_nsmul_eq_zero_of_zsmul_eq_zero exists_nsmul_eq_zero_of_zsmul_eq_zero
 
--- 2024-02-14
-attribute [deprecated natAbs_nsmul_eq_zero] exists_nsmul_eq_zero_of_zsmul_eq_zero
+attribute [deprecated natAbs_nsmul_eq_zero (since := "2024-02-14")]
+exists_nsmul_eq_zero_of_zsmul_eq_zero
 
 @[to_additive sub_nsmul]
 lemma pow_sub (a : G) {m n : ℕ} (h : n ≤ m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹ :=

Mathlib/Algebra/Group/Commutator.lean

@@ -12,6 +12,9 @@ import Mathlib.Data.Bracket
 # The bracket on a group given by commutator.
 -/
 
+assert_not_exists MonoidWithZero
+assert_not_exists DenselyOrdered
+
 /-- The commutator of two elements `g₁` and `g₂`. -/
 instance commutatorElement {G : Type*} [Group G] : Bracket G G :=
   ⟨fun g₁ g₂ ↦ g₁ * g₂ * g₁⁻¹ * g₂⁻¹⟩

Mathlib/Algebra/Group/ConjFinite.lean

@@ -13,6 +13,8 @@ import Mathlib.Data.Fintype.Units
 # Conjugacy of elements of finite groups
 -/
 
+-- TODO: After #13027,
+-- assert_not_exists MonoidWithZero
 
 variable {α : Type*} [Monoid α]
 

Mathlib/Algebra/Group/Defs.lean

@@ -46,6 +46,9 @@ See the module `Algebra.AddTorsor` for a motivating example for the name `VAdd`
 
 -/
 
+assert_not_exists MonoidWithZero
+assert_not_exists DenselyOrdered
+
 universe u v w
 
 open Function

Mathlib/Algebra/Group/Embedding.lean

@@ -12,6 +12,8 @@ import Mathlib.Logic.Embedding.Basic
 # The embedding of a cancellative semigroup into itself by multiplication by a fixed element.
 -/
 
+assert_not_exists MonoidWithZero
+assert_not_exists DenselyOrdered
 
 variable {G : Type*}
 

Mathlib/Algebra/Group/Even.lean

@@ -32,6 +32,7 @@ This file defines square and even elements in a monoid.
 -/
 
 assert_not_exists MonoidWithZero
+assert_not_exists DenselyOrdered
 
 open MulOpposite
 

Mathlib/Algebra/Group/Ext.lean

@@ -27,6 +27,9 @@ former uses `HMul.hMul` which is the canonical spelling.
 monoid, group, extensionality
 -/
 
+assert_not_exists MonoidWithZero
+assert_not_exists DenselyOrdered
+
 open Function
 
 universe u