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

[leanprover-community-bot-assistant]

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

workflow run for this PR

[github-actions]

PR summary 213ff10ae9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RMDBeL (new file)	3

---

Declarations diff

- Absorbent.eventually_nhdsWithin_zero
- Absorbs.eventually_nhdsWithin_zero
- AddMonoidHom.graph_eq_range_sum
- AddSubgroup.quotientEquivSumOfLE
- AddSubgroup.quotientEquivSumOfLE'
- AddSubgroup.quotientEquivSumOfLE'_apply
- AddSubgroup.quotientEquivSumOfLE'_symm_apply
- AddSubgroup.quotientEquivSumOfLE_apply
- AddSubgroup.quotientEquivSumOfLE_symm_apply
- AnalyticAt.add'
- AnalyticAt.const_smul'
- AnalyticAt.div'
- AnalyticAt.inv'
- AnalyticAt.mul'
- AnalyticAt.neg'
- AnalyticAt.smul'
- AnalyticAt.sub'
- BoundedSMul
- BoundedSMul.of_nnnorm_smul_le
- BoundedSMul.of_norm_smul_le
- CauchySeq.prod
- CauchySeq.prod_map
- CofilteredClosure
- CompleteLattice.isStronglyAtomic
- CompleteLattice.isStronglyCoatomic
- Component
- Component.ι
- Config.asFn
- Config.lemmasOnly
- ConnectedSpace.infinite
- ContDiff.prod
- ContDiff.prod_map
- ContDiffAt.prod
- ContDiffAt.prod_map
- ContDiffAt.prod_map'
- ContDiffOn.prod
- ContDiffOn.prod_map
- ContDiffWithinAt.prod
- ContDiffWithinAt.prod_map
- ContDiffWithinAt.prod_map'
- ContMDiff.prod_map
- ContMDiff.prod_mk
- ContMDiff.prod_mk_space
- ContMDiffAt.prod_map
- ContMDiffAt.prod_map'
- ContMDiffAt.prod_mk
- ContMDiffAt.prod_mk_space
- ContMDiffOn.prod_map
- ContMDiffOn.prod_mk
- ContMDiffOn.prod_mk_space
- ContMDiffWithinAt.prod_map
- ContMDiffWithinAt.prod_map'
- ContMDiffWithinAt.prod_mk
- ContMDiffWithinAt.prod_mk_space
- Continuous.Prod.mk
- Continuous.Prod.mk_left
- Continuous.matrix_col
- Continuous.matrix_row
- Continuous.prod_mk
- ContinuousAt.prod
- ContinuousOn.prod
- ContinuousOn.prod_map
- ContinuousWithinAt.prod
- ContinuousWithinAt.prod_map
- Differentiable.prod
- DifferentiableAt.fderiv_prod
- DifferentiableAt.prod
- DifferentiableAt.prod_map
- DifferentiableOn.prod
- DifferentiableWithinAt.fderivWithin_prod
- DifferentiableWithinAt.prod
- Equivalence.ofFullSubcategory
- EventuallyEq.prod_map
- EventuallyEq.prod_mk
- EventuallyLE.prod_map
- Filter.Eventually.prod_mk_nhds
- Filter.EventuallyConst.prod_mk
- Filter.Tendsto.atBot_mul
- Filter.Tendsto.atTop_mul
- Filter.Tendsto.mul_atBot
- Filter.Tendsto.mul_atTop
- Filter.Tendsto.prod_mk_nhds
- FilteredClosure
- Fintype.linearIndependent_iff_injective
- FullSubcategory
- FullSubcategory.lift
- FullSubcategory.lift_comp_inclusion
- FullSubcategory.lift_comp_inclusion_eq
- FullSubcategory.lift_comp_map
- FullSubcategory.map
- FullSubcategory.map_inclusion
- HasDerivAt.prod
- HasDerivAt.tendsto_punctured_nhds
- HasDerivAtFilter.prod
- HasDerivWithinAt.prod
- HasFDerivAt.prod
- HasFDerivAtFilter.prod
- HasFDerivWithinAt.prod
- HasFTaylorSeriesUpToOn.prod
- HasProd.prod_mk
- HasStrictDerivAt.prod
- HasStrictFDerivAt.prod
- HasSum.prod_mk
- Integrable.prod_mk
- IntermediateField.finiteDimensional_bot
- IntermediateField.fixingSubgroup.bot
- Ioc_disjoint_Ioc_same
- IsAddFreimanHom.sum
- IsAddFreimanIso.sum
- IsConjExponent.coe
- IsMulFreimanHom.prod
- IsMulFreimanIso.prod
- IsTopologicalAddGroup.continuous_conj_sum
- IsUniformInducing.uniformAddGroup
- IsUniformInducing.uniformGroup
- IsometricSMul
- IsometricVAdd
- LeftAdjointObjIsDefined
- Lex.nil_left_or_eq_nil
- Lex.singleton_iff
- LinearIndependent.linearCombination_injective
- LinearOrderedField.toTopologicalDivisionRing
- MDifferentiable.prod_mk
- MDifferentiable.prod_mk_space
- MDifferentiableAt.prod_mk
- MDifferentiableAt.prod_mk_space
- MDifferentiableOn.prod_mk
- MDifferentiableOn.prod_mk_space
- MDifferentiableWithinAt.prod_mk
- MDifferentiableWithinAt.prod_mk_space
- Measurable.map_prod_mk_left
- Measurable.map_prod_mk_right
- Measurable.prod_map
- Measurable.prod_mk
- MeasurableEmbedding.prod_mk_left
- MeasurableEmbedding.prod_mk_right
- MeasureTheory.AEStronglyMeasurable.prod_mk_left
- MeasureTheory.Measure.integrable_measure_prod_mk_left
- MonObjOfRepresentableBy
- MonObjOfRepresentableBy_yonedaMonObjRepresentableBy
- MonoidHom.comp_id_commGrp
- MonoidHom.comp_id_commMonCat
- MonoidHom.comp_id_grp
- MonoidHom.comp_id_monCat
- MonoidHom.id_commGrp_comp
- MonoidHom.id_commMonCat_comp
- MonoidHom.id_grp_comp
- MonoidHom.id_monCat_comp
- MonoidalCategory.MonoidalPredicate
- NormedDivisionRing.to_topologicalDivisionRing
- Pairwise.insert_of_symmetric_of_notMem
- ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_mk
- ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_mk_prod_mk
- PullbackObjIsDefined
- Real.IsConjExponent.toNNReal
- RespectsIso.is_localization_away_iff
- RingHom.IsLocalization.exists_smul_mem_of_mem_adjoin
- RingHom.IsLocalization.lift_mem_adjoin_finsetIntegerMultiple
- Subgraph.Copy.map
- SymmetricRel
- SymmetricRel.eq
- SymmetricRel.inter
- SymmetricRel.mk_mem_comm
- Tendsto.prod_map
- Tendsto.prod_map_coprod
- Tendsto.prod_mk
- TendstoUniformly.prod
- TendstoUniformly.prod_map
- TendstoUniformlyOn.prod
- TendstoUniformlyOn.prod_map
- TendstoUniformlyOnFilter.prod
- TendstoUniformlyOnFilter.prod_map
- TopologicalDivisionRing
- UniformAddGroup
- UniformCauchySeqOn.prod_map
- UniformContinuous.prod_mk
- UniformContinuous.prod_mk_left
- UniformContinuous.prod_mk_right
- UniformGroup
- UpgradedPolishSpace
- absorbent_iff_eventually_nhdsWithin_zero
- absorbs_iff_eventually_nhdsWithin_zero
- add_left_eq_self
- add_left_ne_self
- add_right_eq_self
- add_right_ne_self
- aestronglyMeasurable_comp_snd_map_prod_mk_iff
- app_hom
- app_inv
- bind_congr''
- card_fintypeIci
- card_fintypeIoi
- card_fintype_Icc
- card_fintype_Ico
- card_fintype_Ioc
- card_fintype_Ioo
- clusterPt_iff
- coe_inf
- coe_sup
- coe_toHom_apply
- coe_toMeasureEquiv
- col_add
- col_cons
- col_empty
- col_eq_zero
- col_inj
- col_injective
- col_mulVec
- col_smul
- col_vecMul
- col_zero
- colynomialOn
- comap_normalizer_eq_of_injective_of_le_range
- complete_polishSpaceMetric
- conjExponent
- conjTranspose_col
- conjTranspose_row
- contDiff_prod_mk_left
- contDiff_prod_mk_right
- continuous_prod_mk
- diag_col_mul_row
- diff_singleton_sSubset
- dist_bdd_within_interval
- dslope_eventuallyEq_slope_punctured_nhds
- dual_Icc
- dual_Ici
- dual_Ico
- dual_Iic
- dual_Iio
- dual_Ioc
- dual_Ioi
- dual_Ioo
- dual_uIcc
- dual_uIoo
- essImageInclusion
- eval_negPolynomial
- exp_cgf_of_neZero
- exp_of_nilpotent_is_unit
- fermatLastTheoremWith'_of_field
- finiteDimensional_sup
- finiteType_is_local
- finite_or_rankInfinite
- finite_setOf_add_order_eq
- fintypeQuotientOfFreeOfNeBot
- fintypeQuotientOfFreeOfRankEq
- foldr_eta
- forall_ge_iff_eq_top
- forall_gt_iff_eq_top
- forall_le_iff_eq_bot
- forall_lt_iff_eq_bot
- forall_ne_iff_eq_bot
- forall_ne_iff_eq_top
- forall_some_ne_iff_eq_none
- frobeniusBoundedSMul
- frobenius_nnnorm_col
- frobenius_nnnorm_row
- frobenius_norm_col
- frobenius_norm_row
- fst_map_prod_mk
- fst_map_prod_mk₀
- fullSubcategoryInclusion
- fullSubcategoryInclusion.map
- fullSubcategoryInclusion.obj
- fullSubcategoryInclusion_map_lift_map
- fullSubcategoryInclusion_obj_lift_obj
- fullyFaithfulFullSubcategoryInclusion
- hasColimitOfIso
- hasFDerivAt_prod_mk_left
- hasFDerivAt_prod_mk_right
- hasFiniteIntegral_prod_mk_left
- hasLimitEquivalenceComp
- hasLimitOfEquivalenceComp
- hasLimitOfIso
- hom.injective
- hom_apply
- iCondIndepFun.condIndepFun_prod_mk
- iCondIndepFun.condIndepFun_prod_mk_prod_mk
- iIndepFun.indepFun_prod_mk
- iIndepFun.indepFun_prod_mk_prod_mk
- induction_on'''
- integrable_comp_snd_map_prod_mk_iff
- integrable_kernel_prod_mk_left
- intersperse_cons_cons
- intersperse_singleton
- inv_sub_one
- isAlgebraic_of_isLocalization
- isConjExopnent_coe
- isConjExponent_coe
- isLittleO_abs_log_rpow_rpow_nhds_zero
- isLittleO_log_rpow_nhds_zero
- is_localization_basicOpen_of_qcqs
- linearDependent_comp_subtype'ₛ
- linearDependent_comp_subtypeₛ
- linearIndependent_comp_subtypeₛ
- linearIndependent_iff_injective_linearCombination
- linearIndependent_subtypeₛ
- linfty_opNNNorm_col
- linfty_opNNNorm_row
- linfty_opNorm_col
- linfty_opNorm_row
- list_get?
- list_get?₁
- mapClusterPt_iff
- mapSpanningSubgraphs
- mapSpanningSubgraphs_inj
- mapSpanningSubgraphs_injective
- map_prod_map_const_id_principal_coprod_principal
- map_prod_map_coprod_le
- measurableEmbedding_prod_mk_left
- measurable_kernel_prod_mk_left
- measurable_kernel_prod_mk_left'
- measurable_kernel_prod_mk_left_of_finite
- measurable_kernel_prod_mk_right
- measurable_measure_prod_mk_left
- measurable_measure_prod_mk_left_finite
- measurable_measure_prod_mk_right
- measurable_prod_mk_left
- measurable_prod_mk_right
- mem_comap_prod_mk
- mk'
- mk.inj_iff
- mk.inj_left
- mk.inj_right
- mk_complex
- mk_inj_left
- mk_inj_right
- mk_univ_complex
- mulKer
- mulVec_col_eq_const
- mul_ker_mk_eq
- mul_left_eq_self
- mul_left_ne_self
- mul_right_eq_self
- mul_right_ne_self
- negAt_apply_abs_isReal
- neg_nonpos_iff_nonneg
- neg_sum
- nhdsWithin_compl_coe_neBot
- nhdsWithin_compl_infty_eq
- nhdsWithin_compl_infty_neBot
- nhdsWithin_compl_neBot
- nhdsWithin_compl_singleton_sup_pure
- nhds_basis_zero_abs_sub_lt
- nhds_mk
- nnnorm_col
- nnnorm_row
- noZeroDivisors_of_le_nonZeroDivisors
- nonempty_of_infiniteDimensionalType
- nonsingular
- nonsingular_of_Δ_ne_zero
- nonsingular_zero_of_Δ_ne_zero
- norm_col
- norm_row
- nsmul_right_inj
- nsmul_right_injective
- ofBoxProdLeft_boxProdRight
- ofEq
- one_toNNReal
- one_toReal
- one_top
- polishSpaceMetric
- pred_apply
- pred_eq
- preimage_smul_set
- preimage_smul_setₛₗ
- preimage_smul_setₛₗ_of_units
- preimage_vadd_set
- preimage_vadd_setₛₗ
- preimage_vadd_setₛₗ_of_addUnits
- prod_mk_mem_compRel
- punctured_nhds_neBot
- round_add_int
- round_add_nat
- round_int_add
- round_nat_add
- round_sub_int
- round_sub_nat
- row_add
- row_cons
- row_empty
- row_eq_zero
- row_injective
- row_mulVec
- row_mulVec_eq_const
- row_mul_col
- row_mul_col_apply
- row_smul
- row_vecMul
- row_zero
- self_eq_add_left
- self_eq_add_right
- self_eq_mul_left
- self_eq_mul_right
- self_ne_add_left
- self_ne_add_right
- self_ne_mul_left
- self_ne_mul_right
- shiftLeft_coe_nat
- shiftRight_coe_nat
- sign_eq_ediv_abs
- sizeOf_lt_sizeOf_of_mem
- slope_of_Y_ne_eq_eval
- smul_normal
- smul_preimage_set_le
- smul_preimage_set_leₛₗ
- snd_map_prod_mk
- snd_map_prod_mk₀
- spanningHom.injective
- succ_apply
- succ_eq
- sum_add_sum_comm
- t2Space_of_properSMul_of_t2Group
- tendsto_abs_nhdsWithin_zero
- tendsto_atBot_of_add_bdd_below_left
- tendsto_atBot_of_add_bdd_below_left'
- tendsto_atBot_of_add_bdd_below_right
- tendsto_atBot_of_add_bdd_below_right'
- tendsto_atTop_of_add_bdd_above_left
- tendsto_atTop_of_add_bdd_above_left'
- tendsto_atTop_of_add_bdd_above_right
- tendsto_atTop_of_add_bdd_above_right'
- tendsto_gauge_nhds_zero'
- tendsto_log_div_rpow_nhds_zero
- tendsto_log_mul_rpow_nhds_zero
- tendsto_log_mul_self_nhds_zero_left
- tendsto_log_nhdsWithin_zero
- tendsto_log_nhdsWithin_zero_left
- tendsto_log_nhdsWithin_zero_right
- tendsto_logb_nhdsWithin_zero
- tendsto_logb_nhdsWithin_zero_of_base_lt_one
- tendsto_logb_nhdsWithin_zero_right
- tendsto_logb_nhdsWithin_zero_right_of_base_lt_one
- toEssImageCompEssentialImageInclusio
- toMeasureEquiv
- toMeasureEquiv_symm
- toNNReal_coe_nat
- top_one
- top_toNNReal
- top_toReal
- trace_col_mul_row
- transfer_eq_map_of_le
- uniformAddGroup
- uniformAddGroup_of_addCommGroup
- uniformGroup_of_commGroup
- upgradePolishSpace
- vadd_preimage_set_le
- vadd_preimage_set_leₛₗ
- vadd_set_sum
- val_one''
- zero_sum_zero
- zero_toNNReal
- zero_toReal
-- IndepFun.ae_eq
-- IsConjExponent.conjExponent
-- IsConjExponent.inv_add_inv_conj
-- IsConjExponent.one_lt
-- boundedSMul
-- card_fintypeIcc
-- card_fintypeIco
-- card_fintypeIic
-- card_fintypeIio
-- card_fintypeIoc
-- card_fintypeIoo
-- card_fintype_uIcc
-- fromAffine_ne_zero
-- instUniformAddGroup
-- inv_add_inv_conj_ennreal
-- inv_ne_zero
-- inv_nonneg
-- inv_pos
-- isConjExponent_comm
-- isConjExponent_iff_eq_conjExponent
-- isConjExponent_one_div
-- lhopital_zero_nhds'
-- lhopital_zero_nhds_left
-- lhopital_zero_nhds_right
-- nonneg
-- one_div_ne_zero
-- one_div_nonneg
-- one_div_pos
-- one_le
-- prod_mk_left
-- prod_mk_right
-- sub_one_mul_conj
-- sub_one_ne_zero
-- sub_one_pos
--- IsConjExponent
--- conjExponent_eq
--- conj_eq
--- div_conj_eq_sub_one
--- inv_inv
--- inv_one_sub_inv
--- isConjExponent_iff
--- mul_eq_add
--- ne_zero
--- one_sub_inv
--- one_sub_inv_inv
--- pos
--- prod
--- symm
---- prod_mk

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Decrease in tech debt: (relative, absolute) = (1.00, 0.01)

Current number	Change	Type
87	-1	disabled deprecation lints

Current commit 66099ee81a
Reference commit 213ff10ae9

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).