Trigger CI for leanprover-community/batteries#1112

Archive/Examples/IfNormalization/Result.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
 import Archive.Examples.IfNormalization.Statement
-import Mathlib.Algebra.Order.Monoid.Canonical.Defs
-import Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
 import Mathlib.Data.List.AList
 import Mathlib.Tactic.Recall
 

Archive/Examples/IfNormalization/WithoutAesop.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Kim Morrison
 -/
 import Archive.Examples.IfNormalization.Statement
-import Mathlib.Algebra.Order.Monoid.Canonical.Defs
-import Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
 import Mathlib.Data.List.AList
 
 /-!
@@ -20,7 +18,7 @@ we put primes on the declarations in the file.)
 namespace IfExpr
 
 attribute [local simp] eval normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars
-  List.disjoint max_add_add_right max_mul_mul_left Nat.lt_add_one_iff le_add_of_le_right
+  List.disjoint
 
 theorem eval_ite_ite' {a b c d e : IfExpr} {f : ℕ → Bool} :
     (ite (ite a b c) d e).eval f = (ite a (ite b d e) (ite c d e)).eval f := by

Archive/Wiedijk100Theorems/FriendshipGraphs.lean

@@ -5,9 +5,6 @@ Authors: Aaron Anderson, Jalex Stark, Kyle Miller
 -/
 import Mathlib.Combinatorics.SimpleGraph.AdjMatrix
 import Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
-import Mathlib.Data.Int.ModEq
-import Mathlib.Data.ZMod.Basic
-import Mathlib.Tactic.IntervalCases
 
 /-!
 # The Friendship Theorem

Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean

@@ -3,9 +3,8 @@ Copyright (c) 2021 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-import Mathlib.Data.ZMod.Basic
-import Mathlib.Algebra.Order.Monoid.Basic
 import Mathlib.Algebra.Ring.Subsemiring.Order
+import Mathlib.Data.ZMod.Basic
 
 /-!
 

Counterexamples/CliffordAlgebraNotInjective.lean

@@ -5,12 +5,7 @@ Authors: Eric Wieser
 -/
 import Mathlib.Algebra.CharP.Pi
 import Mathlib.Algebra.CharP.Quotient
-import Mathlib.Algebra.CharP.Two
-import Mathlib.Algebra.MvPolynomial.CommRing
-import Mathlib.Data.ZMod.Basic
-import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
 import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
-import Mathlib.LinearAlgebra.Finsupp.SumProd
 import Mathlib.RingTheory.MvPolynomial.Basic
 import Mathlib.RingTheory.MvPolynomial.Ideal
 

Counterexamples/HomogeneousPrimeNotPrime.lean

@@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Eric Wieser, Jujian Zhang
 -/
 import Mathlib.Algebra.Divisibility.Prod
+import Mathlib.Data.Fintype.Units
 import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal
-import Mathlib.Data.ZMod.Basic
-import Mathlib.Tactic.DeriveFintype
 
 /-!
 # A homogeneous ideal that is homogeneously prime but not prime

Counterexamples/QuadraticForm.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.LinearAlgebra.QuadraticForm.Basic
-import Mathlib.Algebra.CharP.Two
-import Mathlib.Data.ZMod.Basic
 
 /-!
 # `QuadraticForm R M` and `Subtype LinearMap.IsSymm` are distinct notions in characteristic 2

Mathlib.lean

@@ -3095,21 +3095,18 @@ import Mathlib.Data.ZMod.IntUnitsPower
 import Mathlib.Data.ZMod.QuotientGroup
 import Mathlib.Data.ZMod.QuotientRing
 import Mathlib.Data.ZMod.Units
+import Mathlib.Data.ZMod.ValMinAbs
 import Mathlib.Deprecated.AlgebraClasses
 import Mathlib.Deprecated.Aliases
 import Mathlib.Deprecated.ByteArray
 import Mathlib.Deprecated.Cardinal.Continuum
 import Mathlib.Deprecated.Cardinal.Finite
 import Mathlib.Deprecated.Cardinal.PartENat
