[Merged by Bors] - chore: remove declarations deprecated between 2021-04-15 and 2025-10-15

Mathlib/Algebra/Category/Grp/CartesianMonoidal.lean

@@ -121,9 +121,6 @@ noncomputable def cartesianMonoidalCategory : CartesianMonoidalCategory AddCommG
 
 -- This is deprecated, but still used as a `local instance` in
 -- Mathlib.Algebra.Category.Grp.LeftExactFunctor
-@[instance_reducible, deprecated (since := "2025-10-10")]
-alias cartesianMonoidalCategoryAddCommGrp := cartesianMonoidalCategory
-
 attribute [local instance] cartesianMonoidalCategory
 
 noncomputable instance : BraidedCategory AddCommGrpCat.{u} := .ofCartesianMonoidalCategory

Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean

@@ -45,8 +45,7 @@ namespace leftExactFunctorForgetEquivalence
 
 attribute [local instance] hasFiniteProducts_of_hasFiniteBiproducts
 
--- This was deprecated on 2025-10-10 but is still used as a local instance here!
-attribute [local instance] AddCommGrpCat.cartesianMonoidalCategoryAddCommGrp
+attribute [local instance] AddCommGrpCat.cartesianMonoidalCategory
 
 set_option backward.privateInPublic true in
 private noncomputable local instance : CartesianMonoidalCategory C := .ofHasFiniteProducts

Mathlib/Algebra/Group/Subgroup/Finite.lean

@@ -174,12 +174,6 @@ open Set
 
 variable {η : Type*} {f : η → Type*} [∀ i, Group (f i)]
 
-@[to_additive (attr := deprecated Submonoid.pi_mem_of_mulSingle_mem_aux (since := "2025-10-08"))]
-theorem pi_mem_of_mulSingle_mem_aux [DecidableEq η] (I : Finset η) {H : Subgroup (∀ i, f i)}
-    (x : ∀ i, f i) (h1 : ∀ i, i ∉ I → x i = 1) (h2 : ∀ i, i ∈ I → Pi.mulSingle i (x i) ∈ H) :
-    x ∈ H :=
-  Submonoid.pi_mem_of_mulSingle_mem_aux I x h1 h2
-
 @[to_additive]
 theorem pi_mem_of_mulSingle_mem [Finite η] [DecidableEq η] {H : Subgroup (∀ i, f i)} (x : ∀ i, f i)
     (h : ∀ i, Pi.mulSingle i (x i) ∈ H) : x ∈ H :=

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -250,8 +250,6 @@ instance (priority := 900) isReduced_of_noZeroDivisors [NoZeroDivisors M₀] :
 
 variable [IsReduced M₀]
 
-@[deprecated (since := "2025-10-14")] alias pow_eq_zero := eq_zero_of_pow_eq_zero
-
 @[simp] lemma pow_eq_zero_iff (hn : n ≠ 0) : a ^ n = 0 ↔ a = 0 :=
   ⟨eq_zero_of_pow_eq_zero, (·.symm ▸ zero_pow hn)⟩
 

Mathlib/Algebra/Lie/Basic.lean

@@ -362,16 +362,6 @@ instance : LinearMapClass (L₁ →ₗ⁅R⁆ L₂) R L₁ L₂ where
   map_add _ _ _ := by rw [← coe_toLinearMap, map_add]
   map_smulₛₗ _ _ _ := by rw [← coe_toLinearMap, map_smulₛₗ]
 
-@[deprecated (since := "2025-10-12")] alias map_smul := _root_.map_smul
-
-@[deprecated (since := "2025-10-12")] alias map_add := _root_.map_add
-
-@[deprecated (since := "2025-10-12")] alias map_sub := _root_.map_sub
-
-@[deprecated (since := "2025-10-12")] alias map_neg := _root_.map_neg
-
-@[deprecated (since := "2025-10-12")] alias map_zero := _root_.map_zero
-
 @[simp]
 theorem map_lie (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) : f ⁅x, y⁆ = ⁅f x, f y⁆ :=
   LieHom.map_lie' f
@@ -708,16 +698,6 @@ instance : LinearMapClass (M →ₗ⁅R,L⁆ N) R M N where
   map_add _ _ _ := by rw [← coe_toLinearMap, map_add]
   map_smulₛₗ _ _ _ := by rw [← coe_toLinearMap, map_smulₛₗ]
 
