chore: fix misspellings in declaration names

[Multramate]

Fixes 34 misspelled declaration names — a dropped, doubled, inserted or transposed letter in each. The new name is the same tokens in the same order with the same capitalisation, so the whole diff is one decision repeated. Each rename keeps a @[deprecated] alias.

Split out of #43889.

Written with the assistance of Claude (Claude Code).

---

Two exceptions worth knowing before reading:

• isIso_SpecMap_stakMap_localization is the one name whose capitalisation also changes (SpecMap → specMap, matching how Spec.map is spelled).
• MonadCoherehnceHom is a class rather than a lemma, spans five tactic files, and carries this PR's only import addition, needed so its alias elaborates.

sylveserMap_comp_adjSylvester and adjSylvester_comp_sylveserMap reflow their signatures onto an extra line to stay under 100 columns; no semantic change.

[github-actions]

PR summary 9b86afb568

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.CategoryTheory.Coherence.Datatypes	95	96	+1 (+1.05%)
Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence	97	98	+1 (+1.03%)

Import changes for all files

Files	Import difference
3 files Mathlib.Tactic.CategoryTheory.Coherence.Datatypes Mathlib.Tactic.CategoryTheory.Coherence.Normalize Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence	1

---

Declarations diff (regex)

+ Bivariate.aeval_eq_map_swap
+ IsLindelof.compl_mem_coclosedLindelof_of_isClosed
+ LSeries.abscissaOfAbsConv_logPowMul
+ MonadCoherenceHom
+ MultilinearMap.domCoprod_alternatization
+ MultilinearMap.domCoprod_alternatization_coe
+ MultilinearMap.domCoprod_alternatization_eq
+ Scheme.Hom.closedPoints_subset_preimage_closedPoints
+ UniversalFactorizationRing.jacobian_presentation
+ _root_.Ideal.quotMapEquivTensorQuot
+ abscissaOfAbsConv_eq_one
+ adjSylvester_comp_sylvesterMap
+ alternatization_map_eq_zero_of_eq_aux
+ archimedeanClassMk_coe
+ cotangentEquiv_tmul
+ cpolynomialOn_uncurry_of_linear
+ div_nat_le_self_of_nonneg
+ dualSubmodulePairing
+ dualSubmodulePairing_spec
+ etaleLocus_eq_unramifiedLocus_inter_smoothLocus
+ exists_eq_graphOn_univ
+ fullyFaithulι
+ instance (priority := 100) _root_.PseudoMetricSpace.toIsCompletelyPseudoMetrizableSpace
+ instance : MonadCoherenceHom BicategoryM
+ instance : MonadCoherenceHom MonoidalM
+ isIso_specMap_stalkMap_localization
+ isSheafFor_ofArrows_iff_bijective_toCompatible
+ leftRightHomologyComparison'_eq_leftHomologyMap'_comp_iso_hom_comp_rightHomologyMap'
+ mapCommGrp_id_mul
+ partOrdEmb_dual_comp_forget_to_partOrd
+ primesOverEquivPrimesOver_inertiaDeg_eq
+ selfRightAction
+ sylvesterMap_comp_adjSylvester
+ tendsto_log_one_sub_sub_log_nhdsGT_atTop
+ toAddMonoidHom_commutes
+ toNonUnitalRingHom_comp_symm_toNonUnitalRingHom
- _root_.Ideal.qoutMapEquivTensorQout
- instance (priority := 100) _root_.PseudoMetricSpace.toIsCompletelPseudoMetrizableSpace
- instance : MonadCoherehnceHom BicategoryM
- instance : MonadCoherehnceHom MonoidalM

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- stale, waiting for the new build)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 9beca4d).

• +50 new declarations
• −18 removed declarations

