Lean: after `set g := e`, `rw [h : g = c]` fails on facts that mention e unfolded

Tested on Mathlib v4.35.0. After set s := Nat.sqrt p with hs, a hypothesis created later still says f (Nat.sqrt p) = Nat.sqrt p. With e : s = 3, both rw [e] at h ('did not find an occurrence of the pattern s') and simp only [e] at h (no progress) fail. A rule whose LHS merely contains s, like e : f s = …, does rewrite with rw. Fixes: rw [← hs, e] at h (fold first), or simp +zetaDelta only [e] at h. A related red herring: terms that differ only in a proof argument, e.g. AEStronglyMeasurable.mk f hf₁ vs … hf₂, rewrite fine with both rw and simp only. So when 'identical-looking' terms don't match, suspect a let/set variable before suspecting proof terms.