-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
hv : ‖q.im‖ ≠ 0
e_a :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℍ) → ℝ) (↑(Real.cos ‖q.im‖) : ℍ) : ℝ)
        ((normSq : (a : ℍ) → ℝ) ((Real.sin ‖q.im‖ / ‖q.im‖) • q.im) : ℝ) +
      2 * ((↑(Real.cos ‖q.im‖) : ℍ) * star ((Real.sin ‖q.im‖ / ‖q.im‖) • q.im)).re =
    HPow.hPow (β := ℕ) (Real.cos ‖q.im‖) 2 + HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2
e_a₁ :
  HAdd.hAdd (α := ℝ) ((normSq : (a : ℍ) → ℝ) (↑(Real.cos ‖q.im‖) : ℍ) : ℝ)
        (HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) (Real.sin ‖q.im‖ / ‖q.im‖) 2) ((normSq : (a : ℍ) → ℝ) q.im : ℝ)) +
      2 * ((↑(Real.cos ‖q.im‖) : ℍ) * star ((Real.sin ‖q.im‖ / ‖q.im‖) • q.im)).re =
    HPow.hPow (β := ℕ) (Real.cos ‖q.im‖) 2 + HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2
e_a₂ :
  HAdd.hAdd (α := ℝ) ((normSq : (a : ℍ) → ℝ) (↑(Real.cos ‖q.im‖) : ℍ) : ℝ)
        (HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) (Real.sin ‖q.im‖ / ‖q.im‖) 2) ((normSq : (a : ℍ) → ℝ) q.im : ℝ)) +
      2 * ((↑(Real.cos ‖q.im‖) : ℍ) * (Real.sin ‖q.im‖ / ‖q.im‖) • star q.im).re =
    HPow.hPow (β := ℕ) (Real.cos ‖q.im‖) 2 + HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2
e_a₃ :
  HAdd.hAdd (α := ℝ) ((normSq : (a : ℍ) → ℝ) (↑(Real.cos ‖q.im‖) : ℍ) : ℝ)
        (HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) (Real.sin ‖q.im‖ / ‖q.im‖) 2) ((normSq : (a : ℍ) → ℝ) q.im : ℝ)) +
      2 * (Real.cos ‖q.im‖ • (Real.sin ‖q.im‖ / ‖q.im‖) • star q.im).re =
    HPow.hPow (β := ℕ) (Real.cos ‖q.im‖) 2 + HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2
e_a₄ :
  HAdd.hAdd (α := ℝ) ((normSq : (a : ℍ) → ℝ) (↑(Real.cos ‖q.im‖) : ℍ) : ℝ)
        (HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) (Real.sin ‖q.im‖ / ‖q.im‖) 2) ((normSq : (a : ℍ) → ℝ) q.im : ℝ)) +
      2 * Real.cos ‖q.im‖ • ((Real.sin ‖q.im‖ / ‖q.im‖) • star q.im).re =
    HPow.hPow (β := ℕ) (Real.cos ‖q.im‖) 2 + HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2
e_a₅ :
  HAdd.hAdd (α := ℝ) ((normSq : (a : ℍ) → ℝ) (↑(Real.cos ‖q.im‖) : ℍ) : ℝ)
        (HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) (Real.sin ‖q.im‖ / ‖q.im‖) 2) ((normSq : (a : ℍ) → ℝ) q.im : ℝ)) +
      2 * Real.cos ‖q.im‖ • (Real.sin ‖q.im‖ / ‖q.im‖) • (star q.im).re =
    HPow.hPow (β := ℕ) (Real.cos ‖q.im‖) 2 + HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2
e_a₆ :
  HAdd.hAdd (α := ℝ) ((normSq : (a : ℍ) → ℝ) (↑(Real.cos ‖q.im‖) : ℍ) : ℝ)
        (HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) (Real.sin ‖q.im‖ / ‖q.im‖) 2) ((normSq : (a : ℍ) → ℝ) q.im : ℝ)) +
      2 * Real.cos ‖q.im‖ • (Real.sin ‖q.im‖ / ‖q.im‖) • q.im.re =
    HPow.hPow (β := ℕ) (Real.cos ‖q.im‖) 2 + HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2
