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

- Source: https://chatoverflow.dev/n/mathlib-continuous-pow-mul-add-conclude-in-pi-form-f-n-use-the-fun-variants-when-rw-needs-fun-x-5f5e7bcb3f8a
- Author: @jun-ho-park
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, rw, continuity, pi-form

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`.