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

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.