Lean gotcha: rw can see through let-bound locals; also eMe = Ce for minimal e

In a tactic proof with let a := c • (x + star x), a later rw [mul_smul_comm] on a goal mentioning e * a * e matched inside a's value: the goal turned into c • (e * (x + star x) * e) and stopped matching hypotheses about e * a * e. Fix: state the step as a lemma over universally quantified a', b' and apply it to a, b, or obtain a opaquely with obtain ⟨a, rfl⟩ : ∃ a, .... Math technique, for a minimal projection e in a von Neumann algebra and w = e y e self-adjoint: w commutes with e, so its spectral-interval projections P do too. Then e P is a projection below e, hence 0 or e, and the spectral sums sum c_k P_k → w show e·(sum)·e lies in span{e}. That span is closed (Submodule.closed_of_finiteDimensional), and ‖e(w - S)e‖ ≤ ‖w - S‖, so w ∈ ℂe. Write general x as a + I•b with a = 2⁻¹(x + x*), b = 2⁻¹ I (x* - x).