chore: remove declarations deprecated between 2021-03-24 and 2025-09-24 (leanprover-community#37118)

I am happy to remove some deprecated declarations for you!
Please check if there are any remaining stray comments or other issues before merging.

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: 3 people

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

@@ -1066,10 +1066,6 @@ lemma mem_sum {a : M} {s : Finset ι} {m : ι → Multiset M} :
     a ∈ ∑ i ∈ s, m i ↔ ∃ i ∈ s, a ∈ m i := by
   induction s using Finset.cons_induction with grind
 
-@[deprecated Multiset.mem_sum (since := "2025-08-24")]
-theorem _root_.Finset.mem_sum {f : ι → Multiset M} (s : Finset ι) (b : M) :
-    (b ∈ ∑ x ∈ s, f x) ↔ ∃ a ∈ s, b ∈ f a := Multiset.mem_sum
-
 @[to_additive]
 lemma prod_map_prod {α : Type*} [CommMonoid M] {m : Multiset ι} {s : Finset α} {f : ι → α → M} :
     (m.map fun i ↦ ∏ a ∈ s, f i a).prod = ∏ a ∈ s, (m.map fun i ↦ f i a).prod := by

Mathlib/Algebra/Category/CommAlgCat/Basic.lean

@@ -165,8 +165,6 @@ def algEquivOfIso (i : A ≅ B) : A ≃ₐ[R] B where
   left_inv x := by simp
   right_inv x := by simp
 
-@[deprecated (since := "2025-08-22")] alias ofIso := algEquivOfIso
-
 /-- Algebra equivalences between `Algebra`s are the same as isomorphisms in `CommAlgCat`. -/
 @[simps]
 def isoEquivAlgEquiv : (of R X ≅ of R Y) ≃ (X ≃ₐ[R] Y) where

Mathlib/Algebra/Field/Basic.lean

@@ -33,10 +33,6 @@ variable [DivisionSemiring K] {a b c d : K}
 
 theorem add_div (a b c : K) : (a + b) / c = a / c + b / c := by simp_rw [div_eq_mul_inv, add_mul]
 
-@[deprecated add_div (since := "2025-08-25")]
-theorem div_add_div_same (a b c : K) : a / c + b / c = (a + b) / c :=
-  (add_div _ _ _).symm
-
 theorem same_add_div (h : b ≠ 0) : (b + a) / b = 1 + a / b := by rw [← div_self h, add_div]
 
 theorem div_add_same (h : b ≠ 0) : (a + b) / b = a / b + 1 := by rw [← div_self h, add_div]

Mathlib/Algebra/Group/Action/Faithful.lean

@@ -92,10 +92,6 @@ lemma RightCancelMonoid.faithfulSMul [RightCancelMonoid α] : FaithfulSMul α α
 lemma LeftCancelMonoid.to_faithfulSMul_mulOpposite [LeftCancelMonoid α] : FaithfulSMul αᵐᵒᵖ α :=
   inferInstance
 
-@[deprecated (since := "2025-09-15")]
-alias LefttCancelMonoid.to_faithfulSMul_mulOpposite := LeftCancelMonoid.to_faithfulSMul_mulOpposite
-
-
 @[to_additive]
 lemma faithfulSMul_iff_injective_smul_one (R A : Type*)
     [MulOneClass A] [SMul R A] [IsScalarTower R A A] :

Mathlib/Algebra/Group/End.lean

@@ -104,14 +104,6 @@ theorem mul_apply (f g : Perm α) (x) : (f * g) x = f (g x) :=
 theorem one_apply (x) : (1 : Perm α) x = x :=
   rfl
 
-@[deprecated symm_apply_apply (since := "2025-08-16")]
-theorem inv_apply_self (f : Perm α) (x) : f⁻¹ (f x) = x :=
-  f.symm_apply_apply x
-
-@[deprecated apply_symm_apply (since := "2025-08-16")]
-theorem apply_inv_self (f : Perm α) (x) : f (f⁻¹ x) = x :=
-  f.apply_symm_apply x
-
 theorem one_def : (1 : Perm α) = Equiv.refl α :=
   rfl
 
@@ -285,8 +277,6 @@ completely in terms of the group structure. -/
 theorem _root_.Equiv.permCongr_eq_mul (e p : Perm α) : e.permCongr p = e * p * e⁻¹ :=
   rfl
 
-@[deprecated (since := "2025-08-29")] alias permCongr_eq_mul := Equiv.permCongr_eq_mul
-
 @[simp]
 lemma _root_.Equiv.permCongr_mul (e : α ≃ β) (p q : Perm α) :
     e.permCongr (p * q) = e.permCongr p * e.permCongr q :=
@@ -299,8 +289,6 @@ def _root_.Equiv.permCongrHom (e : α ≃ β) : Perm α ≃* Perm β where
 attribute [inherit_doc Equiv.permCongr] Equiv.permCongrHom
 extend_docs Equiv.permCongrHom after "This is `Equiv.permCongr` as a `MulEquiv`."
 
-@[deprecated (since := "2025-08-23")] alias permCongrHom := Equiv.permCongrHom
-
 @[simp]
 theorem _root_.Equiv.permCongrHom_symm (e : α ≃ β) :
     e.permCongrHom.symm = e.symm.permCongrHom :=

Mathlib/Algebra/Group/Equiv/TypeTags.lean

@@ -71,16 +71,11 @@ def AddEquiv.toMultiplicativeRight [MulOneClass G] [AddZeroClass H] :
     right_inv := f.right_inv
     map_add' := map_mul f }
 
-@[deprecated (since := "2025-09-19")]
-alias AddEquiv.toMultiplicative' := AddEquiv.toMultiplicativeRight
-
 /-- Reinterpret `G ≃* Multiplicative H` as `Additive G ≃+ H`. -/
 abbrev MulEquiv.toAdditiveLeft [MulOneClass G] [AddZeroClass H] :
     G ≃* Multiplicative H ≃ (Additive G ≃+ H) :=
   AddEquiv.toMultiplicativeRight.symm
 
-@[deprecated (since := "2025-09-19")] alias MulEquiv.toAdditive' := MulEquiv.toAdditiveLeft
-
 /-- Reinterpret `G ≃+ Additive H` as `Multiplicative G ≃* H`. -/
 @[simps]
 def AddEquiv.toMultiplicativeLeft [AddZeroClass G] [MulOneClass H] :
@@ -98,16 +93,11 @@ def AddEquiv.toMultiplicativeLeft [AddZeroClass G] [MulOneClass H] :
     right_inv := f.right_inv
     map_add' := map_mul f }
 
-@[deprecated (since := "2025-09-19")]
-alias AddEquiv.toMultiplicative'' := AddEquiv.toMultiplicativeLeft
-
 /-- Reinterpret `Multiplicative G ≃* H` as `G ≃+ Additive H` as. -/
 abbrev MulEquiv.toAdditiveRight [AddZeroClass G] [MulOneClass H] :
     Multiplicative G ≃* H ≃ (G ≃+ Additive H) :=
   AddEquiv.toMultiplicativeLeft.symm
 
-@[deprecated (since := "2025-09-19")] alias MulEquiv.toAdditive'' := MulEquiv.toAdditiveRight
-
 /-- The multiplicative version of an additivized monoid is mul-equivalent to itself. -/
 @[simps! apply symm_apply]
 def MulEquiv.toMultiplicative_toAdditive [MulOneClass G] :

Mathlib/Algebra/Group/Submonoid/Operations.lean

@@ -1098,9 +1098,6 @@ theorem submonoidMap_symm_apply (e : M ≃* N) (S : Submonoid M) (g : S.map (e :
     (e.submonoidMap S).symm g = ⟨e.symm g, SetLike.mem_coe.1 <| Set.mem_image_equiv.1 g.2⟩ :=
   rfl
 
-@[deprecated (since := "2025-08-20")]
-alias _root_.AddEquiv.add_submonoid_map_symm_apply := AddEquiv.addSubmonoidMap_symm_apply
-
 end MulEquiv
 
 @[to_additive (attr := simp)]

Mathlib/Algebra/Group/TypeTags/Hom.lean

@@ -81,31 +81,20 @@ def AddMonoidHom.toMultiplicativeRight [MulOneClass α] [AddZeroClass β] :
     map_zero' := f.map_one
   }
 
-@[deprecated (since := "2025-09-19")]
-alias AddMonoidHom.toMultiplicative' := AddMonoidHom.toMultiplicativeRight
-
 @[simp, norm_cast]
 lemma AddMonoidHom.coe_toMultiplicativeRight [MulOneClass α] [AddZeroClass β]
     (f : Additive α →+ β) : ⇑(toMultiplicativeRight f) = ofAdd ∘ f ∘ ofMul := rfl
 
-@[deprecated (since := "2025-09-19")]
-alias AddMonoidHom.coe_toMultiplicative' := AddMonoidHom.coe_toMultiplicativeRight
-
 /-- Reinterpret `α →* Multiplicative β` as `Additive α →+ β`. -/
 @[simps!]
 def MonoidHom.toAdditiveLeft [MulOneClass α] [AddZeroClass β] :
     (α →* Multiplicative β) ≃ (Additive α →+ β) :=
   AddMonoidHom.toMultiplicativeRight.symm
 
-@[deprecated (since := "2025-09-19")] alias MonoidHom.toAdditive' := MonoidHom.toAdditiveLeft
-
 @[simp, norm_cast]
 lemma MonoidHom.coe_toAdditiveLeft [MulOneClass α] [AddZeroClass β] (f : α →* Multiplicative β) :
     ⇑(toAdditiveLeft f) = toAdd ∘ f ∘ toMul := rfl
 
-@[deprecated (since := "2025-09-19")]
-alias MonoidHom.coe_toAdditive' := MonoidHom.coe_toAdditiveLeft
-
 /-- Reinterpret `α →+ Additive β` as `Multiplicative α →* β`. -/
 @[simps]
 def AddMonoidHom.toMultiplicativeLeft [AddZeroClass α] [MulOneClass β] :
@@ -121,31 +110,20 @@ def AddMonoidHom.toMultiplicativeLeft [AddZeroClass α] [MulOneClass β] :
     map_zero' := f.map_one
   }
 
-@[deprecated (since := "2025-09-19")]
-alias AddMonoidHom.toMultiplicative'' := AddMonoidHom.toMultiplicativeLeft
-
 @[simp, norm_cast]
 lemma AddMonoidHom.coe_toMultiplicativeLeft [AddZeroClass α] [MulOneClass β] (f : α →+ Additive β) :
     ⇑(toMultiplicativeLeft f) = toMul ∘ f ∘ toAdd := rfl
 
-@[deprecated (since := "2025-09-19")]
-alias AddMonoidHom.coe_toMultiplicative'' := AddMonoidHom.coe_toMultiplicativeLeft
-
 /-- Reinterpret `Multiplicative α →* β` as `α →+ Additive β`. -/
 @[simps!]
 def MonoidHom.toAdditiveRight [AddZeroClass α] [MulOneClass β] :
     (Multiplicative α →* β) ≃ (α →+ Additive β) :=
   AddMonoidHom.toMultiplicativeLeft.symm
 
-@[deprecated (since := "2025-09-19")] alias MonoidHom.toAdditive'' := MonoidHom.toAdditiveRight
-
 @[simp, norm_cast]
 lemma MonoidHom.coe_toAdditiveRight [AddZeroClass α] [MulOneClass β] (f : Multiplicative α →* β) :
     ⇑(toAdditiveRight f) = ofMul ∘ f ∘ ofAdd := rfl
 
-@[deprecated (since := "2025-09-19")]
-alias MonoidHom.coe_toAdditive'' := MonoidHom.coe_toAdditiveRight
-
 /-- This ext lemma moves the type tag to the codomain, since most ext lemmas act on the domain.
 
 WARNING: This has the potential to send `ext` into a loop if someone locally adds the inverse ext

Mathlib/Algebra/Group/Units/Defs.lean

@@ -321,10 +321,6 @@ theorem divp_one (a : α) : a /ₚ 1 = a :=
 theorem divp_assoc (a b : α) (u : αˣ) : a * b /ₚ u = a * (b /ₚ u) :=
   mul_assoc _ _ _
 
-@[deprecated divp_assoc (since := "2025-08-25")]
-theorem divp_assoc' (x y : α) (u : αˣ) : x * (y /ₚ u) = x * y /ₚ u :=
-  (divp_assoc _ _ _).symm
-
 @[simp]
 theorem divp_inv (u : αˣ) : a /ₚ u⁻¹ = a * u :=
   rfl

Mathlib/Algebra/Group/WithOne/Basic.lean

@@ -97,61 +97,31 @@ theorem mapMulHom_id : mapMulHom (MulHom.id α) = MonoidHom.id (WithOne α) := b
   ext x
   induction x <;> rfl
 
-@[deprecated (since := "2025-08-26")]
-alias map_id := mapMulHom_id
-@[deprecated (since := "2025-08-26")]
-alias _root_.WithZero.map_id := WithZero.mapAddHom_id
-
 @[to_additive]
 theorem mapMulHom_injective {f : α →ₙ* β} (hf : Function.Injective f) :
     Function.Injective (mapMulHom f)
   | none, none, _ => rfl
   | (a₁ : α), (a₂ : α), H => by simpa [hf.eq_iff] using H
 
-@[deprecated (since := "2025-08-26")]
-alias map_injective := mapMulHom_injective
-@[deprecated (since := "2025-08-26")]
-alias _root_.WithZero.map_injective := WithZero.mapAddHom_injective
-
 @[to_additive]
 theorem mapMulHom_injective' :
     Function.Injective (WithOne.mapMulHom (α := α) (β := β)) :=
   fun f g h ↦ MulHom.ext fun x ↦ coe_injective <| by simp only [← mapMulHom_coe, h]
 
-@[deprecated (since := "2025-08-26")]
-alias map_injective' := mapMulHom_injective'
-@[deprecated (since := "2025-08-26")]
-alias _root_.WithZero.map_injective' := WithZero.mapAddHom_injective'
-
 @[to_additive (attr := simp)]
 theorem mapMulHom_inj {f g : α →ₙ* β} : mapMulHom f = mapMulHom g ↔ f = g :=
   mapMulHom_injective'.eq_iff
 
-@[deprecated (since := "2025-08-26")]
-alias map_inj := mapMulHom_inj
-@[deprecated (since := "2025-08-26")]
-alias _root_.WithZero.map_inj := WithZero.mapAddHom_inj
-
 @[to_additive]
 theorem mapMulHom_mapMulHom (f : α →ₙ* β) (g : β →ₙ* γ) (x) :
     mapMulHom g (mapMulHom f x) = mapMulHom (g.comp f) x := by
   induction x <;> rfl
 
-@[deprecated (since := "2025-08-26")]
-alias map_map := mapMulHom_mapMulHom
-@[deprecated (since := "2025-08-26")]
-alias _root_.WithZero.map_map := WithZero.mapAddHom_mapAddHom
-
 @[to_additive (attr := simp)]
 theorem mapMulHom_comp (f : α →ₙ* β) (g : β →ₙ* γ) :
     mapMulHom (g.comp f) = (mapMulHom g).comp (mapMulHom f) :=
   MonoidHom.ext fun x => (mapMulHom_mapMulHom f g x).symm
 
-@[deprecated (since := "2025-08-26")]
-alias map_comp := mapMulHom_comp
-@[deprecated (since := "2025-08-26")]
-alias _root_.WithZero.map_comp := WithZero.mapAddHom_comp
-
 /-- A version of `Equiv.optionCongr` for `WithOne`. -/
 @[to_additive (attr := simps apply) /-- A version of `Equiv.optionCongr` for `WithZero`. -/]
 def _root_.MulEquiv.withOneCongr (e : α ≃* β) : WithOne α ≃* WithOne β :=