+Algebra.Extension.cotangentEquiv_tmul
+Algebra.etaleLocus_eq_unramifiedLocus_inter_smoothLocus
+AlgebraicGeometry.Scheme.Hom.closedPoints_subset_preimage_closedPoints
+AlgebraicGeometry.isIso_specMap_stalkMap_localization
+CategoryTheory.Functor.mapCommGrp_id_mul
+CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.fullyFaithfulι
-CategoryTheory.MonoidalCategory.selRightfAction_actionAssocIso_hom
-CategoryTheory.MonoidalCategory.selRightfAction_actionAssocIso_inv
-CategoryTheory.MonoidalCategory.selRightfAction_actionHom
-CategoryTheory.MonoidalCategory.selRightfAction_actionHomLeft
-CategoryTheory.MonoidalCategory.selRightfAction_actionHomRight
-CategoryTheory.MonoidalCategory.selRightfAction_actionObj
-CategoryTheory.MonoidalCategory.selRightfAction_actionUnitIso
+CategoryTheory.MonoidalCategory.selfRightAction
+CategoryTheory.MonoidalCategory.selfRightAction_actionAssocIso_hom
+CategoryTheory.MonoidalCategory.selfRightAction_actionAssocIso_inv
+CategoryTheory.MonoidalCategory.selfRightAction_actionHom
+CategoryTheory.MonoidalCategory.selfRightAction_actionHomLeft
+CategoryTheory.MonoidalCategory.selfRightAction_actionHomRight
+CategoryTheory.MonoidalCategory.selfRightAction_actionObj
+CategoryTheory.MonoidalCategory.selfRightAction_actionUnitIso
+CategoryTheory.Presieve.isSheafFor_ofArrows_iff_bijective_toCompatible
+CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_leftHomologyMap'_comp_iso_hom_comp_rightHomologyMap'
+ContinuousMultilinearMap.cpolynomialOn_uncurry_of_linear
+DirichletCharacter.abscissaOfAbsConv_eq_one
+Hyperreal.archimedeanClassMk_coe
+Ideal.quotMapEquivTensorQuot
+IsDedekindDomain.primesOverEquivPrimesOver_inertiaDeg_eq
+IsLindelof.compl_mem_coclosedLindelof_of_isClosed
+LSeries.abscissaOfAbsConv_logPowMul
+LinearMap.BilinForm.dualSubmodulePairing
+LinearMap.BilinForm.dualSubmodulePairing_spec
-Mathlib.Tactic.Bicategory.instMonadCoherehnceHomBicategoryM
+Mathlib.Tactic.Bicategory.instMonadCoherenceHomBicategoryM
-Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom.casesOn
-Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom.ctorIdx
-Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom.mk
-Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom.mk.noConfusion
-Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom.noConfusion
-Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom.noConfusionType
-Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom.rec
-Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom.recOn
-Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom.unfoldM
+Mathlib.Tactic.BicategoryLike.MonadCoherenceHom
+Mathlib.Tactic.BicategoryLike.MonadCoherenceHom.casesOn
+Mathlib.Tactic.BicategoryLike.MonadCoherenceHom.ctorIdx
+Mathlib.Tactic.BicategoryLike.MonadCoherenceHom.mk
+Mathlib.Tactic.BicategoryLike.MonadCoherenceHom.mk.noConfusion
+Mathlib.Tactic.BicategoryLike.MonadCoherenceHom.noConfusion
+Mathlib.Tactic.BicategoryLike.MonadCoherenceHom.noConfusionType
+Mathlib.Tactic.BicategoryLike.MonadCoherenceHom.rec
+Mathlib.Tactic.BicategoryLike.MonadCoherenceHom.recOn
+Mathlib.Tactic.BicategoryLike.MonadCoherenceHom.unfoldM
-Mathlib.Tactic.Monoidal.instMonadCoherehnceHomMonoidalM
+Mathlib.Tactic.Monoidal.instMonadCoherenceHomMonoidalM
+MultilinearMap.domCoprod_alternatization
+MultilinearMap.domCoprod_alternatization_coe
+MultilinearMap.domCoprod_alternatization_eq
+Polynomial.Bivariate.aeval_eq_map_swap
+Polynomial.UniversalFactorizationRing.jacobian_presentation
+Polynomial.adjSylvester_comp_sylvesterMap
+Polynomial.sylvesterMap_comp_adjSylvester
+PseudoMetricSpace.toIsCompletelyPseudoMetrizableSpace
+RingEquiv.toAddMonoidHom_commutes
+RingEquiv.toNonUnitalRingHom_comp_symm_toNonUnitalRingHom
+Set.exists_eq_graphOn_univ
+div_nat_le_self_of_nonneg
+partOrdEmb_dual_comp_forget_to_partOrd

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 9b86afb568
Reference commit 7d680cae12

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py 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).

[grunweg]

Same question as in the other PRs: can you merge master, mention your LLM usage in the description and shorten the part of the PR description above the fold, please?

[kim-em]

The spelling changes look good, but the Lean-aware declaration diff reports 18 removals. In particular, MonadCoherehnceHom.unfoldM and the generated selRightfAction_* simps lemmas look plausibly user-facing. Could these receive deprecated aliases, or could we confirm that removing these generated names is intentional?