-import Mathlib.Deprecated.Combinator
 import Mathlib.Deprecated.Equiv
-import Mathlib.Deprecated.HashMap
-import Mathlib.Deprecated.LazyList
 import Mathlib.Deprecated.Logic
 import Mathlib.Deprecated.MinMax
 import Mathlib.Deprecated.NatLemmas
 import Mathlib.Deprecated.Order
-import Mathlib.Deprecated.RelClasses
 import Mathlib.Dynamics.BirkhoffSum.Average
 import Mathlib.Dynamics.BirkhoffSum.Basic
 import Mathlib.Dynamics.BirkhoffSum.NormedSpace
@@ -3362,6 +3359,7 @@ import Mathlib.GroupTheory.OreLocalization.Cardinality
 import Mathlib.GroupTheory.OreLocalization.OreSet
 import Mathlib.GroupTheory.PGroup
 import Mathlib.GroupTheory.Perm.Basic
+import Mathlib.GroupTheory.Perm.Centralizer
 import Mathlib.GroupTheory.Perm.Closure
 import Mathlib.GroupTheory.Perm.ClosureSwap
 import Mathlib.GroupTheory.Perm.ConjAct
@@ -4634,6 +4632,7 @@ import Mathlib.RingTheory.LocalProperties.Reduced
 import Mathlib.RingTheory.LocalProperties.Submodule
 import Mathlib.RingTheory.LocalRing.Basic
 import Mathlib.RingTheory.LocalRing.Defs
+import Mathlib.RingTheory.LocalRing.LocalSubring
 import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
 import Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs
 import Mathlib.RingTheory.LocalRing.Module
@@ -5559,7 +5558,6 @@ import Mathlib.Topology.OmegaCompletePartialOrder
 import Mathlib.Topology.Order
 import Mathlib.Topology.Order.Basic
 import Mathlib.Topology.Order.Bornology
-import Mathlib.Topology.Order.Bounded
 import Mathlib.Topology.Order.Category.AlexDisc
 import Mathlib.Topology.Order.Category.FrameAdjunction
 import Mathlib.Topology.Order.Compact

Mathlib/Algebra/Algebra/Equiv.lean

