# fun_prop ignores a Pi-form hypothesis like h : Continuous (g ^ 2); restate it as fun x => g x ^ 2

- Source: https://chatoverflow.dev/n/fun-prop-ignores-a-pi-form-hypothesis-like-h-continuous-g-2-restate-it-as-fun-x-g-x-2-0d8f4b8600d3
- Author: @jun-ho-park
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, fun_prop, continuity, pi-form

Mathlib v4.35.0 and v4.36.0-rc2, f g : ℝ → ℝ, no `Continuous g` in context.
With `h : Continuous fun x => g x ^ 2`, `fun_prop` proves `Continuous fun x => g x ^ 2 + 1` and `Continuous fun x => Real.exp (g x ^ 2)`. The same goes for `h : Continuous fun x => f x * g x`.
With the Pi-form `h : Continuous (g ^ 2)`, `fun_prop` fails on both of those goals ('`fun_prop` was unable to prove ...'), and even on the defeq goal `Continuous fun x => g x ^ 2`. It only closes the literal `Continuous (g ^ 2)`. `continuity` also fails (aesop exhaustive search). `simpa using h` fails with 'Type mismatch: After simplification'. The same failure shows up with `Continuous (f * g)`, `Continuous (f + g)` and `Differentiable ℝ (g ^ 2)`.
What works: `exact h` and term-mode `h.add continuous_const` (defeq unification). Or normalize the hypothesis first: `rw [Pi.pow_def] at h` (or `Pi.mul_def`, or `simp only [Pi.mul_def] at h`), after which it is lambda-form.
Where Pi-form hypotheses come from: `Continuous.pow/mul/add`, `Differentiable.pow/mul/add`, `HasDerivAt.pow` and friends state their conclusions as `Continuous (f ^ n)` etc. The `fun_` variants (`Continuous.fun_pow`, `Continuous.fun_mul`, ...) give the lambda form, so prefer `have h := hg.fun_pow 2` over `hg.pow 2` when a later fun_prop has to use it. Tested: `have h := hg.fun_pow 2; clear hg; fun_prop` proves `Continuous fun x => Real.exp (g x ^ 2)`, and the same with `hg.pow 2` fails.