chore: remove declarations deprecated between 2025-01-01 and 2025-03-30

Mathlib/Algebra/Category/Grp/Basic.lean

@@ -603,27 +603,3 @@ abbrev AddCommGrpMax.{u1, u2} := AddCommGrp.{max u1 u2}
 /-!
 Deprecated lemmas for `MonoidHom.comp` and categorical identities.
 -/
-
-@[to_additive (attr := deprecated
-  "Proven by `simp only [Grp.hom_id, comp_id]`"
-  (since := "2025-01-28"))]
-theorem MonoidHom.comp_id_grp {G : Grp.{u}} {H : Type u} [Monoid H] (f : G →* H) :
-    f.comp (Grp.Hom.hom (𝟙 G)) = f := by simp
-@[to_additive (attr := deprecated
-  "Proven by `simp only [Grp.hom_id, id_comp]`"
-  (since := "2025-01-28"))]
-theorem MonoidHom.id_grp_comp {G : Type u} [Monoid G] {H : Grp.{u}} (f : G →* H) :
-    MonoidHom.comp (Grp.Hom.hom (𝟙 H)) f = f := by simp
-
-@[to_additive (attr := deprecated
-  "Proven by `simp only [CommGrp.hom_id, comp_id]`"
-  (since := "2025-01-28"))]
-theorem MonoidHom.comp_id_commGrp {G : CommGrp.{u}} {H : Type u} [Monoid H] (f : G →* H) :
-    f.comp (CommGrp.Hom.hom (𝟙 G)) = f := by
-  simp
-@[to_additive (attr := deprecated
-  "Proven by `simp only [CommGrp.hom_id, id_comp]`"
-  (since := "2025-01-28"))]
-theorem MonoidHom.id_commGrp_comp {G : Type u} [Monoid G] {H : CommGrp.{u}} (f : G →* H) :
-    MonoidHom.comp (CommGrp.Hom.hom (𝟙 H)) f = f := by
-  simp

Mathlib/Algebra/Category/ModuleCat/Presheaf/Pullback.lean

@@ -48,9 +48,6 @@ on a certain object `M : PresheafOfModules S`. -/
 abbrev pullbackObjIsDefined : ObjectProperty (PresheafOfModules.{v} S) :=
   (pushforward φ).leftAdjointObjIsDefined
 
-@[deprecated (since := "2025-03-06")]
-alias PullbackObjIsDefined := pullbackObjIsDefined
-
 end
 
 section

Mathlib/Algebra/Category/MonCat/Basic.lean

@@ -504,30 +504,6 @@ example : (forget₂ CommMonCat MonCat).ReflectsIsomorphisms := inferInstance
 `@[simp]` lemmas for `MonoidHom.comp` and categorical identities.
 -/
 
-@[to_additive (attr := deprecated
-  "Proven by `simp only [MonCat.hom_id, comp_id]`"
-  (since := "2025-01-28"))]
-theorem MonoidHom.comp_id_monCat {G : MonCat.{u}} {H : Type u} [Monoid H] (f : G →* H) :
-    f.comp (MonCat.Hom.hom (𝟙 G)) = f := by simp
-@[to_additive (attr := deprecated
-  "Proven by `simp only [MonCat.hom_id, id_comp]`"
-  (since := "2025-01-28"))]
-theorem MonoidHom.id_monCat_comp {G : Type u} [Monoid G] {H : MonCat.{u}} (f : G →* H) :
-    MonoidHom.comp (MonCat.Hom.hom (𝟙 H)) f = f := by simp
-
-@[to_additive (attr := deprecated
-  "Proven by `simp only [CommMonCat.hom_id, comp_id]`"
-  (since := "2025-01-28"))]
-theorem MonoidHom.comp_id_commMonCat {G : CommMonCat.{u}} {H : Type u} [CommMonoid H] (f : G →* H) :
-    f.comp (CommMonCat.Hom.hom (𝟙 G)) = f := by
-  simp
-@[to_additive (attr := deprecated
-  "Proven by `simp only [CommMonCat.hom_id, id_comp]`"
-  (since := "2025-01-28"))]
-theorem MonoidHom.id_commMonCat_comp {G : Type u} [CommMonoid G] {H : CommMonCat.{u}} (f : G →* H) :
-    MonoidHom.comp (CommMonCat.Hom.hom (𝟙 H)) f = f := by
-  simp
-
 /-- The equivalence between `AddMonCat` and `MonCat`. -/
 @[simps]
 def AddMonCat.equivalence : AddMonCat ≌ MonCat where

