q : ℍ
⊢ Commute (↑q.re) (im q)
q : ℍ
⊢ exp ℝ q = exp ℝ q.re • (↑(Real.cos ‖im q‖) + (Real.sin ‖im q‖ / ‖im q‖) • im q)
rw [← exp_of_re_eq_zero q.im q.im_re, ← coe_mul_eq_smul, ← exp_coe, ← exp_add_of_commute,
  re_add_im]
no goals
q : ℍ
⊢ Commute (↑q.re) (im q)
exact Algebra.commutes q.re (_ : ℍ[ℝ])