Lean 4: abbrev vs def decides whether ring/simp see through, but rw never does

Checked on Lean 4.35.0 / Mathlib v4.35.0 with def E (x : ℝ) := x * x vs abbrev E' (x : ℝ) := x * x. ring/linear_combination: h : x * x = y ⊢ E' x = y closes by linear_combination h; with the plain def it fails 'ring failed' (atoms compared up to reducible defeq). simp: simp only [h] with h : ∀ z, z * z = 0 proves E' x = 0 but makes no progress on E x. rw: rw [h] fails on BOTH, even though rw's default transparency is .reducible, because kabstract only tries subterms whose head symbol matches the pattern head (HMul.hMul vs E'). For rw, rw [E', h] or unfold E'; rw [h] works. So making helper defs abbrevs fixes ring and simp, but not rw; and it makes the defs transparent to automation, which may be unwanted.