[Merged by Bors] - chore: remove declarations deprecated between 2021-04-15 and 2025-10-15

[mathlib-nolints]

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 11873348d8

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

- AddUnits.neg_mul_left
- AddUnits.neg_mul_right
- AreCardinalFilteredGenerators
- CommGrp_
- Compatible.srel_iff_lt
- CostructuredArrow.isSeparating_proj_preimage
- Cover.pullbackCover
- Cover.pullbackCover'
- FamilyOfElements.Compatible.compPresheafMap
- FamilyOfElements.IsAmalgamation.compPresheafMap
- FamilyOfElements.compPresheafMap
- FamilyOfElements.compPresheafMap_comp
- FamilyOfElements.compPresheafMap_id
- Grp_
- HasCardinalFilteredGenerators
- Hom.Spec_map_residueFieldMap_fromSpecResidueField
- Hom.Spec_map_residueFieldMap_fromSpecResidueField_assoc
- IsClosed.tendsto_coe_cofinite_of_discreteTopology
- IsCodetecting
- IsCodetecting.isCoseparating
- IsCodetecting.isIso_iff_of_epi
- IsCodetecting.mono
- IsCoseparating
- IsCoseparating.isCodetecting
- IsCoseparating.mono
- IsCoseparating.of_equivalence
- IsDetecting
- IsDetecting.isIso_iff_of_mono
- IsDetecting.isSeparating
- IsDetecting.mono
- IsFwInvariant
- IsFwInvariant.isInvariant
- IsIntegralHom.integral_app
- IsInvariant.isFwInvariant
- IsLocalAtSource
- IsLocalAtTarget
- IsLocalAtTarget.descendsAlong
- IsLocalAtTarget.descendsAlong_inf_quasiCompact
- IsProper.of_comp_of_isSeparated
- IsSeparating
- IsSeparating.isDetecting
- IsSeparating.isSeparator_coproduct
- IsSeparating.mono
- IsSeparating.of_equivalence
- IsTopologicalAddGroup.toUniformSpace
- IsTopologicalGroup.toUniformSpace
- IsTransitiveRel.mem_filter_prod_comm
- IsUniformAddGroup.toUniformSpace_eq
- IsUniformGroup.toUniformSpace_eq
- LinearOrderedCommGroup.mul_lt_mul_left'
- LinearOrderedCommGroup.mul_lt_mul_right'
- Nat.Prime.mod_four_ne_three_of_dvd_isSquare_neg_one
- PosDef.commute_iff
- PosDef.posDef_sqrt
- Pullback.forget_comparison_surjective
- QuasiSeparated.diagonalQuasiCompact
- Scheme.Opens.toSpecΓ_SpecMap_map
- Scheme.Opens.toSpecΓ_SpecMap_map_assoc
- Scheme.Spec_map_presheaf_map_eqToHom
- Scheme.exists_hom_isAffine_of_isLocalAtSource
- Scheme.iso_hom_base_inv_base
- Scheme.iso_hom_base_inv_base_apply
- Scheme.iso_inv_base_hom_base
- Scheme.iso_inv_base_hom_base_apply
- Scheme.map_basicOpen
- Scheme.map_basicOpen_map
- Scheme.openCoverOfISupEqTop
- Sorted.coe_getIso_apply
- Sorted.coe_getIso_symm_apply
- Sorted.cons
- Sorted.decide
- Sorted.eq_of_mem_iff
- Sorted.getIso
- Sorted.get_mono
- Sorted.get_strictMono
- Sorted.head!_le
- Sorted.insertionSort_eq
- Sorted.le_head!
- Sorted.nodup
- Sorted.orderedInsert
- Sorted.rel_get_of_le
- Sorted.rel_get_of_lt
- Sorted.sbtw
- Sorted.wbtw
- Spec.map_base_apply
- Spec_map_appLE_fromSpec
- Spec_map_appLE_fromSpec_assoc
- Spec_map_iff
- Spec_map_localization_isIso
- Spec_map_residue
- Spec_map_residue_apply
- Spec_map_stalkMap_fromSpecStalk
- Spec_map_stalkMap_fromSpecStalk_assoc
- Spec_map_stalkSpecializes_fromSpecStalk
- Spec_map_stalkSpecializes_fromSpecStalk_assoc
- Spec_map_tensorInl_fromSpecResidueField
- Spec_map_tensor_isPullback
- StructuredArrow.isCoseparating_proj_preimage
- ZMod.isSquare_neg_one_iff
- abs_characteristic_sub_characteristic_shift_eqO
- affinePreimage
- algEquivOfAssociated_apply_root
- algEquivOfEq_apply_root
- algHomOfDvd_apply_root
- appLE_comp_appLE
- app_eq
- arrowStalkMapIsoOfEq
- basicOpen_union_eq_self_iff
- bsup_eq_sup
- bsup_eq_sup'
- card_le_of_injective
- card_le_of_surjective
- card_sum
- cartesianMonoidalCategoryAddCommGrp
- coe_liftHom
- coe_resLE_base
- comp
- comp_app
- comp_appLE
- comp_appLE_assoc
- comp_appTop
- comp_appTop_assoc
- comp_app_assoc
- comp_base
- comp_base_apply
- comp_base_assoc
- comp_coeBase
- comp_coeBase_assoc
- comp_toLRSHom
- comp_toLRSHom_assoc
- condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft
- congr_app
- diagonal_Spec_map
- differentiableAt_comp_const_add
- discreteTopology
- discreteTopology_of_codiscreteWithin
- ediv_ediv_eq_ediv_mul
- eqToHom_c_app
- eq_of_perm_of_sorted
- eq_of_prod_eq_prod
- eq_top_if_isMultiplyPretransitive
- exists_finite_submodule_left_of_finite
- exists_finite_submodule_left_of_finite'
- exists_finite_submodule_of_finite
- exists_finite_submodule_of_finite'
- exists_finite_submodule_right_of_finite
- exists_finite_submodule_right_of_finite'
- exists_maximalIdeal_pow_le_of_finite_quotient
- finRange_succ_eq_map
- forall_open_iff_discrete
- forgetCreatesConnectedLimits
- forgetPreservesConnectedLimits
- forget₂Grp_
- formPerm_eq_self_of_notMem
- fromGlued_isOpenEmbedding
- fromGlued_open_map
- fullyFaithfulForget₂Grp_
- groupoid_of_isCodetecting_empty
- groupoid_of_isDetecting_empty
- iSup_succ
- id.base
- id_app
- id_appTop
- iff_exists_resLE
- iff_stalk_iso
- image_le_image_of_le
- image_preimage_eq_opensRange_inter
- inv_app
- inv_appTop
- isBasis_affine_open
- isCodetecting_empty_of_groupoid
- isCodetecting_iff_isCoseparating
- isCodetecting_op_iff
- isCodetecting_unop_iff
- isCompactOpen_iff_eq_basicOpen_union
- isCompactOpen_iff_eq_finset_affine_union
- isCoseparating_empty_of_thin
- isCoseparating_iff_mono
- isCoseparating_op_iff
- isCoseparating_unop_iff
- isDetecting_empty_of_groupoid
- isDetecting_iff_isSeparating
- isDetecting_op_iff
- isDetecting_unop_iff
- isFiltered_of_isCardinalDirected
- isFwInvariant_iff_isInvariant
- isLocalAtTarget
- isOpen_closedball
- isPullback_Spec_map_isPushout
- isPullback_Spec_map_pushout
- isSeparating_empty_of_thin
- isSeparating_iff_epi
- isSeparating_op_iff
- isSeparating_unop_iff
- is_closed'
- is_irreducible'
- isoSpec_hom_base_apply
- ker_lift_injective
- le_of_isLocalAtSource
- le_pow_iff_clog_le
- le_preimage_resLE_iff
- lieBracket_fmul_left
- liftHom
- liftHom_eq_algHom
- liftHom_mk
- liftHom_of
- liftHom_root
- lsub_le_sup_succ
- lt_pow_iff_log_lt
- mapComp'_hom_comp_mapComp'_hom_whiskerRight
- mapComp'_hom_comp_whiskerLeft_mapComp'_hom
- mapComp'_inv_comp_mapComp'_hom
- mapComp'_inv_whiskerRight_comp_mapComp'_inv
- map_Spec_map
- map_mem_image_iff
- map_ΓIso_hom
- mem_of_formPerm_ne_self
- mk_Spec_map
- mk_multiset_of_countable
- mul_one'
- mul_zero'
- nat_card_ofStabilizer_eq_add_one
- nonPrincipals
- nonPrincipals_def
- nonPrincipals_eq_empty_iff
- nonPrincipals_zorn
- norm_uncenteredCovarianceBilin_le
- of_isLocalAtSource_of_isLocalAtTarget
- of_isLocalAtTarget
- of_isOpenImmersion
- of_isPullback
- of_range_subset_iSup
- of_stalk_iso
- one_mul'
- openCoverOfISupEqTop
- opensRange_pullback_fst_of_right
- opensRange_pullback_snd_of_left
- orbitRel.Quotient.orbit_nonempty
- orbit_nonempty
- pi_mem_of_mulSingle_mem_aux
- pnat_multipliable_iff_multipliable_succ
- polar_weak_closed
- posDef_iff_eq_conjTranspose_mul_self
- pow_eq_zero
- pow_le_iff_le_log
- pow_lt_iff_lt_clog
- preimage_comp
- preimage_iSup_eq_top
- preimage_le_preimage_of_le
- presheaf_map_eqToHom_op
- prod_roots_eq_coeff_zero_of_monic_of_splits
- quasiCompact_iff_forall_affine
- quasiCompact_iff_spectral
- quasiCompact_over_affine_iff
- quasiSeparatedSpace_iff_affine
- quasiSeparated_over_affine_iff
- range_pullback_fst_of_right
- range_pullback_snd_of_left
- resLE
- respectsLeft_isOpenImmersion
- restrict
- sdiff_eq_self_iff_disjoint'
- selfAdjoint.nnnorm_pow_two_pow
- self_le_basicOpen_union_iff
- sigmaDesc
- singletons_open_iff_discrete
- sorted_cons_cons
- sorted_insertionSort
- sorted_ofFn_iff
- sorted_replicate
- specTensorTo_base_fst
- specTensorTo_base_snd
- stalkMap_comp
- stalkMap_congr
- stalkMap_congr_assoc
- stalkMap_congr_hom
- stalkMap_congr_hom_assoc
- stalkMap_congr_point
- stalkMap_congr_point_assoc
- stalkMap_germ
- stalkMap_germ_apply
- stalkMap_germ_assoc
- stalkMap_hom_inv
- stalkMap_hom_inv_apply
- stalkMap_hom_inv_assoc
- stalkMap_id
- stalkMap_inv_hom
- stalkMap_inv_hom_apply
- stalkMap_inv_hom_assoc
- stalkSpecializes_stalkMap
- stalkSpecializes_stalkMap_apply
- stalkSpecializes_stalkMap_assoc
- stalkwiseIsLocalAtTarget_of_respectsIso
- stalkwise_Spec_map_iff
- stalkwise_isLocalAtSource_of_respectsIso
- sublist_of_subperm_of_sorted
- sum_roots_eq_nextCoeff_of_monic_of_split
- sup_eq_bsup
- sup_eq_bsup'
- sup_eq_lsub
- sup_eq_lsub_iff_lt_sup
- sup_eq_lsub_iff_succ
- sup_eq_lsub_or_sup_succ_eq_lsub
- sup_eq_sup
- sup_le_lsub
- sup_succ_eq_lsub
- sup_succ_le_lsub
- sup_typein_limit
- sup_typein_succ
- tail
- thin_of_isCoseparating_empty
- thin_of_isSeparating_empty
- toGrp_
- toHomeomorphOfContinuousOpen_toEquiv
- toHomeomorph_symm
- toHomeomorph_toEquiv
- to_iso
- topologicalGroup_is_uniform_of_compactSpace
- topologically_isLocalAtSource
- topologically_isLocalAtSource'
- topologically_isLocalAtTarget
- topologically_isLocalAtTarget'
- uncenteredCovarianceBilin
- uncenteredCovarianceBilin_apply
- uncenteredCovarianceBilin_of_not_memLp
- uncenteredCovarianceBilin_zero
- uncurryFin
- uncurryFinLM
- uncurryFin_add
- uncurryFin_apply
- uncurryFin_curryLeft
- uncurryFin_smul
- uncurryFin_uncurryFinLM_comp_of_symmetric
- universally_isLocalAtSource
- universally_isLocalAtTarget
- weightedHomogeneousComponent_of_isWeightedHomogeneous_ne
- weightedHomogeneousComponent_of_isWeightedHomogeneous_same
- whiskerLeft_mapComp'_inv_comp_mapComp'_inv
- xor_cancel_left
- xor_cancel_right
- xor_eq_zero
- xor_ne_zero
- zero_mul'
- zeta_mul_kappa
- Γ_map_morphismRestrict
- ι_base_apply
-- iff_of_iSup_eq_top
-- iff_of_openCover
-- lt_of_forall_lt_of_lt
-- map_add
-- map_neg
-- map_smul
-- map_sub
-- map_zero
-- mk'
-- of_iSup_eq_top
-- of_openCover
-- small_proj_preimage_of_locallySmall
-- sort_sorted

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

