Morphism classes not used for integration and related issues

There are a number of theorems about Bochner integrals (or even interval integrals) involving continuous linear maps related to composition. Most of these lemmas take honest-to-god ContinuousLinearMaps, but only ever use them in applied form. Therefore, they could be stated for the corresponding morphism class† without committing the cardinal sin of using morphism class coercions†† in the statement of a lemma. Since they are not, this leads to duplication of these lemmas for morphism types which happen to be continuous and linear (e.g., ContinuousLinearEquiv, LinearIsometry, etc.).

I noticed this during review of #40471 but decided not to ask the author to fix it because it's a comparatively large job.

An example of duplicated lemmas include: ContinuousLinearMap.integral_comp_comm, ContinuousLinearEquiv.integral_comp_comm, LinearIsometry.integral_comp_comm, but there are several others.

† We have ContinuousSemilinearMapClass and ContinuousLinearMapClass. We should deprecate these in favor of the existing unbundled classes ContinuousMapClass and SemilinearMapClass and LinearMapClass.

†† It seems we don't have these morphism class coercions for ContinuousLinearMap, which is good, but we're missing the underlying declarations themselves too (i.e., ContinuousLinearMap.ofClass); we should have those.

Start with the duplicated integral lemmas listed in Mathlib/MeasureTheory/Integral/Bochner/ContinuousLinearMap and compare their ContinuousLinearMap, ContinuousLinearEquiv, and LinearIsometry forms. Review ContinuousSemilinearMapClass and ContinuousLinearMapClass in Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean. Done means the relevant lemmas use the appropriate morphism classes without duplication, with the requested class deprecations and ContinuousLinearMap.ofClass declarations addressed.