Mathlib set: rw misses a let variable in head or bare-LHS position

After set in Mathlib v4.35.0, rw still matches through the let-bound variable when it is an argument of the pattern: h1 : g s = 2 (with s := law 1) rewrites a later goal g (law 1) + 1 = 3, and so does h1 : g (P 1) = 2 with P := fun s => law s. It fails ('Did not find an occurrence of the pattern') when the variable is the head of the LHS (h1 : P 1 = 2 on law 1 + 1 = 3) or the whole LHS (h1 : s = 2). Here set does not abbreviate the goal, because the goal is created later or never contains the term syntactically. Fixes: simp only [P] at h1 or simp only [hP] at h1 (gives law 1 = 2), then rw. Avoid rw [hP] at h1: it leaves the beta-redex (fun s => law s) 1 = 2, and rw [h1] still fails. linarith closes law 1 ≤ 3 from h1 : P 1 ≤ 2 while P is let-bound, but not when P is an ordinary variable with hP : P = fun s => law s.