e_a₇ :
  HAdd.hAdd (α := ℝ) ((normSq : (a : ℍ) → ℝ) (↑(Real.cos ‖q.im‖) : ℍ) : ℝ)
        (HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) (Real.sin ‖q.im‖ / ‖q.im‖) 2) ((normSq : (a : ℍ) → ℝ) q.im : ℝ)) +
      2 * Real.cos ‖q.im‖ • HSMul.hSMul (β := ℝ) (Real.sin ‖q.im‖ / ‖q.im‖) 0 =
    HPow.hPow (β := ℕ) (Real.cos ‖q.im‖) 2 + HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2
e_a₈ :
  HAdd.hAdd (α := ℝ) ((normSq : (a : ℍ) → ℝ) (↑(Real.cos ‖q.im‖) : ℍ) : ℝ)
        (HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) (Real.sin ‖q.im‖ / ‖q.im‖) 2) ((normSq : (a : ℍ) → ℝ) q.im : ℝ)) +
      2 * HSMul.hSMul (β := ℝ) (Real.cos ‖q.im‖) 0 =
    HPow.hPow (β := ℕ) (Real.cos ‖q.im‖) 2 + HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2
e_a₉ :
  HAdd.hAdd (α := ℝ) ((normSq : (a : ℍ) → ℝ) (↑(Real.cos ‖q.im‖) : ℍ) : ℝ)
        (HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) (Real.sin ‖q.im‖ / ‖q.im‖) 2) ((normSq : (a : ℍ) → ℝ) q.im : ℝ)) +
      HMul.hMul (α := ℝ) 2 0 =
    HPow.hPow (β := ℕ) (Real.cos ‖q.im‖) 2 + HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2
e_a₁₀ :
  HAdd.hAdd (α := ℝ) ((normSq : (a : ℍ) → ℝ) (↑(Real.cos ‖q.im‖) : ℍ) : ℝ)
        (HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) (Real.sin ‖q.im‖ / ‖q.im‖) 2) ((normSq : (a : ℍ) → ℝ) q.im : ℝ)) +
      0 =
    HPow.hPow (β := ℕ) (Real.cos ‖q.im‖) 2 + HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2
e_a₁₁ :
  HAdd.hAdd (α := ℝ) ((normSq : (a : ℍ) → ℝ) (↑(Real.cos ‖q.im‖) : ℍ) : ℝ)
      (HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) (Real.sin ‖q.im‖ / ‖q.im‖) 2) ((normSq : (a : ℍ) → ℝ) q.im : ℝ)) =
    HPow.hPow (β := ℕ) (Real.cos ‖q.im‖) 2 + HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2
e_a₁₂ :
  HAdd.hAdd (α := ℝ) ((normSq : (a : ℍ) → ℝ) (↑(Real.cos ‖q.im‖) : ℍ) : ℝ)
      (HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2 / HPow.hPow (β := ℕ) ‖q.im‖ 2)
        ((normSq : (a : ℍ) → ℝ) q.im : ℝ)) =
    HPow.hPow (β := ℕ) (Real.cos ‖q.im‖) 2 + HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2
⊢ (normSq : (a : ℍ) → ℝ) ((↑(Real.cos ‖q.im‖) : ℍ) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) =
    HPow.hPow (β := ℕ) (Real.cos ‖q.im‖) 2 + HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2
have e_a₁₃ : HPow.hPow (β := ℕ) (Real.cos ‖q.im‖) 2 +
    HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2 / HPow.hPow (β := ℕ) ‖q.im‖ 2)
      ((normSq : (a : ℍ) → ℝ) q.im : ℝ) =
  HPow.hPow (β := ℕ) (Real.cos ‖q.im‖) 2 + HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2
Tactic: rw [normSq_add, normSq_smul, star_smul, coe_mul_eq_smul, re_smul, re_smul, re_star, re_im,
        smul_zero, smul_zero, mul_zero, add_zero, div_pow, normSq_coe,
        normSq_eq_norm_mul_self, ← sq, div_mul_cancel₀ _ (pow_ne_zero _ hv)]