Use `Is*Apply` classes

[mcdoll]

This is a tracking issue for replacing foo_apply type lemmas by the IsFooApply typeclasses introduced in #37779

The following list is not comprehensive and will be extended over time:

1. Abstract results

   • [Merged by Bors] - feat(Algebra): add abstract prod_apply and FunLike.coe_prod #39657
   • [Merged by Bors] - feat(Data/FunLike): coe_zero_iff lemmas #40260
   • [Merged by Bors] - chore(Data/FunLike): add apply lemmas for bundled coercions #40501
   • feat(Data/FunLike): add abbrevs for pointwise multiplication #40899
   • feat(Data/FunLike): typeclass for FunLike and coercion between types #40277
   • feat(Algebra): introduce notation typeclass for composition of functions #40534
   • IsCompApply

2. Homomorphism classes

   • feat(Algebra): use Is*Apply for LinearMap #39638
   • [Merged by Bors] - feat(Topology/Algebra): use Is*Apply for ContinuousLinearMap #39637
   • [Merged by Bors] - feat(Topology/Algebra): use Is*Apply for UniformConvergenceCLM #40446
   • NormedAddGroupHom

3. Multilinear

   • [Merged by Bors] - feat(LinearAlgebra): use Is*Apply for MultilinearMap #40466
   • [Merged by Bors] - feat(Topology/Algebra): use Is*Apply for ContinuousMultilinearMap #40463
   • FormalMultilinearSeries

4. Measure theory

   • [Merged by Bors] - feat(MeasureTheory): use IsApply for OuterMeasure #40945
   • feat(MeasureTheory): use IsApply for Measure #40840
   • [Merged by Bors] - feat(MeasureTheory): use Is*Apply for VectorMeasure #40450
   • StieltjesFunction
   • feat(MeasureTheory): use IsApply for SimpleFunc #40918

5. Continuous functions

   • ContinuousMap
   • BoundedContinuousMap
   • feat(Topology): use IsApply for ZeroAtInftyContinuousMap #40611
   • [Merged by Bors] - feat(Analysis): use IsApply for ContDiffMapSupportedIn #40607
   • [Merged by Bors] - feat(Analysis): use IsApply for TestFunction #40608
   • [Merged by Bors] - feat(Analysis/Distribution): use Is*Apply for SchwartzMap #40447

6. The rest

   • Matrix
   • feat(Algebra): use Is*Apply for CauSeq #40917
   • Finsupp
   • [Merged by Bors] - feat(Analysis): use Is*Apply for Seminorm #40880