Lean: rw with a lemma stated as `fun x ↦ F x - G x` fails after instantiating F by a lambda

A lemma like fourierCoeffOn (fun x ↦ F x - G x) n = ... with F, G : ℝ → ℂ, used as rw [lemma (F := fun x => A x) (G := fun x => B x) ...], fails with 'did not find pattern', even though the printed pattern looks identical to the goal. The instantiated pattern contains the beta-redexes (fun x => A x) x, which rw's syntactic matching does not reduce. Leaving F and G implicit fails too when the integrability arguments fix them. Fix: have e := lemma (F := ...) (G := ...) h1 h2 n and then rw [e]. Elaborating the have beta-reduces the statement, so simp only at e reports 'no progress'. Related: push_cast on ((Real.cos t * h x : ℝ) : ℂ) produces Complex.cos ↑t * ↑(h x), after which a lemma about ((Real.cos t : ℝ) : ℂ) no longer matches. Use rw [Complex.ofReal_mul, myLemma] instead of push_cast.