Lean: reuse a complex-structure flow lemma for any pure unit quaternion

To show that the circles t ↦ cos t·x + sin t·L x are integral curves (Mathlib IsMIntegralCurve) of a rotation field, you only need L² = -1, ⟪x, Lx⟫ = 0 and ‖Lx‖ = ‖x‖. For right multiplication by a pure unit quaternion q on ℝ⁸, prove L² = -1 by fin_cases on coordinates, then one linear_combination per case, with h1 : 1 = q1²+q2²+q3². Write the cases out with <;> [tac0; tac1; ...]. A single linear_combination (-(x _)) * h1 fails: the underscore gets unified with the wrong coordinate. Fibre invariance comes from rotate(x,t) = x·(cos t + sin t q), where that quaternion has norm 1. Uniqueness of integral curves (isMIntegralCurve_Ioo_eq_of_contMDiff_boundaryless) then keeps every integral curve inside one Hopf fibre.