[adomani]

The commits deleting the empty sections were manual, right? We should look into running the global syntax linter on the output of this workflow and act on its findings.

[bryangingechen]

Yes, they were manual.

[adomani]

The script

git diff upstream/master...deprecated-decls | grep -5 "^ --[^-]"

finds comments that are present in deprecated-decls and are "close" to the diff with master.

For instance, running it on the commit where @Parcly-Taxel identified the extra comment that could be removed:

git diff upstream/master...85044fb2bff2101617e4055cc4f92e226ea2c72d | grep -5 "^ --[^-]"

identifies the comment that was flagged. With a bit more effort, the command could also show just the hits where the comment precedes a deleted line, but since there are so few false positives, maybe it is not worth fixing.

Anyway, I am mentioning this, since the PR description might suggest it (below the fold) as a test to perform.

[adomani]

#38124 is running the generic syntax linter on this PR.

[adomani]

I removed the pairs section/variable/namespace followed by end that the linter found, without even checking if they were caused by this PR.

Everything looks good to me!

bors d+

[mathlib-bors]

✌️ mathlib-nolints[bot] can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[adomani]

bors d=bryangingechen

[mathlib-bors]

✌️ bryangingechen can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[bryangingechen]

bors r+

[bryangingechen]

I couldn't find the PR for the global syntax linter, but maybe we should add it as an extra step to the deprecated declarations workflow in that PR.

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job