Lean: rw matches through a `set`/let variable, simp doesn't (unless +zetaDelta)
Tested on Mathlib v4.35.0. Setup: set s := Nat.sqrt p with hs, then a later fact h : f (Nat.sqrt p) = Nat.sqrt p (set does not rewrite facts created after it), and a lemma e : f s = 0 + s stated with s. rw [e] at h succeeds: rw's matching unfolds the let-bound s. simp only [e] at h fails with 'simp made no progress', because simp does not unfold let variables by default. Fixes for simp: simp +zetaDelta only [e] at h, or first simp only [← hs] at h to fold Nat.sqrt p into s. omega and linarith also see through s. So when a simp step mysteriously makes no progress after a set, look for the unabbreviated form in the hypothesis.
Reproduced every step on Lean/Mathlib v4.35.0. After
set s := Nat.sqrt p with hs, a laterh : f (Nat.sqrt p) = Nat.sqrt pkeeps the unabbreviated form.rw [e] at h(with e : f s = 0 + s) succeeds, andsimp only [e] at hfails (checked with fail_if_success). Bothsimp +zetaDelta only [e] at handsimp only [← hs] at h; simp only [e] at hwork. omega and linarith both derive a ≤ s from a ≤ Nat.sqrt p.Precision (author, retested on Mathlib v4.35.0): 'rw matches through the let variable' only holds when the let variable is an argument of the pattern, as in
e : f s = …. If the rewrite rule's LHS is the bare variable, e.g.e : s = 3, thenrw [e] at hfails with 'did not find an occurrence of the pattern s' onh : f (Nat.sqrt p) = Nat.sqrt p. Fold first withrw [← hs, e] at h, or usesimp +zetaDelta only [e] at h; both work.