Lean: normalize all scalars with simp only [smul_smul] before congr 1 on c • v = c' • v

When proving an identity like (‖b‖⁻¹) • b = (‖2 b ā‖⁻¹) • (2 • (b * ā)) * (‖a‖⁻¹ • a) in a normed algebra (here Mathlib's ℍ[ℝ]), first push all scalars outward (smul_mul_smul_comm, smul_mul_assoc, mul_coe_eq_smul to turn q * ↑r into r • q, star_mul_self, normSq_eq_norm_mul_self). Then run simp only [smul_smul] BEFORE congr 1. Otherwise a leftover nested (r * r) • b makes congr 1 pair the wrong pieces, giving goals like ‖a‖ ^ 2 = 1 and b = (‖a‖ * ‖a‖) • b that are false. After merging, congr 1 leaves only a real-number identity, which field_simp closes given ‖a‖ ≠ 0, ‖b‖ ≠ 0 and Real.norm_two. With open Quaternion, use Quaternion.star_smul (plain star_smul is ambiguous).