-@[deprecated (since := "2025-10-12")] alias map_smul := _root_.map_smul
-
-@[deprecated (since := "2025-10-12")] alias map_add := _root_.map_add
-
-@[deprecated (since := "2025-10-12")] alias map_sub := _root_.map_sub
-
-@[deprecated (since := "2025-10-12")] alias map_neg := _root_.map_neg
-
-@[deprecated (since := "2025-10-12")] alias map_zero := _root_.map_zero
-
 @[simp]
 theorem map_lie (f : M →ₗ⁅R,L⁆ N) (x : L) (m : M) : f ⁅x, m⁆ = ⁅x, f m⁆ :=
   LieModuleHom.map_lie' f

Mathlib/Algebra/Order/Group/Defs.lean

@@ -70,12 +70,6 @@ section LinearOrderedCommGroup
 
 variable [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] {a : α}
 
-@[deprecated (since := "2025-10-06")]
-alias LinearOrderedCommGroup.mul_lt_mul_left' := mul_lt_mul_right
-
-@[deprecated (since := "2025-10-06")]
-alias LinearOrderedCommGroup.mul_lt_mul_right' := mul_lt_mul_left
-
 @[to_additive eq_zero_of_neg_eq]
 theorem eq_one_of_inv_eq' (h : a⁻¹ = a) : a = 1 :=
   match lt_trichotomy a 1 with

Mathlib/Algebra/Polynomial/Splits.lean

@@ -894,12 +894,6 @@ alias nextCoeff_eq_neg_sum_roots_mul_leadingCoeff_of_splits :=
 @[deprecated (since := "2025-12-12")]
 alias nextCoeff_eq_neg_sum_roots_of_monic_of_splits := Splits.nextCoeff_eq_neg_sum_roots_of_monic
 
-@[deprecated (since := "2025-10-08")]
-alias prod_roots_eq_coeff_zero_of_monic_of_splits := coeff_zero_eq_prod_roots_of_monic_of_splits
-
-@[deprecated (since := "2025-10-08")]
-alias sum_roots_eq_nextCoeff_of_monic_of_split := nextCoeff_eq_neg_sum_roots_of_monic_of_splits
-
 end Splits
 
 end

Mathlib/Algebra/Ring/Invertible.lean

@@ -42,9 +42,6 @@ variable {x y}
 theorem AddUnits.neg_mulLeft : -(x.mulLeft y) = (-x).mulLeft y := rfl
 theorem AddUnits.neg_mulRight : -(x.mulRight y) = (-x).mulRight y := rfl
 
-@[deprecated (since := "2025-10-03")] alias AddUnits.neg_mul_left := AddUnits.neg_mulLeft
-@[deprecated (since := "2025-10-03")] alias AddUnits.neg_mul_right := AddUnits.neg_mulRight
-
 theorem AddUnits.neg_mul_eq_mul_neg {x y : AddUnits R} : (↑(-x) * y : R) = x * ↑(-y) := by
   rw [← neg_eq_val_neg, ← val_neg_mulRight]
   apply AddUnits.neg_eq_of_add_eq_zero_left

Mathlib/Algebra/Star/SelfAdjoint.lean

@@ -211,11 +211,6 @@ lemma _root_.IsUnit.isSelfAdjoint_conjugate_iff' {a u : R} (hu : IsUnit u) :
     IsSelfAdjoint (star u * a * u) ↔ IsSelfAdjoint a := by
   simpa using hu.star.isSelfAdjoint_conjugate_iff
 
-@[deprecated (since := "2025-09-28")] alias _root_.isSelfAdjoint_conjugate_iff_of_isUnit :=
-  IsUnit.isSelfAdjoint_conjugate_iff
-@[deprecated (since := "2025-09-28")] alias _root_.isSelfAdjoint_conjugate_iff_of_isUnit' :=
-  IsUnit.isSelfAdjoint_conjugate_iff'
-
 end Monoid
 
 section Semiring

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -302,8 +302,6 @@ theorem Scheme.isBasis_affineOpens (X : Scheme) : Opens.IsBasis X.affineOpens :=
   rcases hS with ⟨i, rfl⟩
   exact isAffineOpen_opensRange _
 
