fix: add missing deprecations (leanprover-community#34087)

Ruben-VandeVelde · Ruben-VandeVelde · commit 7048ffa529b9 · 2026-01-18T15:55:04.000Z
From leanprover-community#33633, leanprover-community#30563, leanprover-community#33771, leanprover-community#33755, leanprover-community#31988, leanprover-community#33622, leanprover-community#32837, leanprover-community#33638, leanprover-community#33503, leanprover-community#33321, leanprover-community#33242, leanprover-community#32955, leanprover-community#33159, leanprover-community#33152, leanprover-community#33131, leanprover-community#33144, leanprover-community#32116, leanprover-community#31259, leanprover-community#26831, leanprover-community#32917, leanprover-community#32589, leanprover-community#32584, leanprover-community#32562, leanprover-community#32788, and leanprover-community#32568.
diff --git a/Mathlib/Algebra/BigOperators/Finprod.lean b/Mathlib/Algebra/BigOperators/Finprod.lean
@@ -545,6 +545,8 @@ theorem one_lt_finprod_cond {M : Type*} [CommMonoid M] [PartialOrder M] [IsOrder
     · aesop
   · simp +contextual
 
+@[deprecated (since := "2026-01-06")] alias finprod_cond_pos := finsum_cond_pos
+
 @[to_additive finsum_pos]
 theorem one_lt_finprod {M : Type*} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M]
     {f : ι → M}
diff --git a/Mathlib/Algebra/Group/Irreducible/Indecomposable.lean b/Mathlib/Algebra/Group/Irreducible/Indecomposable.lean
@@ -111,6 +111,10 @@ lemma Submonoid.closure_image_isMulIndecomposable_baseOf [Finite ι]
   replace hjk : v i ∈ closure (v '' t) := hjk ▸ mul_mem hj' hk'
   exact hi₁ hjk
 
+@[deprecated (since := "2025-12-30")]
+alias Submonoid.closure_image_one_lt_and_isMulIndecomposable :=
+  Submonoid.closure_image_isMulIndecomposable_baseOf
+
 @[to_additive]
 lemma Subgroup.closure_image_isMulIndecomposable_baseOf [Finite ι] [InvolutiveInv ι]
     [CommGroup S] [IsOrderedMonoid S]
diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean
@@ -401,6 +401,9 @@ noncomputable def derivativeFinsupp : R[X] →ₗ[R] ℕ →₀ R[X] where
   map_add' _ _ := by ext; simp
   map_smul' _ _ := by ext; simp
 
+@[deprecated (since := "2025-12-15")]
+alias derivativeFinsupp_apply_toFun := derivativeFinsupp_apply_apply
+
 @[simp]
 theorem support_derivativeFinsupp_subset_range {p : R[X]} {n : ℕ} (h : p.natDegree < n) :
     (derivativeFinsupp p).support ⊆ range n := by
diff --git a/Mathlib/Algebra/Polynomial/Roots.lean b/Mathlib/Algebra/Polynomial/Roots.lean
@@ -307,6 +307,8 @@ theorem roots_eq_of_degree_eq_card {S : Finset R}
     (hS : ∀ x ∈ S, p.eval x = 0) (hcard : S.card = p.degree) : p.roots = S.val :=
   roots_eq_of_degree_le_card_of_ne_zero hS (by lia) (by contrapose! hcard; simp [hcard])
 
+@[deprecated (since := "2025-12-16")] alias roots_eq_of_degree_le_card := roots_eq_of_degree_eq_card
+
 theorem roots_eq_of_natDegree_le_card_of_ne_zero {S : Finset R}
     (hS : ∀ x ∈ S, p.eval x = 0) (hcard : p.natDegree ≤ S.card) (hp : p ≠ 0) : p.roots = S.val :=
   roots_eq_of_degree_le_card_of_ne_zero hS (degree_le_of_natDegree_le hcard) hp
diff --git a/Mathlib/Analysis/Calculus/ImplicitContDiff.lean b/Mathlib/Analysis/Calculus/ImplicitContDiff.lean
@@ -70,6 +70,12 @@ namespace IsContDiffImplicitAt
 variable
   {n : WithTop ℕ∞} {f : E × F → G} {f' : E × F →L[𝕜] G} {a : E × F}
 
+omit [CompleteSpace E] [CompleteSpace F] [CompleteSpace G] in
+@[deprecated IsContDiffImplicitAt.ne_zero (since := "2025-12-22")]
+theorem one_le (h : IsContDiffImplicitAt n f f' a) : 1 ≤ n := by
+  rw [ENat.one_le_iff_ne_zero_withTop]
+  exact h.ne_zero
+
 /-- We record the parameters of our specific case in order to apply the general implicit function
 theorem. -/
 def implicitFunctionData (h : IsContDiffImplicitAt n f f' a) :
@@ -105,10 +111,20 @@ lemma implicitFunctionData_pt (h : IsContDiffImplicitAt n f f' a) :
 lemma implicitFunctionData_leftFun_apply {h : IsContDiffImplicitAt n f f' a} {xy : E × F} :
     h.implicitFunctionData.leftFun xy = xy.1 := rfl
 
+@[deprecated "use simp" (since := "2026-01-08")]
+lemma implicitFunctionData_leftFun_pt (h : IsContDiffImplicitAt n f f' a) :
+    h.implicitFunctionData.leftFun h.implicitFunctionData.pt = a.1 := by
+  simp
+
 @[simp]
 lemma implicitFunctionData_rightFun_apply {h : IsContDiffImplicitAt n f f' a} {xy : E × F} :
     h.implicitFunctionData.rightFun xy = f xy := rfl
 
+@[deprecated "use simp" (since := "2026-01-08")]
+lemma implicitFunctionData_rightFun_pt (h : IsContDiffImplicitAt n f f' a) :
+    h.implicitFunctionData.rightFun h.implicitFunctionData.pt = f a := by
+  simp
+
 /-- The implicit function provided by the general theorem, from which we construct the more useful
 form `IsContDiffImplicitAt.implicitFunction`. -/
 noncomputable def implicitFunctionAux (h : IsContDiffImplicitAt n f f' a) : E → G → E × F :=
diff --git a/Mathlib/Analysis/Distribution/TemperedDistribution.lean b/Mathlib/Analysis/Distribution/TemperedDistribution.lean
@@ -413,6 +413,9 @@ theorem fourier_toTemperedDistributionCLM_eq (f : 𝓢(E, F)) :
   ext g
   simpa using integral_fourier_smul_eq g f
 
+@[deprecated (since := "2026-01-14")]
+alias fourierTransform_toTemperedDistributionCLM_eq := fourier_toTemperedDistributionCLM_eq
+
 /-- The distributional inverse Fourier transform and the classical inverse Fourier transform
 coincide on `𝓢(E, F)`. -/
 theorem fourierInv_toTemperedDistributionCLM_eq (f : 𝓢(E, F)) :
@@ -423,6 +426,9 @@ theorem fourierInv_toTemperedDistributionCLM_eq (f : 𝓢(E, F)) :
     rw [fourier_toTemperedDistributionCLM_eq]
   _ = _ := fourierInv_fourier_eq _
 
+@[deprecated (since := "2026-01-14")]
+alias fourierTransformInv_toTemperedDistributionCLM_eq := fourierInv_toTemperedDistributionCLM_eq
+
 end Fourier
 
 section DiracDelta
diff --git a/Mathlib/Analysis/Fourier/LpSpace.lean b/Mathlib/Analysis/Fourier/LpSpace.lean
@@ -103,6 +103,9 @@ theorem SchwartzMap.toLp_fourier_eq (f : 𝓢(E, F)) : 𝓕 (f.toLp 2) = (𝓕 f
   rw [one_mul]
   exact (norm_fourier_toL2_eq f).le
 
+@[deprecated (since := "2025-12-31")]
+alias SchwartzMap.toLp_fourierTransform_eq := SchwartzMap.toLp_fourier_eq
+
 @[simp]
 theorem SchwartzMap.toLp_fourierInv_eq (f : 𝓢(E, F)) : 𝓕⁻ (f.toLp 2) = (𝓕⁻ f).toLp 2 := by
   apply LinearMap.extendOfNorm_eq
@@ -113,6 +116,9 @@ theorem SchwartzMap.toLp_fourierInv_eq (f : 𝓢(E, F)) : 𝓕⁻ (f.toLp 2) = (
   convert (norm_fourier_toL2_eq (𝓕⁻ f)).symm.le
   simp
 
+@[deprecated (since := "2025-12-31")]
+alias SchwartzMap.toLp_fourierTransformInv_eq := SchwartzMap.toLp_fourierInv_eq
+
 namespace MeasureTheory.Lp
 
 /-- The `𝓢'`-Fourier transform and the `L2`-Fourier transform coincide on `L2`. -/
diff --git a/Mathlib/Analysis/Fourier/Notation.lean b/Mathlib/Analysis/Fourier/Notation.lean
@@ -138,6 +138,11 @@ def fourierₗ : E →ₗ[R] F where
 @[simp]
 lemma fourierₗ_apply (f : E) : fourierₗ R E f = 𝓕 f := rfl
 
+include R in
+variable (R) in
+lemma fourier_zero : 𝓕 (0 : E) = 0 :=
+  (fourierₗ R E).map_zero
+
 variable [TopologicalSpace E] [TopologicalSpace F] [ContinuousFourier E F]
 
 variable (R E) in
@@ -165,6 +170,11 @@ def fourierInvₗ : E →ₗ[R] F where
 @[simp]
 lemma fourierInvₗ_apply (f : E) : fourierInvₗ R E f = 𝓕⁻ f := rfl
 
+include R in
+variable (R) in
+lemma fourierInv_zero : 𝓕⁻ (0 : E) = 0 :=
+  (fourierInvₗ R E).map_zero
+
 variable [TopologicalSpace E] [TopologicalSpace F] [ContinuousFourierInv E F]
 
 variable (R E) in
diff --git a/Mathlib/Analysis/Meromorphic/Basic.lean b/Mathlib/Analysis/Meromorphic/Basic.lean
@@ -330,6 +330,11 @@ protected theorem deriv [CompleteSpace E] {f : 𝕜 → E} {x : 𝕜} (h : Merom
     MeromorphicAt.meromorphicAt_congr this]
   fun_prop
 
+@[deprecated MeromorphicAt.deriv (since := "2025-12-21")]
+theorem fun_deriv [CompleteSpace E] {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicAt f x) :
+    MeromorphicAt (fun z ↦ _root_.deriv f z) x :=
+  h.deriv
+
 /--
 Iterated derivatives of meromorphic functions are meromorphic.
 -/
@@ -340,6 +345,12 @@ Iterated derivatives of meromorphic functions are meromorphic.
   | zero => exact h
   | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv
 
+@[deprecated MeromorphicAt.iterated_deriv (since := "2025-12-21")]
+theorem fun_iterated_deriv [CompleteSpace E] {n : ℕ} {f : 𝕜 → E} {x : 𝕜}
+    (h : MeromorphicAt f x) :
+    MeromorphicAt (fun z ↦ _root_.deriv^[n] f z) x :=
+  h.iterated_deriv
+
 end MeromorphicAt
 
 section smul_iff
@@ -522,11 +533,21 @@ include hf in
 /-- Derivatives of meromorphic functions are meromorphic. -/
 protected theorem deriv [CompleteSpace E] : MeromorphicOn (deriv f) U := fun z hz ↦ (hf z hz).deriv
 
+include hf in
+@[deprecated MeromorphicOn.deriv (since := "2025-12-21")]
+theorem fun_deriv [CompleteSpace E] : MeromorphicOn (fun z ↦ _root_.deriv f z) U := hf.deriv
+
 include hf in
 /-- Iterated derivatives of meromorphic functions are meromorphic. -/
 theorem iterated_deriv [CompleteSpace E] {n : ℕ} : MeromorphicOn (_root_.deriv^[n] f) U :=
   fun z hz ↦ (hf z hz).iterated_deriv
 
+include hf in
+@[deprecated MeromorphicOn.iterated_deriv (since := "2025-12-21")]
+theorem fun_iterated_deriv [CompleteSpace E] {n : ℕ} :
+    MeromorphicOn (fun z ↦ _root_.deriv^[n] f z) U :=
+  hf.iterated_deriv
+
 end arithmetic
 
 include hf in
@@ -636,6 +657,8 @@ theorem countable_compl_analyticAt [SecondCountableTopology 𝕜] [CompleteSpace
 
 @[deprecated (since := "2025-12-21")] alias MeromorphicOn.countable_compl_analyticAt :=
   countable_compl_analyticAt
+@[deprecated (since := "2025-12-21")] alias _root_.MeromorphicOn.countable_compl_analyticAt :=
+  countable_compl_analyticAt
 
 /--
 Meromorphic functions are measurable.
@@ -652,5 +675,6 @@ theorem measurable [MeasurableSpace 𝕜] [SecondCountableTopology 𝕜] [BorelS
     (by simp [-mem_compl_iff]) h₃.restrict.measurable (measurable_of_countable _)
 
 @[deprecated (since := "2025-12-21")] alias MeromorphicOn.measurable := measurable
+@[deprecated (since := "2025-12-21")] alias _root_.MeromorphicOn.measurable := measurable
 
 end Meromorphic
diff --git a/Mathlib/Analysis/Normed/Lp/ProdLp.lean b/Mathlib/Analysis/Normed/Lp/ProdLp.lean
@@ -1199,6 +1199,8 @@ def withLpProdCongr (f : α ≃ₗᵢ[𝕜] α') (g : β ≃ₗᵢ[𝕜] β') :
   __ := (f.toLinearEquiv.prodCongr g.toLinearEquiv).withLpCongr p
   norm_map' := (f.toLinearIsometry.withLpProdMap p g.toLinearIsometry).norm_map
 
+@[deprecated (since := "2025-12-22")] alias _root_.LinearIsometry.withLpProdCongr := withLpProdCongr
+
 /-- Commutativity of the `L^p` product as a linear isometric equivalence. -/
 def withLpProdComm : WithLp p (α × β) ≃ₗᵢ[𝕜] WithLp p (β × α) where
   __ := (LinearEquiv.prodComm 𝕜 α β).withLpCongr p
diff --git a/Mathlib/Combinatorics/SimpleGraph/Metric.lean b/Mathlib/Combinatorics/SimpleGraph/Metric.lean
@@ -288,6 +288,11 @@ theorem Adj.diff_dist_adj (hadj : G.Adj v w) :
   have : G.dist u v ≤ G.dist u w + G.dist w v := huw.dist_triangle_left v
   lia
 
+@[deprecated Adj.diff_dist_adj (since := "2025-12-11"), nolint unusedArguments]
+theorem Connected.diff_dist_adj (_ : G.Connected) (hadj : G.Adj v w) :
+    G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1 := by
+  apply Adj.diff_dist_adj hadj
+
 theorem Walk.isPath_of_length_eq_dist (p : G.Walk u v) (hp : p.length = G.dist u v) :
     p.IsPath := by
   classical
diff --git a/Mathlib/Combinatorics/SimpleGraph/VertexCover.lean b/Mathlib/Combinatorics/SimpleGraph/VertexCover.lean
@@ -190,6 +190,11 @@ theorem IsContained.vertexCoverNum_le_vertexCoverNum (h : G ⊑ H) :
   grw [this.vertexCoverNum_le, ← hs₁]
   exact Function.Embedding.encard_le <| Function.Embedding.mk f hf |>.subtypeMap (by simp)
 
+@[deprecated IsContained.vertexCoverNum_le_vertexCoverNum (since := "2026-01-07")]
+theorem vertexCoverNum_le_vertexCoverNum_of_injective (f : G →g H) (hf : Function.Injective f) :
+    vertexCoverNum G ≤ vertexCoverNum H :=
+  IsContained.vertexCoverNum_le_vertexCoverNum ⟨f, hf⟩
+
 @[gcongr]
 theorem vertexCoverNum_mono (h : G ≤ G') : vertexCoverNum G ≤ vertexCoverNum G' :=
   (IsContained.of_le h).vertexCoverNum_le_vertexCoverNum
diff --git a/Mathlib/Data/Finsupp/Basic.lean b/Mathlib/Data/Finsupp/Basic.lean
@@ -1121,6 +1121,9 @@ theorem subtypeDomain_not_piecewise (f : Subtype P →₀ M) (g : {a // ¬ P a}
 @[simps! (attr := grind =) support apply]
 def extendDomain (f : Subtype P →₀ M) : α →₀ M := piecewise f 0
 
+@[deprecated (since := "2025-12-15")]
+alias extendDomain_toFun := extendDomain_apply
+
 theorem extendDomain_eq_embDomain_subtype (f : Subtype P →₀ M) :
     extendDomain f = embDomain (.subtype _) f := by
   ext a
diff --git a/Mathlib/Data/Finsupp/Interval.lean b/Mathlib/Data/Finsupp/Interval.lean
@@ -67,6 +67,9 @@ def rangeIcc (f g : ι →₀ α) : ι →₀ Finset α where
     rw [mem_union, ← not_iff_not, not_or, notMem_support_iff, notMem_support_iff, not_ne_iff]
     exact Icc_eq_singleton_iff.symm
 
+@[deprecated (since := "2025-12-15")]
+alias rangeIcc_toFun := rangeIcc_apply
+
 lemma coe_rangeIcc (f g : ι →₀ α) : rangeIcc f g i = Icc (f i) (g i) := rfl
 
 @[simp]
diff --git a/Mathlib/Data/Rel/Cover.lean b/Mathlib/Data/Rel/Cover.lean
@@ -80,4 +80,6 @@ lemma IsCover.of_maximal_isSeparated [U.IsRefl] [U.IsSymm]
 
 @[simp] lemma isCover_id : IsCover .id s N ↔ s ⊆ N := by simp [IsCover, subset_def]
 
+@[deprecated (since := "2025-12-19")] alias isCover_relId := isCover_id
+
 end SetRel
diff --git a/Mathlib/Geometry/Euclidean/Angle/Unoriented/TriangleInequality.lean b/Mathlib/Geometry/Euclidean/Angle/Unoriented/TriangleInequality.lean
@@ -38,6 +38,8 @@ lemma inner_ortho_nonneg {x y : V} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : 0 ≤
     inner_self_eq_one_of_norm_eq_one hx, real_inner_smul_right, real_inner_comm, sub_nonneg]
   grw [← sq, sq_le_one_iff_abs_le_one, abs_real_inner_le_norm, hx, hy, one_mul]
 
+@[deprecated (since := "2025-12-20")] alias inner_ortho_nonneg_of_norm_eq_one := inner_ortho_nonneg
+
 lemma inner_normalize_ortho (x y : V) : ⟪y, normalize (ortho y x)⟫ = 0 := by
   simp only [NormedSpace.normalize, real_inner_smul_right, mul_eq_zero, inv_eq_zero, norm_eq_zero]
   right; rw [ortho, real_inner_comm, Submodule.starProjection_inner_eq_zero]
diff --git a/Mathlib/Geometry/Manifold/Immersion.lean b/Mathlib/Geometry/Manifold/Immersion.lean
@@ -409,6 +409,8 @@ lemma of_opens [IsManifold I n M] (s : TopologicalSpace.Opens M) (y : s) :
     simp_all
   · exact I.right_inv (by simp_all)
 
+@[deprecated (since := "2025-12-16")] alias ofOpen := of_opens
+
 end IsImmersionAtOfComplement
 
 namespace IsImmersionAt
@@ -580,6 +582,8 @@ lemma of_opens [IsManifold I n M] (s : TopologicalSpace.Opens M) (hx : x ∈ s)
   use PUnit, by infer_instance, by infer_instance
   apply Manifold.IsImmersionAtOfComplement.of_opens
 
+@[deprecated (since := "2025-12-16")] alias ofOpen := of_opens
+
 end IsImmersionAt
 
 variable (F I J n) in
@@ -673,6 +677,8 @@ lemma of_opens [IsManifold I n M] (s : TopologicalSpace.Opens M) :
     IsImmersionOfComplement PUnit I I n (Subtype.val : s → M) :=
   fun y ↦ IsImmersionAtOfComplement.of_opens s y
 
+@[deprecated (since := "2025-12-16")] alias ofOpen := of_opens
+
 end IsImmersionOfComplement
 
 namespace IsImmersion
@@ -730,6 +736,8 @@ lemma of_opens [IsManifold I n M] (s : TopologicalSpace.Opens M) :
     IsImmersion I I n (Subtype.val : s → M) :=
   ⟨PUnit, by infer_instance, by infer_instance, IsImmersionOfComplement.of_opens s⟩
 
+@[deprecated (since := "2025-12-16")] alias ofOpen := of_opens
+
 end IsImmersion
 
 end Manifold
diff --git a/Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean b/Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean
@@ -743,3 +743,16 @@ theorem isPreprimitive_of_three_le_card (h : 3 ≤ Nat.card α) :
   { isTrivialBlock_of_isBlock := isTrivialBlock_of_isBlock α }
 
 end alternatingGroup
+
+namespace AlternatingGroup
+
+@[deprecated (since := "2025-12-16")]
+alias isMultiplyPretransitive := alternatingGroup.isMultiplyPretransitive
+@[deprecated (since := "2025-12-16")]
+alias isPretransitive_of_three_le_card := alternatingGroup.isPretransitive_of_three_le_card
+@[deprecated (since := "2025-12-16")]
+alias isTrivialBlock_of_isBlock := alternatingGroup.isTrivialBlock_of_isBlock
+@[deprecated (since := "2025-12-16")]
+alias isPreprimitive_of_three_le_card := alternatingGroup.isPreprimitive_of_three_le_card
+
+end AlternatingGroup
diff --git a/Mathlib/GroupTheory/Perm/MaximalSubgroups.lean b/Mathlib/GroupTheory/Perm/MaximalSubgroups.lean
@@ -130,6 +130,8 @@ theorem exists_mem_stabilizer_smul_eq :
   classical
   exact ⟨swap a b, swap_mem_stabilizer ha hb, swap_apply_left a b⟩
 
+@[deprecated (since := "2025-12-16")] alias moves_in := exists_mem_stabilizer_smul_eq
+
 theorem stabilizer.surjective_toPerm (s : Set α) :
     Function.Surjective (toPerm : stabilizer (Perm α) s → Perm s) := fun g ↦ by
   classical
@@ -252,6 +254,10 @@ lemma subsingleton_of_ssubset_of_stabilizer_le
   rw [isPreprimitive_congr hG hf]
   infer_instance
 
+@[deprecated (since := "2025-12-16")]
+alias _root_.IsBlock.subsingleton_of_ssubset_compl_of_stabilizer_le :=
+  subsingleton_of_ssubset_of_stabilizer_le
+
 lemma subsingleton_of_ssubset_of_stabilizer_Perm_le
     {B : Set α} {G : Subgroup (Perm α)} (hB : IsBlock G B)
     (hB_ss_sc : B ⊂ s) (hG : stabilizer (Perm α) s ≤ G) :
@@ -328,6 +334,10 @@ lemma compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl
     rw [← is_one_pretransitive_iff]
     apply ofFixingSubgroup.isMultiplyPretransitive M s rfl
 
+@[deprecated (since := "2025-12-16")]
+alias _root_.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl :=
+  compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl
+
 end MulAction.IsBlock
 
 namespace Equiv.Perm
@@ -393,7 +403,8 @@ theorem isCoatom_stabilizer_of_ncard_lt_ncard_compl
     hB.subsingleton_of_stabilizer_lt_of_subset hB_not_le_sc hG hBs
   -- Step 4 : `sᶜ ⊆ B`
   have _ := isMultiplyPretransitive α (s.ncard + 1)
-  apply IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl hG.le <;> grind
+  apply MulAction.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl hG.le <;>
+    grind
 
 /-- `MulAction.stabilizer (Perm α) s` is a maximal subgroup of `Perm α`,
 provided `s` and `sᶜ` are nonempty, and `Nat.card α ≠ 2 * Nat.card s`.
diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean
@@ -60,6 +60,8 @@ variable {r : α → α → Prop}
 
 theorem Std.Refl.reflexive [Std.Refl r] : Reflexive r := fun x ↦ Std.Refl.refl x
 
+@[deprecated (since := "2026-01-09")] alias IsRefl.reflexive := Std.Refl.reflexive
+
 /-- To show a reflexive relation `r : α → α → Prop` holds over `x y : α`,
 it suffices to show it holds when `x ≠ y`. -/
 theorem Reflexive.rel_of_ne_imp (h : Reflexive r) {x y : α} (hr : x ≠ y → r x y) : r x y := by
diff --git a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean
@@ -166,6 +166,11 @@ lemma linear_isTheta_right_add (c e : ℤ) (z : ℂ) :
   simpa [-Int.cofinite_eq] using
     .inr <| tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding Int.isClosedEmbedding_coe_real
 
+@[deprecated linear_isTheta_right_add (since := "2025-12-27")]
+lemma linear_isTheta_right (c : ℤ) (z : ℂ) :
+    (fun (d : ℤ) ↦ (c * z + d)) =Θ[cofinite] fun n ↦ (n : ℝ) := by
+  simpa using linear_isTheta_right_add c 0 z
+
 lemma linear_isTheta_left (d : ℤ) {z : ℂ} (hz : z ≠ 0) :
     (fun (c : ℤ) ↦ (c * z + d)) =Θ[cofinite] fun n ↦ (n : ℝ) := by
   apply IsTheta.add_isLittleO
diff --git a/Mathlib/Order/Defs/Unbundled.lean b/Mathlib/Order/Defs/Unbundled.lean
@@ -343,11 +343,13 @@ theorem comm_of (r : α → α → Prop) [Std.Symm r] {a b : α} : r a b ↔ r b
 protected theorem Std.Asymm.antisymm (r : α → α → Prop) [Std.Asymm r] : Std.Antisymm r :=
   inferInstance
 
+@[deprecated (since := "2026-01-05")] protected alias IsAsymm.isAntisymm := Std.Asymm.antisymm
 @[deprecated (since := "2026-01-06")] protected alias Std.Asymm.isAntisymm := Std.Asymm.antisymm
 
 protected theorem Std.Asymm.irrefl [Std.Asymm r] : Std.Irrefl r :=
   inferInstance
 
+@[deprecated (since := "2026-01-05")] protected alias IsAsymm.isIrrefl := Std.Asymm.irrefl
 @[deprecated (since := "2026-01-07")] protected alias Std.Asymm.isIrrefl := Std.Asymm.irrefl
 
 protected theorem IsTotal.isTrichotomous (r) [IsTotal α r] : IsTrichotomous α r :=
diff --git a/Mathlib/Order/RelClasses.lean b/Mathlib/Order/RelClasses.lean
diff --git a/Mathlib/Probability/Process/Adapted.lean b/Mathlib/Probability/Process/Adapted.lean
diff --git a/Mathlib/RingTheory/AlgebraTower.lean b/Mathlib/RingTheory/AlgebraTower.lean
diff --git a/Mathlib/RingTheory/Filtration.lean b/Mathlib/RingTheory/Filtration.lean
diff --git a/Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean b/Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
diff --git a/Mathlib/RingTheory/Smooth/NoetherianDescent.lean b/Mathlib/RingTheory/Smooth/NoetherianDescent.lean
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/ConditionalInt.lean b/Mathlib/Topology/Algebra/InfiniteSum/ConditionalInt.lean
