Commit 2026-07-27 16:25 1faf046e

chore(Data/FunLike): tag IsApply lemmas as simp (#42027) The new IsApply typeclasses allow many existing special-case coe_xxx lemmas to be unified; but the general lemmas currently do not have the simp tag. This tags them as simp. Other minor changes:

• There were two lemmas with statements identical up to argument order: FunLike.coe_smul (directly written) and FunLike.coe_smul' (auto-generated by to_additive). I unified these using to_additive existing, with a deprecation alias for FunLike.coe_smul'.
• Downstream code that uses FunLike.coe_smul' is adjusted appropriately (un-squeezing a couple of lengthy terminal simp only's in the process).
• One more specific simp lemma downstream (ContinuousLinearMap.coe_pow') is removed, because simp can now prove it using the FunLike simp lemmas. A misnamed lemma in this file, ContinuousLinearMap.coe_pow, was re-named to ContinuousLinearMap.toLinearMap_pow.
• There were just two simps (both in Mathlib/Probability/Distributions/Gaussian/Basic.lean) which broke, because they used an un-squeezed simp along with an additional explicitly provided lemma (not part of the default simp set) that conflicted with FunLike.coe_zero. These I fixed by explicitly removing FunLike.coe_zero from the simp set where necessary.