[EtienneC30]

---

• depends on: [Merged by Bors] - feat: use IsApply for BoundedContinuousFunction #45087
• depends on: [Merged by Bors] - feat: use IsApply for FiniteMeasure #45123
• depends on: feat: missing evaluation and coercion definitions #45295

[github-actions]

PR summary a81cdf663b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ add_apply
+ coeFnAddMonoidHom
+ coe_add
+ coe_neg
+ coe_nsmul
+ coe_sub
+ coe_sum
+ coe_vadd
+ coe_zero
+ coe_zsmul
+ instance [CommMonoid β] [ContinuousMul β] : CommMonoid C(α, β) := fast_instance% FunLike.commMonoid
+ instance [Div β] [ContinuousDiv β] : IsDivApply C(α, β)
+ instance [Group β] [IsTopologicalGroup β] : Group C(α, β) := fast_instance% FunLike.group
+ instance [Group β] [IsTopologicalGroup β] : IsPowApply ℤ C(α, β)
+ instance [IntCast β] : IsIntCastApply C(α, β)
+ instance [Inv β] [ContinuousInv β] : IsInvApply C(α, β)
+ instance [Monoid β] [ContinuousMul β] : IsPowApply ℕ C(α, β)
+ instance [Monoid β] [ContinuousMul β] : Monoid C(α, β) := fast_instance% FunLike.monoid
+ instance [Mul β] [ContinuousMul β] : IsMulApply C(α, β)
+ instance [NatCast β] : IsNatCastApply C(α, β)
+ instance [One β] : IsOneApply C(α, β)
+ instance [SMul R M] [ContinuousConstSMul R M] : IsSMulApply R C(α, M)
+ instance [Semigroup β] [ContinuousMul β] : Semigroup C(α, β) := fast_instance% FunLike.semigroup
+ neg_apply
+ nsmul_apply
+ sub_apply
+ sum_apply
+ vadd_apply
+ zero_apply
+ zsmul_apply
- instance [CommMonoid β] [ContinuousMul β] : CommMonoid C(α, β) := fast_instance%
- instance [Group β] [IsTopologicalGroup β] : Group C(α, β) := fast_instance%
- instance [Monoid β] [ContinuousMul β] : Monoid C(α, β) := fast_instance%
- instance [Semigroup β] [ContinuousMul β] : Semigroup C(α, β) := fast_instance%

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)

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

• +16 new declarations
• −2 removed declarations

-ContinuousMap.coeFnAddMonoidHom_apply
-ContinuousMap.coeFnMonoidHom_apply
+ContinuousMap.instIsAddApply
+ContinuousMap.instIsDivApply
+ContinuousMap.instIsIntCastApply
+ContinuousMap.instIsInvApply
+ContinuousMap.instIsMulApply
+ContinuousMap.instIsNSMulApplyInt
+ContinuousMap.instIsNSMulApplyNat
+ContinuousMap.instIsNatCastApply
+ContinuousMap.instIsNegApply
+ContinuousMap.instIsOneApply
+ContinuousMap.instIsPowApplyInt
+ContinuousMap.instIsPowApplyNat
+ContinuousMap.instIsSMulApply
+ContinuousMap.instIsSubApply
+ContinuousMap.instIsVAddApply
+ContinuousMap.instIsZeroApply

---

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

Current commit a81cdf663b
Reference commit 401d9e6852

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).

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat: use IsApply for BoundedContinuousFunction #45087
• [Merged by Bors] - feat: use IsApply for FiniteMeasure #45123
• feat: missing evaluation and coercion definitions #45295
  By Dependent Issues (🤖). Happy coding!

[grunweg]

Thanks for doing this. I have only minor comments.

[grunweg]

Do these declarations differ in their order of implicit arguments? (Do we care? Can we make the deprecation indicate this, e.g. via +typeChanged.)

[grunweg]

In general, these names are somewhat common among other classes: should we mark more of these aliasses are protected?

[EtienneC30]

In #45081 Moritz indeed deprecated with +typeChanged instead of just putting an alias. Here it is actually the explicit arguments that are swapped for some reason. But among all the fixes I had to do they were all in simp or rw calls, so the arguments were not the issue.

To answer your second question, in most cases the coe_smul lemmas should not be protected but deprecated in favor of the right IsApply class.

[grunweg]

I agree about the deprecation. My question is: should we have a deprecated alias or a deprecated protected alias? If the latter ends up nicer, I think we should do the latter. (Perhaps it doesn't work, I haven't tested.)

[EtienneC30]

I think there is no need to protect the coe lemmas because the corresponding FunLike ones are in the FunLike namespace which is never opened. However the apply lemmas should be protected because the corresponding FunLike lemmas do not have a namespace.

[grunweg]

For instance, should these be protected? (Though I gather that this will be written explicitly much less.)

[mcdoll]

I think this should be an abstract definition for FunLike in the file for rings

[mcdoll]

Done in #45295

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.