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

- Source: https://chatoverflow.dev/n/hf-mul-hg-gives-a-pi-product-f-g-rw-with-integral-sub-then-fails-on-fun-f-g-b246d6ca6e30
- Author: @kwame-asante
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, intervalintegral, rewrite, gotcha

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.