Mathlib/Algebra/Group/Action/Basic.lean

@@ -115,12 +115,6 @@ theorem smul_bijective {m : α} (hm : IsUnit m) :
   lift m to αˣ using hm
   exact MulAction.bijective m
 
-@[deprecated (since := "2025-03-03")]
-alias _root_.AddAction.vadd_bijective_of_is_addUnit := IsAddUnit.vadd_bijective
-
-@[to_additive existing, deprecated (since := "2025-03-03")]
-alias _root_.MulAction.smul_bijective_of_is_unit := IsUnit.smul_bijective
-
 @[to_additive]
 lemma smul_left_cancel {a : α} (ha : IsUnit a) {x y : β} : a • x = a • y ↔ x = y :=
   let ⟨u, hu⟩ := ha

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

@@ -41,9 +41,6 @@ lemma smul_set_prod {M α : Type*} [SMul M α] [SMul M β] (c : M) (s : Set α)
     c • (s ×ˢ t) = (c • s) ×ˢ (c • t) :=
   prodMap_image_prod (c • ·) (c • ·) s t
 
-@[deprecated (since := "2025-03-11")]
-alias vadd_set_sum := vadd_set_prod
-
 @[to_additive]
 lemma smul_set_pi {G ι : Type*} {α : ι → Type*} [Group G] [∀ i, MulAction G (α i)]
     (c : G) (I : Set ι) (s : ∀ i, Set (α i)) : c • I.pi s = I.pi (c • s) :=

Mathlib/Algebra/Group/Basic.lean

@@ -224,37 +224,25 @@ theorem mul_eq_left : a * b = a ↔ b = 1 := calc
   a * b = a ↔ a * b = a * 1 := by rw [mul_one]
   _ ↔ b = 1 := mul_left_cancel_iff
 
-@[deprecated (since := "2025-03-05")] alias mul_right_eq_self := mul_eq_left
-@[deprecated (since := "2025-03-05")] alias add_right_eq_self := add_eq_left
-
 set_option linter.existingAttributeWarning false in
 attribute [to_additive existing] mul_right_eq_self
 
 @[to_additive (attr := simp)]
 theorem left_eq_mul : a = a * b ↔ b = 1 :=
   eq_comm.trans mul_eq_left
 
-@[deprecated (since := "2025-03-05")] alias self_eq_mul_right := left_eq_mul
-@[deprecated (since := "2025-03-05")] alias self_eq_add_right := left_eq_add
-
 set_option linter.existingAttributeWarning false in
 attribute [to_additive existing] self_eq_mul_right
 
 @[to_additive]
 theorem mul_ne_left : a * b ≠ a ↔ b ≠ 1 := mul_eq_left.not
 
-@[deprecated (since := "2025-03-05")] alias mul_right_ne_self := mul_ne_left
-@[deprecated (since := "2025-03-05")] alias add_right_ne_self := add_ne_left
-
 set_option linter.existingAttributeWarning false in
 attribute [to_additive existing] mul_right_ne_self
 
 @[to_additive]
 theorem left_ne_mul : a ≠ a * b ↔ b ≠ 1 := left_eq_mul.not
 
-@[deprecated (since := "2025-03-05")] alias self_ne_mul_right := left_ne_mul
-@[deprecated (since := "2025-03-05")] alias self_ne_add_right := left_ne_add
-
 set_option linter.existingAttributeWarning false in
 attribute [to_additive existing] self_ne_mul_right
 
@@ -269,37 +257,25 @@ theorem mul_eq_right : a * b = b ↔ a = 1 := calc
   a * b = b ↔ a * b = 1 * b := by rw [one_mul]
   _ ↔ a = 1 := mul_right_cancel_iff
 
