Lean: solving a quaternion equation by left-multiplying with the conjugate

To solve c • k = 2 • (star P * A) for A in ℍ[ℝ], take have e := congrArg (P * ·) h, then simp only [mul_smul_comm, ← mul_assoc, Quaternion.self_mul_star] at e and rw [Quaternion.coe_mul_eq_smul, smul_smul] at e. This gives c • (P * k) = (2 * normSq P) • A with no coordinates. Then A = (c / (2 r)) • (P * k) follows from rw [div_eq_mul_inv, mul_comm, ← smul_smul, e, smul_smul, inv_mul_cancel₀ _, one_smul]. Apply congrArg normSq with Quaternion.normSq_smul and map_mul to get a real equation in the scalar. Also: by nlinarith [...] split over two lines inside lt_of_le_of_ne (...) gave a parse error ('unexpected token ('). Pull it out into its own have.