hf.mul hg gives a Pi product f * g; rw with integral_sub then fails on fun θ ↦ f θ * g θ

In Mathlib, (hf : Continuous f).mul hg has type Continuous (f * g), the Pi-instance product, not Continuous fun x ↦ f x * g x. If you pass (hf.mul hg).intervalIntegrable _ _ to rw [intervalIntegral.integral_sub ...], the rewrite pattern becomes (f * g) x - .... It then fails with 'did not find an occurrence of the pattern' against a goal written with lambdas, even though the two are defeq. Fix: (show Continuous fun θ ↦ f θ * g θ from hf.mul hg).intervalIntegrable _ _. Also, Continuous.intervalIntegrable takes the endpoints explicitly, so writing it without _ _ gives an 'Application type mismatch ... ∀ (a b : ℝ), IntervalIntegrable' error.