chore: delete deprecated declarations to the end of 2025 (leanprover-community#41178)

The automated commits were made by running
```
#clear_deprecations "2025-11-01" "2025-12-31" really
```
(I had to do this in multiple sessions because VS Code kept running out of memory.)

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: Parcly-Taxel

Mathlib.lean

@@ -953,7 +953,6 @@ public import Mathlib.Algebra.Order.CompleteField
 public import Mathlib.Algebra.Order.Disjointed
 public import Mathlib.Algebra.Order.Field.Basic
 public import Mathlib.Algebra.Order.Field.Canonical
-public import Mathlib.Algebra.Order.Field.Defs
 public import Mathlib.Algebra.Order.Field.GeomSum
 public import Mathlib.Algebra.Order.Field.Pi
 public import Mathlib.Algebra.Order.Field.Pointwise

Mathlib/Algebra/Algebra/Basic.lean

@@ -117,16 +117,6 @@ theorem algebraMap_ofSubring {R : Type*} [CommRing R] (S : Subring R) :
     (algebraMap S R : S →+* R) = S.subtype :=
   rfl
 
-@[deprecated coe_algebraMap_ofSubsemiring (since := "2025-11-23")]
-theorem coe_algebraMap_ofSubring {R : Type*} [CommRing R] (S : Subring R) :
-    (algebraMap S R : S → R) = Subtype.val :=
-  rfl
-
-@[deprecated algebraMap_ofSubsemiring_apply (since := "2025-11-23")]
-theorem algebraMap_ofSubring_apply {R : Type*} [CommRing R] (S : Subring R) (x : S) :
-    algebraMap S R x = x :=
-  rfl
-
 end SubsemiringAlgebra
 
 /-- Explicit characterization of the submonoid map in the case of an algebra.

Mathlib/Algebra/Algebra/Bilinear.lean

@@ -162,9 +162,6 @@ theorem _root_.Algebra.lmul_isUnit_iff {x : A} :
 theorem toSpanSingleton_one_eq_algebraLinearMap :
     toSpanSingleton R A 1 = Algebra.linearMap R A := by ext; simp
 
-@[deprecated (since := "2025-12-30")] alias toSpanSingleton_eq_algebra_linearMap :=
-  toSpanSingleton_one_eq_algebraLinearMap
-
 variable (R A) in
 /-- The multiplication map on an `R`-algebra, as an `A`-linear map from `A ⊗[R] A` to `A`. -/
 @[simps!] def mul'' : A ⊗[R] A →ₗ[A] A where

Mathlib/Algebra/Algebra/Defs.lean

@@ -396,14 +396,6 @@ variable {R A}
 @[simp] lemma algebraMap_self : algebraMap R R = .id _ := rfl
 lemma algebraMap_self_apply (x : R) : algebraMap R R x = x := rfl
 
-namespace id
-
-@[deprecated _root_.smul_eq_mul (since := "2025-12-02")]
-theorem smul_eq_mul (x y : R) : x • y = x * y :=
-  rfl
-
-end id
-
 end Semiring
 
 end Algebra

Mathlib/Algebra/Algebra/Equiv.lean

@@ -902,8 +902,6 @@ endomorphisms. -/
   __ := e.conjRingEquiv
   commutes' _ := by ext; change e.restrictScalars R _ = _; simp
 
-@[deprecated (since := "2025-12-06")] alias algConj := conjAlgEquiv
-
 theorem conjAlgEquiv_apply (e : M₁ ≃ₗ[S] M₂) (f : Module.End S M₁) :
     e.conjAlgEquiv R f = e.toLinearMap ∘ₗ f ∘ₗ e.symm.toLinearMap := rfl
 

Mathlib/Algebra/BigOperators/Finsupp/Basic.lean

@@ -306,10 +306,6 @@ theorem support_finsetSum [DecidableEq β] [AddCommMonoid M] {s : Finset α} {f
 
 @[deprecated (since := "2026-04-08")] alias support_finset_sum := support_finsetSum
 
-@[deprecated sum_fun_zero (since := "2025-12-19")]
-theorem sum_zero [Zero M] [AddCommMonoid N] {f : α →₀ M} : (f.sum fun _ _ => (0 : N)) = 0 :=
-  Finset.sum_const_zero
-
 theorem sum_eq_one_iff (d : α →₀ ℕ) : sum d (fun _ n ↦ n) = 1 ↔ ∃ a, d = single a 1 := by
   classical
   refine ⟨fun h1 ↦ ?_, ?_⟩

Mathlib/Algebra/Category/FGModuleCat/Basic.lean

@@ -85,9 +85,6 @@ variable (R : Type u) [Ring R]
 
 @[simp] lemma hom_hom_id (A : FGModuleCat.{v} R) : (𝟙 A : A ⟶ A).hom.hom = LinearMap.id := rfl
 
-@[deprecated (since := "2025-12-18")] alias hom_comp := hom_hom_comp
-@[deprecated (since := "2025-12-18")] alias hom_id := hom_hom_id
-
 instance : Inhabited (FGModuleCat.{v} R) :=
   ⟨⟨ModuleCat.of R PUnit, by unfold ModuleCat.isFG; infer_instance⟩⟩
 

Mathlib/Algebra/Category/Ring/FinitePresentation.lean

@@ -161,28 +161,18 @@ lemma CommRingCat.preservesColimit_coyoneda_of_finitePresentation
       f₁.right (Under.w f₁) f₂.right (Under.w f₂) congr($(e).right)
     exact ⟨k, hik, hjk, Under.UnderMorphism.ext e⟩
 
-@[deprecated (since := "2025-12-19")]
-alias preservesColimit_coyoneda_of_finitePresentation :=
-  CommRingCat.preservesColimit_coyoneda_of_finitePresentation
-
 /-- If `S` is a finitely presented `R`-algebra, then `Hom_R(S, -)` preserves filtered colimits. -/
 lemma CommRingCat.preservesFilteredColimits_coyoneda (S : Under R)
     (hS : S.hom.hom.FinitePresentation) :
     PreservesFilteredColimits (coyoneda.obj (.op S)) :=
   ⟨fun _ _ _ ↦ ⟨preservesColimit_coyoneda_of_finitePresentation R S hS _⟩⟩
 
-@[deprecated (since := "2025-12-19")]
-alias preservesFilteredColimits_coyoneda := CommRingCat.preservesFilteredColimits_coyoneda
-
 /-- If `S` is a finitely presented `R`-algebra, `S : Under R` is finitely presentable. -/
 lemma CommRingCat.isFinitelyPresentable_under (S : Under R) (hS : S.hom.hom.FinitePresentation) :
     IsFinitelyPresentable.{u} S := by
   rw [isFinitelyPresentable_iff_preservesFilteredColimits]
   exact preservesFilteredColimits_coyoneda R S hS
 
-@[deprecated (since := "2025-12-19")]
-alias isFinitelyPresentable := CommRingCat.isFinitelyPresentable_under
-
 variable {R} in
 lemma CommRingCat.isFinitelyPresentable_hom {S : CommRingCat.{u}} (f : R ⟶ S)
     (hf : f.hom.FinitePresentation) :

Mathlib/Algebra/DirectSum/Module.lean

@@ -577,43 +577,29 @@ def congrAddEquiv (u : (i : ι) → N i ≃+ P i) :
   left_inv x := by aesop
   right_inv y := by aesop
 
-@[deprecated (since := "2025-12-01")] alias congr_addEquiv := congrAddEquiv
-
 theorem coe_congrAddEquiv (u : (i : ι) → N i ≃+ P i) :
     ⇑(congrAddEquiv u).toAddMonoidHom = ⇑(DirectSum.map fun i ↦ (u i).toAddMonoidHom) :=
   rfl
 
-@[deprecated (since := "2025-12-01")] alias coe_congr_addEquiv := coe_congrAddEquiv
-
 /-- Direct sums of isomorphic modules are isomorphic. -/
 def congrLinearEquiv (u : (i : ι) → N i ≃ₗ[R] P i) :
     (⨁ i, N i) ≃ₗ[R] ⨁ i, P i where
   toAddEquiv := congrAddEquiv (fun i ↦ (u i).toAddEquiv)
   map_smul' r x := by
     exact (DirectSum.lmap (fun i ↦ (u i).toLinearMap)).map_smul r x
 
-@[deprecated (since := "2025-12-01")] alias congr_linearEquiv := congrLinearEquiv
-
 theorem coe_congrLinearEquiv (u : (i : ι) → N i ≃ₗ[R] P i) :
     ⇑(congrLinearEquiv u) = ⇑(DirectSum.lmap (fun i ↦ (u i).toLinearMap)) :=
   rfl
 
-@[deprecated (since := "2025-12-01")] alias coe_congr_linearEquiv := coe_congrLinearEquiv
-
 theorem congrLinearEquiv_toAddEquiv (u : (i : ι) → N i ≃ₗ[R] P i) :
     (congrLinearEquiv u).toAddEquiv = congrAddEquiv (fun i ↦ (u i).toAddEquiv) :=
   rfl
 
-@[deprecated (since := "2025-12-01")]
-alias congr_linearEquiv_toAddEquiv := congrLinearEquiv_toAddEquiv
-
 theorem congrLinearEquiv_toLinearMap (u : (i : ι) → N i ≃ₗ[R] P i) :
     (congrLinearEquiv u).toLinearMap = DirectSum.lmap (fun i ↦ (u i).toLinearMap) :=
   rfl
 
-@[deprecated (since := "2025-12-01")]
-alias congr_linearEquiv_toLinearMap := congrLinearEquiv_toLinearMap
-
 end Congr
 
 end DirectSum

Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean

@@ -272,21 +272,11 @@ theorem smul_inter_nonempty_iff {s t : Set α} {x : α} :
   · rintro ⟨a, b, ⟨ha, hb⟩, rfl⟩
     exact ⟨a, mem_inter (mem_smul_set.mpr ⟨b, hb, by simp⟩) ha⟩
 
-@[to_additive (attr := deprecated smul_inter_nonempty_iff (since := "2025-12-10"))]
-theorem smul_inter_ne_empty_iff {s t : Set α} {x : α} :
-    x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x := by
-  rw [← nonempty_iff_ne_empty, smul_inter_nonempty_iff]
-
 @[to_additive]
 theorem smul_inter_nonempty_iff' {s t : Set α} {x : α} :
     (x • s ∩ t).Nonempty ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a / b = x := by
   simp_rw [smul_inter_nonempty_iff, div_eq_mul_inv]
 
-@[to_additive (attr := deprecated smul_inter_nonempty_iff' (since := "2025-12-10"))]
-theorem smul_inter_ne_empty_iff' {s t : Set α} {x : α} :
-    x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a / b = x := by
-  rw [← nonempty_iff_ne_empty, smul_inter_nonempty_iff']
-
 @[to_additive]
 theorem op_smul_inter_nonempty_iff {s t : Set α} {x : αᵐᵒᵖ} :
     (x • s ∩ t).Nonempty ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = MulOpposite.unop x := by
@@ -298,11 +288,6 @@ theorem op_smul_inter_nonempty_iff {s t : Set α} {x : αᵐᵒᵖ} :
     have : MulOpposite.op (a⁻¹ * b) = x := congr_arg MulOpposite.op H
     exact ⟨b, mem_inter (mem_smul_set.mpr ⟨a, ha, by simp [← this]⟩) hb⟩
 
-@[to_additive (attr := deprecated op_smul_inter_nonempty_iff (since := "2025-12-10"))]
-theorem op_smul_inter_ne_empty_iff {s t : Set α} {x : αᵐᵒᵖ} :
-    x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = MulOpposite.unop x := by
-  rw [← nonempty_iff_ne_empty, op_smul_inter_nonempty_iff]
-
 @[to_additive (attr := simp)]
 theorem iUnion_inv_smul : ⋃ g : α, g⁻¹ • s = ⋃ g : α, g • s :=
   (Function.Surjective.iSup_congr _ inv_surjective) fun _ ↦ rfl