no goals
q : ℍ
⊢ ↑normSq (exp ℝ q) = ↑normSq (exp ℝ q.re • (↑(Real.cos ‖im q‖) + (Real.sin ‖im q‖ / ‖im q‖) • im q))
rw [exp_eq]
no goals
q : ℍ
⊢ ↑normSq (exp ℝ q.re • (↑(Real.cos ‖im q‖) + (Real.sin ‖im q‖ / ‖im q‖) • im q)) =
    exp ℝ q.re ^ 2 * ↑normSq (↑(Real.cos ‖im q‖) + (Real.sin ‖im q‖ / ‖im q‖) • im q)
rw [normSq_smul]
case e_a
q : ℍ
⊢ ↑normSq (↑(Real.cos ‖im q‖) + (Real.sin ‖im q‖ / ‖im q‖) • im q) = Real.cos ‖im q‖ ^ 2 + Real.sin ‖im q‖ ^ 2
q : ℍ
⊢ exp ℝ q.re ^ 2 * ↑normSq (↑(Real.cos ‖im q‖) + (Real.sin ‖im q‖ / ‖im q‖) • im q) =
    exp ℝ q.re ^ 2 * (Real.cos ‖im q‖ ^ 2 + Real.sin ‖im q‖ ^ 2)
congr 1
case e_a.inl
q : ℍ
hv : ‖im q‖ = 0
⊢ ↑normSq (↑(Real.cos ‖im q‖) + (Real.sin ‖im q‖ / ‖im q‖) • im q) = Real.cos ‖im q‖ ^ 2 + Real.sin ‖im q‖ ^ 2

case e_a.inr
q : ℍ
hv : ‖im q‖ ≠ 0
⊢ ↑normSq (↑(Real.cos ‖im q‖) + (Real.sin ‖im q‖ / ‖im q‖) • im q) = Real.cos ‖im q‖ ^ 2 + Real.sin ‖im q‖ ^ 2
case e_a
q : ℍ
⊢ ↑normSq (↑(Real.cos ‖im q‖) + (Real.sin ‖im q‖ / ‖im q‖) • im q) = Real.cos ‖im q‖ ^ 2 + Real.sin ‖im q‖ ^ 2
obtain hv | hv := eq_or_ne ‖q.im‖ 0
no goals
case e_a.inr
q : ℍ
hv : ‖im q‖ ≠ 0
⊢ ↑normSq (↑(Real.cos ‖im q‖) + (Real.sin ‖im q‖ / ‖im q‖) • im q) = Real.cos ‖im q‖ ^ 2 + Real.sin ‖im q‖ ^ 2
rw [normSq_add, normSq_smul, star_smul, coe_mul_eq_smul, smul_re, smul_re, star_re, im_re,
  smul_zero, smul_zero, MulZeroClass.mul_zero, add_zero, div_pow, normSq_coe,
  normSq_eq_norm_mul_self, ← sq, div_mul_cancel _ (pow_ne_zero _ hv)]
no goals
case e_a.inl
q : ℍ
hv : ‖im q‖ = 0
⊢ ↑normSq (↑(Real.cos ‖im q‖) + (Real.sin ‖im q‖ / ‖im q‖) • im q) = Real.cos ‖im q‖ ^ 2 + Real.sin ‖im q‖ ^ 2
simp [hv]
no goals
q : ℍ
⊢ exp ℝ q.re ^ 2 * (Real.cos ‖im q‖ ^ 2 + Real.sin ‖im q‖ ^ 2) = exp ℝ q.re ^ 2
rw [Real.cos_sq_add_sin_sq, mul_one]