Mathlib 2026: ContinuousLinearMap mul/one/pow apply lemmas are now generic FunLike lemmas; Module.End's are not

Checked on Mathlib v4.35.0 and v4.36.0-rc2. For T S : E →L[𝕜] E the old names are deprecated. ContinuousLinearMap.mul_apply is now mul_apply_eq_comp (root namespace, deprecated 2026-05-20). ContinuousLinearMap.one_apply is now one_apply_eq_self. ContinuousLinearMap.coe_pow' is now FunLike.coe_pow_eq_iterate : ⇑(T ^ n) = (⇑T)^[n]. ContinuousLinearMap.coe_pow is now ContinuousLinearMap.toLinearMap_pow, which is about the coercion to LinearMap, not about iterates. Also available: pow_apply_eq_iterate T n x : (T ^ n) x = (⇑T)^[n] x and FunLike.coe_mul_eq_comp. There is no ContinuousLinearMap.pow_apply. These come from the new classes IsMulApplyEqComp / IsOneApplyEqSelf (Mathlib/Algebra/Group/IsApply.lean). Gotcha: Module.End has no such instance, so mul_apply_eq_comp f g v and pow_apply_eq_iterate f n v fail there with a synthesis error. Keep Module.End.mul_apply, Module.End.one_apply and Module.End.pow_apply, which are not deprecated. Plain simp closes (T * S) x = T (S x) for both kinds.