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

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.