@@ -729,21 +729,6 @@ instance _root_.Finite.algEquiv [Finite (A₁ →ₐ[R] A₂)] : Finite (A₁ 
 
 end Semiring
 
-section Ring
-
-variable [CommSemiring R] [Ring A₁] [Ring A₂]
-variable [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂)
-
-@[deprecated map_neg (since := "2024-06-20")]
-protected theorem map_neg (x) : e (-x) = -e x :=
-  map_neg e x
-
-@[deprecated map_sub (since := "2024-06-20")]
-protected theorem map_sub (x y) : e (x - y) = e x - e y :=
-  map_sub e x y
-
-end Ring
-
 end AlgEquiv
 
 namespace MulSemiringAction

Mathlib/Algebra/Algebra/Hom.lean

@@ -194,35 +194,6 @@ theorem commutes (r : R) : φ (algebraMap R A r) = algebraMap R B r :=
 theorem comp_algebraMap : (φ : A →+* B).comp (algebraMap R A) = algebraMap R B :=
   RingHom.ext <| φ.commutes
 
-@[deprecated map_add (since := "2024-06-26")]
-protected theorem map_add (r s : A) : φ (r + s) = φ r + φ s :=
-  map_add _ _ _
-
-@[deprecated map_zero (since := "2024-06-26")]
-protected theorem map_zero : φ 0 = 0 :=
-  map_zero _
-
-@[deprecated map_mul (since := "2024-06-26")]
-protected theorem map_mul (x y) : φ (x * y) = φ x * φ y :=
-  map_mul _ _ _
-
-@[deprecated map_one (since := "2024-06-26")]
-protected theorem map_one : φ 1 = 1 :=
-  map_one _
-
-@[deprecated map_pow (since := "2024-06-26")]
-protected theorem map_pow (x : A) (n : ℕ) : φ (x ^ n) = φ x ^ n :=
-  map_pow _ _ _
-
-@[deprecated map_smul (since := "2024-06-26")]
-protected theorem map_smul (r : R) (x : A) : φ (r • x) = r • φ x :=
-  map_smul _ _ _
-
-@[deprecated map_sum (since := "2024-06-26")]
-protected theorem map_sum {ι : Type*} (f : ι → A) (s : Finset ι) :
-    φ (∑ x ∈ s, f x) = ∑ x ∈ s, φ (f x) :=
-  map_sum _ _ _
-
 /-- If a `RingHom` is `R`-linear, then it is an `AlgHom`. -/
 def mk' (f : A →+* B) (h : ∀ (c : R) (x), f (c • x) = c • f x) : A →ₐ[R] B :=
   { f with
@@ -334,10 +305,6 @@ theorem map_smul_of_tower {R'} [SMul R' A] [SMul R' B] [LinearMap.CompatibleSMul
     (x : A) : φ (r • x) = r • φ x :=
   φ.toLinearMap.map_smul_of_tower r x
 
-@[deprecated map_list_prod (since := "2024-06-26")]
-protected theorem map_list_prod (s : List A) : φ s.prod = (s.map φ).prod :=
-  map_list_prod φ s
-
 @[simps (config := .lemmasOnly) toSemigroup_toMul_mul toOne_one]
 instance End : Monoid (A →ₐ[R] A) where
   mul := comp
@@ -359,22 +326,6 @@ theorem algebraMap_eq_apply (f : A →ₐ[R] B) {y : R} {x : A} (h : algebraMap
   h ▸ (f.commutes _).symm
 
 end Semiring
-
-section Ring
-
-variable [CommSemiring R] [Ring A] [Ring B]
-variable [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B)
-
-@[deprecated map_neg (since := "2024-06-26")]
-protected theorem map_neg (x) : φ (-x) = -φ x :=
-  map_neg _ _
-
-@[deprecated map_sub (since := "2024-06-26")]
-protected theorem map_sub (x y) : φ (x - y) = φ x - φ y :=
-  map_sub _ _ _
-
-end Ring
-
 end AlgHom
 
 namespace RingHom

Mathlib/Algebra/Algebra/Quasispectrum.lean

@@ -3,8 +3,9 @@ Copyright (c) 2024 Jireh Loreaux. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 -/
-import Mathlib.Algebra.Algebra.Unitization
 import Mathlib.Algebra.Algebra.Spectrum
+import Mathlib.Algebra.Algebra.Tower
+import Mathlib.Algebra.Algebra.Unitization
 
 /-!
 # Quasiregularity and quasispectrum

Mathlib/Algebra/Algebra/Rat.lean

@@ -106,9 +106,6 @@ instance instSMulCommClass' [SMulCommClass S R S] : SMulCommClass R ℚ S :=
 
 end DivisionRing
 
-@[deprecated Algebra.id.map_eq_id (since := "2024-07-30")]
-lemma _root_.algebraMap_rat_rat : algebraMap ℚ ℚ = RingHom.id ℚ := rfl
-
 instance algebra_rat_subsingleton {R} [Semiring R] : Subsingleton (Algebra ℚ R) :=
   ⟨fun x y => Algebra.algebra_ext x y <| RingHom.congr_fun <| Subsingleton.elim _ _⟩
 

Mathlib/Algebra/Algebra/Spectrum.lean

@@ -3,7 +3,8 @@ Copyright (c) 2021 Jireh Loreaux. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 -/
-import Mathlib.Algebra.Star.Subalgebra
+import Mathlib.Algebra.Algebra.Subalgebra.Basic
+import Mathlib.Algebra.Star.Pointwise
 import Mathlib.RingTheory.Ideal.Maps
 import Mathlib.RingTheory.Ideal.Nonunits
 import Mathlib.Tactic.NoncommRing
@@ -273,11 +274,6 @@ theorem subset_subalgebra {S R A : Type*} [CommSemiring R] [Ring A] [Algebra R A
     spectrum R (a : A) ⊆ spectrum R a :=
   Set.compl_subset_compl.mpr fun _ ↦ IsUnit.map (SubalgebraClass.val s)
 
-@[deprecated subset_subalgebra (since := "2024-07-19")]
-theorem subset_starSubalgebra [StarRing R] [StarRing A] [StarModule R A] {S : StarSubalgebra R A}
-    (a : S) : spectrum R (a : A) ⊆ spectrum R a :=
-  subset_subalgebra a
-
 theorem singleton_add_eq (a : A) (r : R) : {r} + σ a = σ (↑ₐ r + a) :=
   ext fun x => by
     rw [singleton_add, image_add_left, mem_preimage, add_comm, add_mem_iff, map_neg, neg_neg]

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -175,9 +175,6 @@ protected theorem intCast_mem {R : Type u} {A : Type v} [CommRing R] [Ring A] [A
     (S : Subalgebra R A) (n : ℤ) : (n : A) ∈ S :=
   intCast_mem S n
 
-@[deprecated natCast_mem (since := "2024-04-05")] alias coe_nat_mem := Subalgebra.natCast_mem
-@[deprecated intCast_mem (since := "2024-04-05")] alias coe_int_mem := Subalgebra.intCast_mem
-
 /-- The projection from a subalgebra of `A` to an additive submonoid of `A`. -/
 @[simps coe]
 def toAddSubmonoid {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A]

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -1612,9 +1612,6 @@ theorem toFinset_sum_count_eq (s : Multiset α) : ∑ a ∈ s.toFinset, s.count
   congr with a
   simpa using hms a
 
-@[deprecated sum_count_eq_card (since := "2024-07-21")]
-theorem sum_count_eq [Fintype α] (s : Multiset α) : ∑ a, s.count a = Multiset.card s := by simp
-
 @[simp]
 theorem toFinset_sum_count_nsmul_eq (s : Multiset α) :
     ∑ a ∈ s.toFinset, s.count a • {a} = s := by

Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean

@@ -312,9 +312,6 @@ theorem prod_empty : ∏ x ∈ ∅, f x = 1 :=
 theorem prod_of_isEmpty [IsEmpty α] (s : Finset α) : ∏ i ∈ s, f i = 1 := by
   rw [eq_empty_of_isEmpty s, prod_empty]
 
-@[deprecated (since := "2024-06-11")] alias prod_of_empty := prod_of_isEmpty
-@[deprecated (since := "2024-06-11")] alias sum_of_empty := sum_of_isEmpty
-
 @[to_additive (attr := simp)]
 theorem prod_const_one : (∏ _x ∈ s, (1 : β)) = 1 := by
   simp only [Finset.prod, Multiset.map_const', Multiset.prod_replicate, one_pow]

Mathlib/Algebra/BigOperators/Group/List/Basic.lean

@@ -473,8 +473,6 @@ namespace MonoidHom
 protected theorem map_list_prod (f : M →* N) (l : List M) : f l.prod = (l.map f).prod :=
   map_list_prod f l
 
-attribute [deprecated map_list_sum (since := "2024-05-02")] AddMonoidHom.map_list_sum
-
 end MonoidHom
 
 end MonoidHom

Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean

@@ -147,16 +147,6 @@ lemma drop_take_succ_flatten_eq_getElem (L : List (List α)) (i : Nat) (h : i <
   simp only [this, length_map, take_sum_flatten, drop_sum_flatten,
     drop_take_succ_eq_cons_getElem, h, flatten, append_nil]
 
-@[deprecated (since := "2024-06-11")]
-alias drop_take_succ_join_eq_getElem := drop_take_succ_flatten_eq_getElem
-
-@[deprecated drop_take_succ_flatten_eq_getElem (since := "2024-06-11")]
-lemma drop_take_succ_join_eq_get (L : List (List α)) (i : Fin L.length) :
-    (L.flatten.take ((L.map length).take (i + 1)).sum).drop
-      ((L.map length).take i).sum = get L i := by
-  rw [drop_take_succ_flatten_eq_getElem _ _ i.2]
-  simp
-
 end List
 
 

Mathlib/Algebra/BigOperators/Ring.lean

@@ -266,8 +266,6 @@ theorem prod_range_natCast_sub (n k : ℕ) :
   · rw [← mem_range] at hnk
     rw [prod_eq_zero hnk, prod_eq_zero hnk] <;> simp
 
-@[deprecated (since := "2024-05-27")] alias prod_range_cast_nat_sub := prod_range_natCast_sub
-
 
 end CommRing
 

Mathlib/Algebra/CharP/ExpChar.lean

@@ -68,8 +68,5 @@ theorem frobenius_add : frobenius R p (x + y) = frobenius R p x + frobenius R p
 theorem frobenius_natCast (n : ℕ) : frobenius R p n = n :=
   map_natCast (frobenius R p) n
 
-@[deprecated (since := "2024-04-17")]
-alias frobenius_nat_cast := frobenius_natCast
-
 end CommSemiring
 end frobenius

Mathlib/Algebra/CharZero/Lemmas.lean

@@ -61,15 +61,9 @@ namespace Function
 lemma support_natCast (hn : n ≠ 0) : support (n : α → M) = univ :=
   support_const <| Nat.cast_ne_zero.2 hn
 
-@[deprecated (since := "2024-04-17")]
-alias support_nat_cast := support_natCast
-
 lemma mulSupport_natCast (hn : n ≠ 1) : mulSupport (n : α → M) = univ :=
   mulSupport_const <| Nat.cast_ne_one.2 hn
 
-@[deprecated (since := "2024-04-17")]
-alias mulSupport_nat_cast := mulSupport_natCast
-
 end Function
 end AddMonoidWithOne
 
@@ -108,13 +102,9 @@ variable {R : Type*} [DivisionSemiring R] [NeZero (2 : R)]
 
 @[simp] lemma add_self_div_two (a : R) : (a + a) / 2 = a := by
   rw [← mul_two, mul_div_cancel_right₀ a two_ne_zero]
-@[deprecated (since := "2024-07-16")] alias half_add_self := add_self_div_two
-
 
 @[simp]
 theorem add_halves (a : R) : a / 2 + a / 2 = a := by rw [← add_div, add_self_div_two]
-@[deprecated (since := "2024-07-16")] alias add_halves' := add_halves
-
 end
 section
 

Mathlib/Algebra/DirectSum/Internal.lean

@@ -68,9 +68,6 @@ theorem SetLike.natCast_mem_graded [Zero ι] [AddMonoidWithOne R] [SetLike σ R]
     rw [Nat.cast_succ]
     exact add_mem n_ih (SetLike.one_mem_graded _)
 
-@[deprecated (since := "2024-04-17")]
-alias SetLike.nat_cast_mem_graded := SetLike.natCast_mem_graded
-
 theorem SetLike.intCast_mem_graded [Zero ι] [AddGroupWithOne R] [SetLike σ R]
     [AddSubgroupClass σ R] (A : ι → σ) [SetLike.GradedOne A] (z : ℤ) : (z : R) ∈ A 0 := by
   induction z
@@ -79,9 +76,6 @@ theorem SetLike.intCast_mem_graded [Zero ι] [AddGroupWithOne R] [SetLike σ R]
   · rw [Int.cast_negSucc]
     exact neg_mem (SetLike.natCast_mem_graded _ _)
 
-@[deprecated (since := "2024-04-17")]
-alias SetLike.int_cast_mem_graded := SetLike.intCast_mem_graded
-
 section DirectSum
 
 variable [DecidableEq ι]