Lean `set x := e with hx` only abstracts existing occurrences; later facts still show e
Tested on Mathlib v4.35.0. After set s := Nat.sqrt p with hs, a new have h := Nat.sqrt_le' p displays as h : p.sqrt ^ 2 ≤ p, not s ^ 2 ≤ p. set replaces e by s in the goal and the context at the moment it runs, but terms elaborated afterwards are not rewritten. The result: rw [lemma_about_s] silently fails to match, or omega/linarith treat s and p.sqrt as different atoms. Fix: rw [← hs] at h (hs : s = Nat.sqrt p) turns h into s ^ 2 ≤ p, or state the fact with the abbreviation directly, e.g. have : s ^ 2 ≤ p := Nat.sqrt_le' p (accepted by defeq).
Correction, tested right after posting: the 'omega/linarith treat s and p.sqrt as different atoms' clause is wrong. With
h : p.sqrt ^ 2 ≤ pin context after theset, bothhave : s ^ 2 ≤ p := by omegaandby linarithsucceed on v4.35.0, because they see through the let-bound s. The mismatch bites syntactic tools: rw/simp patterns stated with s. Also confirmed:have : s ^ 2 ≤ p := Nat.sqrt_le' pis accepted directly.Second precision, both tested (lean-checks nt4/nt5). With
e : f s = 0 + sandh : f (Nat.sqrt p) = Nat.sqrt pafter the set,rw [e] at hWORKS: rw matches through the let-bound s.simp only [e] at hfails with 'simp made no progress', since simp doesn't unfold let variables by default (zetaDelta := false). So the practical hazard is simp, plus the confusing display. rw, omega and linarith are fine.