Mathlib: Continuous.pow/mul/add conclude in Pi form (f ^ n); use the fun_ variants when rw needs fun x => ...

Mathlib v4.35.0 and v4.36.0-rc2, checked with #check. Many combinator lemmas state their conclusion about the Pi-type operation, not a lambda: Continuous.pow : Continuous f → ∀ n, Continuous (f ^ n), and likewise Continuous.mul/add/sub/neg/smul/div (Continuous (f * g) etc.), Continuous.inv₀ (Continuous f⁻¹), ContinuousOn.pow, ContinuousAt.pow, Differentiable.pow/mul/add, DifferentiableAt.pow, HasDerivAt.pow/mul, Measurable.mul/add, MeasureTheory.Integrable.add/neg, IntervalIntegrable.neg. exact/apply unify up to defeq, so they don't mind (in the example below, the same term passed to apply compiles). But anything you build from them carries (g ^ 2) x. Example: rw [intervalIntegral.integral_sub (hf.intervalIntegrable _ _) ((hg.pow 2).intervalIntegrable _ _)] fails against a goal containing ∫ θ in (0:ℝ)..c, g θ ^ 2 with 'did not find an occurrence of the pattern'. The lambda-form lemmas exist with a fun_ prefix: Continuous.fun_pow : Continuous fun i => f i ^ n, Continuous.fun_mul/fun_add/fun_sub/fun_neg/fun_smul/fun_inv₀, ContinuousOn.fun_pow, ContinuousAt.fun_pow, Differentiable.fun_mul/fun_add, Differentiable.fun_pow, DifferentiableAt.fun_pow, HasDerivAt.fun_pow/fun_mul, Measurable.fun_mul/fun_add, MeasureTheory.Integrable.fun_add/fun_neg. With (hg.fun_pow 2).intervalIntegrable _ _ the rw above succeeds. Continuous.fun_div, IntervalIntegrable.fun_neg and Continuous.fun_comp do not exist. For those, use (by fun_prop : Continuous fun θ ↦ ...) or show ... from. Already lambda-form without a prefix: Continuous.norm, Continuous.zpow₀, Differentiable.exp, Measurable.pow (two-function f x ^ g x), Measurable.pow_const, IntervalIntegrable.add, IntervalIntegrable.mul_continuousOn.