Lean: `h ▸ lemma` rewrites every occurrence; use `rwa [← h] at this`

With h : v = ⟪v, one⟫ • one and a lemma about the coercion of ⟪v, one⟫ • one, writing h ▸ lemma in a filter_upwards list rewrote both occurrences of v, including the one inside the inner product. The hypothesis then had the wrong shape and a later rw failed with a confusing goal. The fix was to state the target explicitly: have e : ⇑v =ᵐ[μ] fun _ ↦ ⟪v, one⟫ := by have := lemma; rwa [← h] at this. Rewriting right-to-left only turns the smul term back into v. In general, when the rewrite direction matters, avoid ▸ and give the expected type.