chore(Calculus/FDeriv/Pi): migrate to TVS

[urkud]

---

• depends on: [Merged by Bors] - chore(FDeriv/Pi): golf #35663
• depends on: feat(FDeriv/Prod): generalize to TVS #34941
• depends on: feat(FDeriv/Comp): migrate to TVS #34867

[github-actions]

PR summary c013fad581

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Calculus.FDeriv.Prod	1713	1710	-3 (-0.18%)
Mathlib.Analysis.BoxIntegral.DivergenceTheorem	2325	2322	-3 (-0.13%)
Mathlib.Analysis.Calculus.FDeriv.Bilinear	1714	1712	-2 (-0.12%)
Mathlib.Analysis.Calculus.FDeriv.CompCLM	1726	1724	-2 (-0.12%)
Mathlib.Analysis.Calculus.FDeriv.Pi	1714	1713	-1 (-0.06%)

Import changes for all files

Files	Import difference
Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.Analysis.Calculus.FDeriv.Prod	-3
Mathlib.Analysis.Calculus.FDeriv.Bilinear Mathlib.Analysis.Calculus.FDeriv.CompCLM	-2
3 files Mathlib.Analysis.Calculus.Deriv.Pi Mathlib.Analysis.Calculus.Deriv.Prod Mathlib.Analysis.Calculus.FDeriv.Pi	-1

---

Declarations diff

+ HasFDerivAt.comp_continuousLinearMap_of_eq
+ HasFDerivAtFilter.comp_continuousLinearMap
+ HasFDerivWithinAt.comp_continuousLinearMap_of_eq
+ HasStrictFDerivAt.comp_continuousLinearMap_of_eq
+ comp_differentiable
+ comp_differentiableAt
+ comp_differentiableOn
+ comp_differentiableWithinAt
+ comp_hasFDerivAt
+ comp_hasFDerivAtFilter
+ comp_hasFDerivWithinAt
+ comp_hasStrictFDerivAt
+ fderivWithin_comp_left
+ fderiv_comp_left
+ proj_comp_piCompRightL

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 scripts/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

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

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - chore(FDeriv/Pi): golf #35663
• feat(FDeriv/Prod): generalize to TVS #34941
• feat(FDeriv/Comp): migrate to TVS #34867
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

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