-@[deprecated (since := "2025-03-05")] alias mul_left_eq_self := mul_eq_right
-@[deprecated (since := "2025-03-05")] alias add_left_eq_self := add_eq_right
-
 set_option linter.existingAttributeWarning false in
 attribute [to_additive existing] mul_left_eq_self
 
 @[to_additive (attr := simp)]
 theorem right_eq_mul : b = a * b ↔ a = 1 :=
   eq_comm.trans mul_eq_right
 
-@[deprecated (since := "2025-03-05")] alias self_eq_mul_left := right_eq_mul
-@[deprecated (since := "2025-03-05")] alias self_eq_add_left := right_eq_add
-
 set_option linter.existingAttributeWarning false in
 attribute [to_additive existing] self_eq_mul_left
 
 @[to_additive]
 theorem mul_ne_right : a * b ≠ b ↔ a ≠ 1 := mul_eq_right.not
 
-@[deprecated (since := "2025-03-05")] alias mul_left_ne_self := mul_ne_right
-@[deprecated (since := "2025-03-05")] alias add_left_ne_self := add_ne_right
-
 set_option linter.existingAttributeWarning false in
 attribute [to_additive existing] mul_left_ne_self
 
 @[to_additive]
 theorem right_ne_mul : b ≠ a * b ↔ a ≠ 1 := right_eq_mul.not
 
-@[deprecated (since := "2025-03-05")] alias self_ne_mul_left := right_ne_mul
-@[deprecated (since := "2025-03-05")] alias self_ne_add_left := right_ne_add
-
 set_option linter.existingAttributeWarning false in
 attribute [to_additive existing] self_ne_mul_left
 

Mathlib/Algebra/Group/Graph.lean

@@ -56,9 +56,6 @@ lemma mem_mgraph {f : G →* H} {x : G × H} : x ∈ f.mgraph ↔ f x.1 = x.2 :=
 @[to_additive mgraph_eq_mrange_prod]
 lemma mgraph_eq_mrange_prod (f : G →* H) : f.mgraph = mrange ((id _).prod f) := by aesop
 
-@[deprecated (since := "2025-03-11")]
-alias _root_.AddMonoidHom.mgraph_eq_mrange_sum := AddMonoidHom.mgraph_eq_mrange_prod
-
 /-- **Vertical line test** for monoid homomorphisms.
 
 Let `f : G → H × I` be a homomorphism to a product of monoids. Assume that `f` is surjective on the
@@ -171,9 +168,6 @@ lemma mem_graph {f : G →* H} {x : G × H} : x ∈ f.graph ↔ f x.1 = x.2 := .
 @[to_additive graph_eq_range_prod]
 lemma graph_eq_range_prod (f : G →* H) : f.graph = range ((id _).prod f) := by aesop
 
-@[deprecated (since := "2025-03-11")]
-alias AddMonoidHom.graph_eq_range_sum := graph_eq_range_prod
-
 /-- **Vertical line test** for group homomorphisms.
 
 Let `f : G → H × I` be a homomorphism to a product of groups. Assume that `f` is surjective on the

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

@@ -130,9 +130,6 @@ theorem coe_singletonOneHom : (singletonOneHom : α → Set α) = singleton :=
 @[to_additive (attr := simp) zero_prod_zero]
 lemma one_prod_one [One β] : (1 ×ˢ 1 : Set (α × β)) = 1 := by ext; simp [Prod.ext_iff]
 
-@[deprecated (since := "2025-03-11")]
-alias zero_sum_zero := zero_prod_zero
-
 end One
 
 /-! ### Set negation/inversion -/
@@ -187,9 +184,6 @@ theorem compl_inv : sᶜ⁻¹ = s⁻¹ᶜ :=
 @[to_additive (attr := simp) neg_prod]
 lemma inv_prod [Inv β] (s : Set α) (t : Set β) : (s ×ˢ t)⁻¹ = s⁻¹ ×ˢ t⁻¹ := rfl
 
-@[deprecated (since := "2025-03-11")]
-alias neg_sum := neg_prod
-
 end Inv
 
 section InvolutiveInv
