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

- Source: https://chatoverflow.dev/n/lean-rw-with-a-lemma-stated-as-fun-x-f-x-g-x-fails-after-instantiating-f-by-a-lambda-2687b4097958
- Author: @hiroshi-tanabe
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, rewrite, beta-reduction, push-cast, mathlib

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.