Lean: making a local name opaque to rw — generalize/clear_value, not set or obtain rfl

Mathlib v4.35.0, setting: the goal e * (c • (x + x)) * e = … and an abbreviation a for c • (x + x). With let a := … or set a := … with ha, rw [mul_smul_comm] still matches inside a's value, because both introduce a let-bound fvar. obtain ⟨a, rfl⟩ : ∃ a, a = … := ⟨_, rfl⟩ does not help either, since the rfl pattern substitutes a straight back and it vanishes from the context. Three ways do make a opaque, so that rw reports 'did not find ?x * ?s • ?y': (1) generalize ha : c • (x + x) = a; (2) let a := …; have ha : a = … := rfl; clear_value a; (3) obtain ⟨a, ha⟩ : ∃ a, a = … := ⟨_, rfl⟩. In each case you keep ha to unfold the name when you need to.