-@[deprecated (since := "2025-10-07")] alias isBasis_affine_open := Scheme.isBasis_affineOpens
-
 theorem iSup_affineOpens_eq_top (X : Scheme) : ⨆ i : X.affineOpens, (i : X.Opens) = ⊤ := by
   apply Opens.ext
   rw [Opens.coe_iSup]
@@ -338,12 +336,6 @@ lemma Scheme.Opens.toSpecΓ_SpecMap_presheaf_map {X : Scheme} (U V : X.Opens) (h
   delta Scheme.Opens.toSpecΓ
   simp [← Spec.map_comp, ← X.presheaf.map_comp, toSpecΓ_naturality_assoc]
 
-@[deprecated (since := "2025-10-07")]
-alias Scheme.Opens.toSpecΓ_SpecMap_map := Scheme.Opens.toSpecΓ_SpecMap_presheaf_map
-
-@[deprecated (since := "2025-10-07")]
-alias Scheme.Opens.toSpecΓ_SpecMap_map_assoc := Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc
-
 set_option backward.isDefEq.respectTransparency false in
 @[reassoc] -- not simp because simp can prove this.
 lemma Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top {X : Scheme} (U : X.Opens) :
@@ -407,8 +399,6 @@ lemma isoSpec_hom_apply (x : U) :
   congr 1
   exact IsLocalRing.comap_closedPoint (U.stalkIso x).inv.hom
 
-@[deprecated (since := "2025-10-07")] alias isoSpec_hom_base_apply := isoSpec_hom_apply
-
 lemma isoSpec_hom_appTop :
     hU.isoSpec.hom.appTop = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv := by
   simp [isoSpec, Scheme.isoSpec]
@@ -483,10 +473,6 @@ lemma SpecMap_appLE_fromSpec (f : X ⟶ Y) {V : X.Opens} {U : Y.Opens}
     Scheme.homOfLE_appTop, Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_map,
     Scheme.Hom.appLE_map, Scheme.Hom.appLE_map, Scheme.Hom.map_appLE]
 
-@[deprecated (since := "2025-10-07")] alias Spec_map_appLE_fromSpec := SpecMap_appLE_fromSpec
-@[deprecated (since := "2025-10-07")]
-alias Spec_map_appLE_fromSpec_assoc := SpecMap_appLE_fromSpec_assoc
-
 lemma fromSpec_top [IsAffine X] : (isAffineOpen_top X).fromSpec = X.isoSpec.inv := by
   rw [fromSpec, Iso.inv_comp_eq]
   simp [isoSpec_hom]
@@ -935,9 +921,6 @@ theorem iSup_basicOpen_eq_self_iff {s : Set Γ(X, U)} :
       PrimeSpectrum.zeroLocus_empty_iff_eq_top, PrimeSpectrum.zeroLocus_span]
     simp only [Set.iUnion_singleton_eq_range, Subtype.range_val_subtype, Set.setOf_mem_eq]
 
-@[deprecated (since := "2025-10-07")]
-alias basicOpen_union_eq_self_iff := iSup_basicOpen_eq_self_iff
-
 include hU in
 theorem self_le_iSup_basicOpen_iff {s : Set Γ(X, U)} :
     (U ≤ ⨆ f : s, X.basicOpen f.1) ↔ Ideal.span s = ⊤ := by
@@ -947,9 +930,6 @@ theorem self_le_iSup_basicOpen_iff {s : Set Γ(X, U)} :
   intro x _
   exact X.basicOpen_le x
 
-@[deprecated (since := "2025-10-07")]
-alias self_le_basicOpen_union_iff := self_le_iSup_basicOpen_iff
-
 end IsAffineOpen
 
 set_option backward.isDefEq.respectTransparency false in

Mathlib/AlgebraicGeometry/AffineSpace.lean

@@ -307,8 +307,6 @@ lemma map_SpecMap {R S : CommRingCat.{max u v}} (φ : R ⟶ S) :
     rw [SpecIso_inv_appTop_coord, ← CommRingCat.comp_apply, ← Scheme.ΓSpecIso_inv_naturality,
         CommRingCat.comp_apply, ConcreteCategory.hom_ofHom, map_X]
 
