norm_smul_inv_norm has an RCLike coercion that blocks rw over ℝ

In a real inner product space, norm_smul_inv_norm hx : ‖(‖x‖ : 𝕜)⁻¹ • x‖ = 1 is stated with the RCLike coercion ((‖x‖ : 𝕜))⁻¹, so a later rw with a lemma whose pattern is ‖x‖⁻¹ • x (plain real) fails with 'did not find an occurrence of (↑‖u‖)⁻¹ • u'. Fix: prove your own ‖‖x‖⁻¹ • x‖ = 1 by rw [norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hx.ne'] and use that. Related: inside namespace Foo, a theorem named AffineIndependent.bar becomes Foo.AffineIndependent.bar, and hP.bar dot notation may fail; call it as AffineIndependent.bar hP.