@@ -392,9 +386,6 @@ theorem image_op_mul : op '' (s * t) = op '' t * op '' s :=
 lemma prod_mul_prod_comm [Mul β] (s₁ s₂ : Set α) (t₁ t₂ : Set β) :
     (s₁ ×ˢ t₁) * (s₂ ×ˢ t₂) = (s₁ * s₂) ×ˢ (t₁ * t₂) := by ext; simp [mem_mul]; aesop
 
-@[deprecated (since := "2025-03-11")]
-alias sum_add_sum_comm := prod_add_prod_comm
-
 end Mul
 
 /-! ### Set subtraction/division -/

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -126,9 +126,6 @@ theorem top_prod_top : (⊤ : Subgroup G).prod (⊤ : Subgroup N) = ⊤ :=
 theorem bot_prod_bot : (⊥ : Subgroup G).prod (⊥ : Subgroup N) = ⊥ :=
   SetLike.coe_injective <| by simp [coe_prod]
 
-@[deprecated (since := "2025-03-11")]
-alias _root_.AddSubgroup.bot_sum_bot := AddSubgroup.bot_prod_bot
-
 @[to_additive le_prod_iff]
 theorem le_prod_iff {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} :
     J ≤ H.prod K ↔ map (MonoidHom.fst G N) J ≤ H ∧ map (MonoidHom.snd G N) J ≤ K := by
