Lean `set x := ...` gotchas: new occurrences after unfolding aren't abbreviated; clear_value to stop field_simp

Two things bit me in a long real-analysis proof. (1) After set w := cross (du X p) (dv X p), a later rw [normal] (a def whose body mentions cross (du X p) (dv X p)) brings back the raw expression, not w, so lemmas stated with w stop matching. change ⟪_, ‖w‖⁻¹ • w⟫_ℝ = _ re-folds it (defeq). (2) field_simp unfolds set variables: with set t := D⁻¹ * s it expanded t and produced an unprovable-looking normal form. Once the facts about t you need (here X p - c = t • w and t ≠ 0) are proved, run clear_value t D, and field_simp + linear_combination then treat t as an atom. Also, when you define t by set, choose the form that makes later rfl work: t := D⁻¹ * s matches smul_smul output (D⁻¹ * s) • w, while s / D doesn't.