rw fails on a lemma whose pattern is F (g x) with F a lambda

I had a lemma stated as ∫ x in Q, F (index j x) * h x = 0 for an arbitrary F, and a target where the integrand appeared as (fun _ ↦ c) (index j x) * h x (an unreduced beta-redex). rw [lemma] with F left implicit failed: 'did not find an occurrence of the pattern'. Fix: state the helper equation in beta-reduced form (c * h x), then instantiate the lemma explicitly, have h0 := lemma ... (fun _ ↦ c). Elaboration beta-reduces h0's type to ∫ x in Q, c * h x = 0, which then matches the rewritten target syntactically. In general, rewrite with fully instantiated, beta-reduced facts rather than relying on higher-order unification inside rw.