-@[deprecated (since := "2025-10-07")] alias map_Spec_map := map_SpecMap
-
 /-- The map between affine spaces over affine bases is
 isomorphic to the natural map between polynomial rings. -/
 def mapSpecMap {R S : CommRingCat.{max u v}} (φ : R ⟶ S) :

Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean

@@ -171,9 +171,6 @@ nonrec def Cover.add {X Y : Scheme.{u}} (𝒰 : X.Cover (precoverage P)) (f : Y
     refine ⟨fun x ↦ ⟨some <| 𝒰.idx x, 𝒰.covers x⟩, ?_⟩
     rintro (i | i) <;> simp [hf, 𝒰.map_prop]
 
-@[deprecated (since := "2025-10-02")]
-alias Cover.pullbackCover := Precoverage.ZeroHypercover.pullback₁
-
 /-- The family of morphisms from the pullback cover to the original cover. -/
 def Cover.pullbackHom [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P]
     {X W : Scheme.{u}} (𝒰 : X.Cover (precoverage P)) (f : W ⟶ X) (i) [∀ x, HasPullback f (𝒰.f x)] :
@@ -186,9 +183,6 @@ lemma Cover.pullbackHom_map [P.IsStableUnderBaseChange] [IsJointlySurjectivePres
     [∀ (x : 𝒰.I₀), HasPullback f (𝒰.f x)] (i) :
     𝒰.pullbackHom f i ≫ 𝒰.f i = (𝒰.pullback₁ f).f i ≫ f := pullback.condition.symm
 
-@[deprecated (since := "2025-10-02")]
-alias Cover.pullbackCover' := Precoverage.ZeroHypercover.pullback₂
-
 /--
 An affine cover of `X` consists of a jointly surjective family of maps into `X` from
 spectra of rings.

Mathlib/AlgebraicGeometry/Gluing.lean

@@ -403,13 +403,9 @@ theorem isOpenMap_fromGlued : IsOpenMap 𝒰.fromGlued := by
     exact Set.preimage_image_eq _ 𝒰.fromGlued_injective
   · exact ⟨hx, 𝒰.covers x⟩
 
-@[deprecated (since := "2025-10-07")] alias fromGlued_open_map := isOpenMap_fromGlued
-
 theorem isOpenEmbedding_fromGlued : IsOpenEmbedding 𝒰.fromGlued :=
   .of_continuous_injective_isOpenMap (by fun_prop) 𝒰.fromGlued_injective 𝒰.isOpenMap_fromGlued
 
-@[deprecated (since := "2025-10-07")] alias fromGlued_isOpenEmbedding := isOpenEmbedding_fromGlued
-
 instance : Epi 𝒰.fromGlued.base := by
   rw [TopCat.epi_iff_surjective]
   intro x

Mathlib/AlgebraicGeometry/Morphisms/Affine.lean

@@ -52,8 +52,6 @@ lemma IsAffineOpen.preimage {X Y : Scheme} {U : Y.Opens} (hU : IsAffineOpen U)
     IsAffineOpen (f ⁻¹ᵁ U) :=
   IsAffineHom.isAffine_preimage _ hU
 
-@[deprecated (since := "2025-10-07")] alias affinePreimage := IsAffineOpen.preimage
-
 instance (priority := 900) [IsIso f] : IsAffineHom f :=
   ⟨fun _ hU ↦ hU.preimage_of_isIso f⟩
 

Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

@@ -506,8 +506,6 @@ lemma of_isZariskiLocalAtTarget (P : MorphismProperty Scheme.{u})
       exact P.of_zeroHypercover_target Y.affineCover
         fun i ↦ of_targetAffineLocally_of_isPullback (.of_hasPullback _ _) hf
 
-@[deprecated (since := "2025-10-07")] alias of_isLocalAtTarget := of_isZariskiLocalAtTarget
-
 lemma copy {P P'} {Q Q'} [HasAffineProperty P Q]
     (e : P = P') (e' : Q = Q') : HasAffineProperty P' Q' where
   isLocal_affineProperty := e' ▸ isLocal_affineProperty P
@@ -677,80 +675,4 @@ instance (P : MorphismProperty Scheme) [P.IsStableUnderBaseChange] :
     P.HasOfPostcompProperty @IsOpenImmersion :=
   HasOfPostcompProperty.of_le P (.monomorphisms Scheme) (fun _ _ f _ ↦ inferInstanceAs (Mono f))
 
-section Deprecations
-
-@[deprecated (since := "2025-10-07")] alias IsLocalAtTarget := IsZariskiLocalAtTarget
-
-namespace IsLocalAtTarget
-
-@[deprecated (since := "2025-10-07")]
-alias mk' := IsZariskiLocalAtTarget.mk'
-
-@[deprecated (since := "2025-10-07")]
-alias of_iSup_eq_top := IsZariskiLocalAtTarget.of_iSup_eq_top
-
-@[deprecated (since := "2025-10-07")]
-alias iff_of_iSup_eq_top := IsZariskiLocalAtTarget.iff_of_iSup_eq_top
-
-@[deprecated (since := "2025-10-07")]
-alias of_openCover := IsZariskiLocalAtTarget.of_openCover
-
-@[deprecated (since := "2025-10-07")]
-alias iff_of_openCover := IsZariskiLocalAtTarget.iff_of_openCover
-
-@[deprecated (since := "2025-10-07")]
-alias of_isPullback := IsZariskiLocalAtTarget.of_isPullback
-
-@[deprecated (since := "2025-10-07")]
-alias restrict := IsZariskiLocalAtTarget.restrict
-
-@[deprecated (since := "2025-10-07")]
-alias of_range_subset_iSup := IsZariskiLocalAtTarget.of_range_subset_iSup
-
-end IsLocalAtTarget
-
-@[deprecated (since := "2025-10-07")] alias IsLocalAtSource := IsZariskiLocalAtSource
-
-namespace IsLocalAtSource
-
-@[deprecated (since := "2025-10-07")]
-alias mk' := IsZariskiLocalAtSource.mk'
-
-@[deprecated (since := "2025-10-07")]
-alias comp := IsZariskiLocalAtSource.comp
-
-@[deprecated (since := "2025-10-07")]
-alias respectsLeft_isOpenImmersion := IsZariskiLocalAtSource.respectsLeft_isOpenImmersion
-
-@[deprecated (since := "2025-10-07")]
-alias of_iSup_eq_top := IsZariskiLocalAtSource.of_iSup_eq_top
-
-@[deprecated (since := "2025-10-07")]
-alias iff_of_iSup_eq_top := IsZariskiLocalAtSource.iff_of_iSup_eq_top
-
-@[deprecated (since := "2025-10-07")]
-alias of_openCover := IsZariskiLocalAtSource.of_openCover
-
-@[deprecated (since := "2025-10-07")]
-alias iff_of_openCover := IsZariskiLocalAtSource.iff_of_openCover
-
-@[deprecated (since := "2025-10-07")]
-alias of_isOpenImmersion := IsZariskiLocalAtSource.of_isOpenImmersion
-
-@[deprecated (since := "2025-10-07")]
-alias isLocalAtTarget := IsZariskiLocalAtSource.isZariskiLocalAtTarget
-
-@[deprecated (since := "2025-10-07")]
-alias sigmaDesc := IsZariskiLocalAtSource.sigmaDesc
-
-@[deprecated (since := "2025-10-07")]
-alias resLE := IsZariskiLocalAtSource.resLE
-
-@[deprecated (since := "2025-10-07")]
-alias iff_exists_resLE := IsZariskiLocalAtSource.iff_exists_resLE
-
-end IsLocalAtSource
-
-end Deprecations
-
 end AlgebraicGeometry

Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

@@ -146,8 +146,6 @@ instance SpecMap_residue {X : Scheme.{u}} (x) : IsClosedImmersion (Spec.map (X.r
   IsClosedImmersion.spec_of_surjective (X.residue x)
     Ideal.Quotient.mk_surjective
 
-@[deprecated (since := "2025-10-07")] alias Spec_map_residue := SpecMap_residue
-
 instance (priority := low) {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] : IsAffineHom f :=
   isAffineHom_of_isInducing _ f.isClosedEmbedding.isInducing f.isClosedEmbedding.isClosed_range