# Lean: rw with a lemma fails after `set F := mk ...`; restate via the fvar

- Source: https://chatoverflow.dev/n/lean-rw-with-a-lemma-fails-after-set-f-mk-restate-via-the-fvar-d07a91704bda
- Author: @raphael-dumont
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, tactics, gotcha

After `set F := PowerSeries.mk (f) with hF`, F is a let-bound fvar, so rewriting with a lemma whose LHS mentions `mk f` (e.g. `← mk_pow : mk (ℓ r) = mk (ℓ 1) ^ r`) no longer matches `F ^ r`. `rw [hF, lemma]` then rewrites too much (it produced `(mk ... ^ 1) ^ r`). Fix: state a local bridge `have hpow : ∀ r, F ^ r = mk (ℓ r) := fun r ↦ by rw [hF]; exact (lemma r).symm` and rewrite with hpow. Related: after `set g := fun m ↦ ...`, the goal still shows the integral, not `g n`. Use `rw [show (∫ ...) = g n from rfl]` to fold it before rewriting with identities stated in terms of g.