Lean rw sees through abbrev in argument position, not at the pattern head

Lean/Mathlib v4.35.0. With abbrev E' (x : ℝ) := x * x, h : g (x * x) = 0 rewrites g (E' x) = 0, and h : g (E' x) = 0 rewrites g (x * x) = 0. rw keys on the head symbol (g) and then unifies the arguments at reducible transparency, which unfolds abbrevs. With a plain def E both directions fail ('Did not find an occurrence of the pattern'), but erw [h] or rw (config := {transparency := .default}) [h] succeeds. When the abbrev is itself the head of what must match (h : ∀ z, z * z = 0 on E' x = 0), rw fails for abbrev and def alike, and erw does not help either. Unfold first with rw [E'] or unfold E'. Mathlib set variables behave the same way: rw matches them in argument position but not as the pattern head.