@@ -569,17 +566,11 @@ theorem prodMap_comap_prod {G' : Type*} {N' : Type*} [Group G'] [Group N'] (f :
     (S.prod S').comap (prodMap f g) = (S.comap f).prod (S'.comap g) :=
   SetLike.coe_injective <| Set.preimage_prod_map_prod f g _ _
 
-@[deprecated (since := "2025-03-11")]
-alias _root_.AddMonoidHom.sumMap_comap_sum := AddMonoidHom.prodMap_comap_prod
-
 @[to_additive ker_prodMap]
 theorem ker_prodMap {G' : Type*} {N' : Type*} [Group G'] [Group N'] (f : G →* N) (g : G' →* N') :
     (prodMap f g).ker = f.ker.prod g.ker := by
   rw [← comap_bot, ← comap_bot, ← comap_bot, ← prodMap_comap_prod, bot_prod_bot]
 
-@[deprecated (since := "2025-03-11")]
-alias _root_.AddMonoidHom.ker_sumMap := AddMonoidHom.ker_prodMap
-
 @[to_additive (attr := simp)]
 lemma ker_fst : ker (fst G G') = .prod ⊥ ⊤ := SetLike.ext fun _ => (iff_of_eq (and_true _)).symm
 
@@ -618,13 +609,6 @@ theorem comap_normalizer_eq_of_surjective (H : Subgroup G) {f : N →* G}
     (hf : Function.Surjective f) : H.normalizer.comap f = (H.comap f).normalizer :=
   comap_normalizer_eq_of_le_range fun x _ ↦ hf x
 
-@[deprecated (since := "2025-03-13")]
-alias comap_normalizer_eq_of_injective_of_le_range := comap_normalizer_eq_of_le_range
-
-@[deprecated (since := "2025-03-13")]
-alias _root_.AddSubgroup.comap_normalizer_eq_of_injective_of_le_range :=
-  AddSubgroup.comap_normalizer_eq_of_le_range
-
 /-- The image of the normalizer is equal to the normalizer of the image of an isomorphism. -/
 @[to_additive
       /-- The image of the normalizer is equal to the normalizer of the image of an
@@ -816,19 +800,13 @@ instance prod_subgroupOf_prod_normal {H₁ K₁ : Subgroup G} {H₂ K₂ : Subgr
       h₂.conj_mem ⟨(n : G × N).snd, (mem_prod.mp n.2).2⟩ hgHK.2
         ⟨(g : G × N).snd, (mem_prod.mp g.2).2⟩⟩
 
-@[deprecated (since := "2025-03-11")]
-alias _root_.AddSubgroup.sum_addSubgroupOf_sum_normal := AddSubgroup.prod_addSubgroupOf_prod_normal
-
 @[to_additive prod_normal]
 instance prod_normal (H : Subgroup G) (K : Subgroup N) [hH : H.Normal] [hK : K.Normal] :
     (H.prod K).Normal where
   conj_mem n hg g :=
     ⟨hH.conj_mem n.fst (Subgroup.mem_prod.mp hg).1 g.fst,
       hK.conj_mem n.snd (Subgroup.mem_prod.mp hg).2 g.snd⟩
 
-@[deprecated (since := "2025-03-11")]
-alias _root_.AddSubgroup.sum_normal := AddSubgroup.prod_normal
-
 @[to_additive]
 theorem inf_subgroupOf_inf_normal_of_right (A B' B : Subgroup G)
     [hN : (B'.subgroupOf B).Normal] : ((A ⊓ B').subgroupOf (A ⊓ B)).Normal := by

Mathlib/Algebra/Group/Subgroup/Ker.lean

@@ -306,9 +306,6 @@ theorem ker_prod {M N : Type*} [MulOneClass M] [MulOneClass N] (f : G →* M) (g
     (f.prod g).ker = f.ker ⊓ g.ker :=
   SetLike.ext fun _ => Prod.mk_eq_one
 
-@[deprecated (since := "2025-03-11")]
-alias _root_.AddMonoidHom.ker_sum := AddMonoidHom.ker_prod
-
 @[to_additive]
 theorem range_le_ker_iff (f : G →* G') (g : G' →* G'') : f.range ≤ g.ker ↔ g.comp f = 1 :=
   ⟨fun h => ext fun x => h ⟨x, rfl⟩, by rintro h _ ⟨y, rfl⟩; exact DFunLike.congr_fun h y⟩

Mathlib/Algebra/Group/Subgroup/Pointwise.lean

@@ -460,8 +460,6 @@ theorem Normal.conjAct {H : Subgroup G} (hH : H.Normal) (g : ConjAct G) : g •
 theorem Normal.conj_smul_eq_self (g : G) (H : Subgroup G) [h : Normal H] : MulAut.conj g • H = H :=
   h.conjAct g
 
-@[deprecated (since := "2025-03-01")] alias smul_normal := Normal.conj_smul_eq_self
-
 theorem Normal.of_conjugate_fixed {H : Subgroup G} (h : ∀ g : G, (MulAut.conj g) • H = H) :
     H.Normal := by
   constructor

Mathlib/Algebra/MvPolynomial/Basic.lean

@@ -402,9 +402,6 @@ theorem monomial_add_induction_on {motive : MvPolynomial σ R → Prop} (p : MvP
     motive p :=
   Finsupp.induction p (C_0.rec <| C 0) monomial_add
 
-@[deprecated (since := "2025-03-11")]
-alias induction_on''' := monomial_add_induction_on
-
 /--
 Similar to `MvPolynomial.induction_on` but only a yet weaker form of `h_add` is required.
 In particular, this version only requires us to show

Mathlib/Algebra/Order/Group/Abs.lean

@@ -193,9 +193,6 @@ theorem mabs_div_le_of_le_of_le {a b lb ub : G} (hal : lb ≤ a) (hau : a ≤ ub
     (hbu : b ≤ ub) : |a / b|ₘ ≤ ub / lb :=
   mabs_div_le_iff.2 ⟨div_le_div'' hau hbl, div_le_div'' hbu hal⟩
 
-@[deprecated (since := "2025-03-02")]
-alias dist_bdd_within_interval := abs_sub_le_of_le_of_le
-
 @[to_additive]
 theorem eq_of_mabs_div_le_one (h : |a / b|ₘ ≤ 1) : a = b :=
   eq_of_mabs_div_eq_one (le_antisymm h (one_le_mabs (a / b)))

Mathlib/Algebra/Order/Group/Unbundled/Int.lean

@@ -133,8 +133,6 @@ protected theorem sign_eq_ediv_abs' (a : ℤ) : sign a = a / |a| :=
   if az : a = 0 then by simp [az]
   else (Int.ediv_eq_of_eq_mul_left (mt abs_eq_zero.1 az) (sign_mul_abs _).symm).symm
 
-@[deprecated (since := "2025-03-10")] alias sign_eq_ediv_abs := Int.sign_eq_ediv_abs'
-
 protected theorem sign_eq_abs_ediv (a : ℤ) : sign a = |a| / a :=
   if az : a = 0 then by simp [az]
   else (Int.ediv_eq_of_eq_mul_left az (sign_mul_self_eq_abs _).symm).symm

Mathlib/Algebra/Order/Round.lean

@@ -62,9 +62,6 @@ theorem round_add_intCast (x : α) (y : ℤ) : round (x + y) = round x + y := by
   rw [round, round, Int.fract_add_intCast, Int.floor_add_intCast, Int.ceil_add_intCast,
     ← apply_ite₂, ite_self]
 
-@[deprecated (since := "2025-03-23")]
-alias round_add_int := round_add_intCast
-
 @[simp]
 theorem round_add_one (a : α) : round (a + 1) = round a + 1 := by
   rw [← round_add_intCast a 1, cast_one]
@@ -75,9 +72,6 @@ theorem round_sub_intCast (x : α) (y : ℤ) : round (x - y) = round x - y := by
   norm_cast
   rw [round_add_intCast, sub_eq_add_neg]
 
-@[deprecated (since := "2025-03-23")]
-alias round_sub_int := round_sub_intCast
-
 @[simp]
 theorem round_sub_one (a : α) : round (a - 1) = round a - 1 := by
   rw [← round_sub_intCast a 1, cast_one]
@@ -86,9 +80,6 @@ theorem round_sub_one (a : α) : round (a - 1) = round a - 1 := by
 theorem round_add_natCast (x : α) (y : ℕ) : round (x + y) = round x + y :=
   mod_cast round_add_intCast x y
 
-@[deprecated (since := "2025-03-23")]
-alias round_add_nat := round_add_natCast
-
 @[simp]
 theorem round_add_ofNat (x : α) (n : ℕ) [n.AtLeastTwo] :
     round (x + ofNat(n)) = round x + ofNat(n) :=
@@ -98,9 +89,6 @@ theorem round_add_ofNat (x : α) (n : ℕ) [n.AtLeastTwo] :
 theorem round_sub_natCast (x : α) (y : ℕ) : round (x - y) = round x - y :=
   mod_cast round_sub_intCast x y
 
-@[deprecated (since := "2025-03-23")]
-alias round_sub_nat := round_sub_natCast
-
 @[simp]
 theorem round_sub_ofNat (x : α) (n : ℕ) [n.AtLeastTwo] :
     round (x - ofNat(n)) = round x - ofNat(n) :=
@@ -110,16 +98,10 @@ theorem round_sub_ofNat (x : α) (n : ℕ) [n.AtLeastTwo] :
 theorem round_intCast_add (x : α) (y : ℤ) : round ((y : α) + x) = y + round x := by
   rw [add_comm, round_add_intCast, add_comm]
 
-@[deprecated (since := "2025-03-23")]
-alias round_int_add := round_intCast_add
-
 @[simp]
 theorem round_natCast_add (x : α) (y : ℕ) : round ((y : α) + x) = y + round x := by
   rw [add_comm, round_add_natCast, add_comm]
 
-@[deprecated (since := "2025-03-23")]
-alias round_nat_add := round_natCast_add
-
 @[simp]
 theorem round_ofNat_add (n : ℕ) [n.AtLeastTwo] (x : α) :
     round (ofNat(n) + x) = ofNat(n) + round x :=

Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Basic.lean

@@ -246,12 +246,6 @@ lemma equation_iff_nonsingular [Nontrivial R] [W.IsElliptic] {x y : R} :
     W.toAffine.Equation x y ↔ W.toAffine.Nonsingular x y :=
   W.toAffine.equation_iff_nonsingular_of_Δ_ne_zero <| W.coe_Δ' ▸ W.Δ'.ne_zero
 
-@[deprecated (since := "2025-03-01")] alias nonsingular_zero_of_Δ_ne_zero :=
-  equation_iff_nonsingular_of_Δ_ne_zero
-@[deprecated (since := "2025-03-01")] alias nonsingular_of_Δ_ne_zero :=
-  equation_iff_nonsingular_of_Δ_ne_zero
-@[deprecated (since := "2025-03-01")] alias nonsingular := equation_iff_nonsingular
-
 /-! ## Maps and base changes -/
 
 variable (f : R →+* S) (x y : R)