awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (α := ℍ) (fun (a : ℕ) ↦ (↑(HPow.hPow (α := ℝ) (-1) a * ‖q‖ ^ (2 * a) / (↑(2 * a)! : ℝ)) : ℍ)) (↑c : ℍ)
hs :
  HasSum (fun (z : ℕ) ↦ (HPow.hPow (α := ℝ) (-1) z * ‖q‖ ^ (2 * z + 1) / (↑(2 * z + 1)! : ℝ) / ‖q‖) • q) ((s / ‖q‖) • q)
n : ℕ
⊢ ((expSeries ℝ ℍ (2 * n + 1) : (a : (i : Fin (2 * n + 1)) → ℍ) → ℍ) fun (x : Fin (2 * n + 1)) ↦ q) =
    (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / ‖q‖) • q
have h : (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / ‖q‖) • q =
  (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / ‖q‖) • q
Tactic: rw [expSeries_odd_of_imaginary hq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
hq : q.re = 0
⊢ exp q = (↑(Real.cos ‖q‖) : ℍ) + (Real.sin ‖q‖ / ‖q‖) • q
have rw : (fun (x : ℍ) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℝ) (↑n ! : ℝ)⁻¹ (x ^ n) : ℍ)) q =
  (↑(Real.cos ‖q‖) : ℍ) + (Real.sin ‖q‖ / ‖q‖) • q
Tactic: rw [exp_eq_tsum ℝ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
hq : q.re = 0
⊢ (fun (x : ℍ) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℝ) (↑n ! : ℝ)⁻¹ (x ^ n) : ℍ)) q =
    (↑(Real.cos ‖q‖) : ℍ) + (Real.sin ‖q‖ / ‖q‖) • q
have refine : HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (↑n ! : ℝ)⁻¹ (q ^ n)) ((↑(Real.cos ‖q‖) : ℍ) + (Real.sin ‖q‖ / ‖q‖) • q)
Tactic: refine HasSum.tsum_eq ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
hq : q.re = 0
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (↑n ! : ℝ)⁻¹ (q ^ n)) ((↑(Real.cos ‖q‖) : ℍ) + (Real.sin ‖q‖ / ‖q‖) • q)
have simp_rw : HasSum (fun (n : ℕ) ↦ (expSeries ℝ ℍ n : (a : (i : Fin n) → ℍ) → ℍ) fun (x : Fin n) ↦ q)
  ((↑(Real.cos ‖q‖) : ℍ) + (Real.sin ‖q‖ / ‖q‖) • q)
Tactic: simp_rw [← expSeries_apply_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
⊢ exp q = exp q.re • ((↑(Real.cos ‖q.im‖) : ℍ) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)
have let : ∀ (this : NormedAlgebra ℚ ℍ), exp q = exp q.re • ((↑(Real.cos ‖q.im‖) : ℍ) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)
Tactic: let +nondep : NormedAlgebra ℚ ℍ := .restrictScalars ℚ ℝ ℍ
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
this : NormedAlgebra ℚ ℍ
⊢ exp q = exp q.re • ((↑(Real.cos ‖q.im‖) : ℍ) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)
have rw : Commute (↑q.re : ℍ) q.im
Tactic: rw [← exp_of_re_eq_zero q.im q.re_im, ← coe_mul_eq_smul, ← exp_coe, ← exp_add_of_commute,
    re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
⊢ Eq (α := ℝ) ((normSq : (a : ℍ) → ℝ) (exp q) : ℝ)
    ((normSq : (a : ℍ) → ℝ) (exp q.re • ((↑(Real.cos ‖q.im‖) : ℍ) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)) : ℝ)
have rw : Eq (α := ℝ) ((normSq : (a : ℍ) → ℝ) (exp q.re • ((↑(Real.cos ‖q.im‖) : ℍ) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)) : ℝ)
  ((normSq : (a : ℍ) → ℝ) (exp q.re • ((↑(Real.cos ‖q.im‖) : ℍ) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)) : ℝ)
Tactic: rw [exp_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
⊢ (normSq : (a : ℍ) → ℝ) (exp q.re • ((↑(Real.cos ‖q.im‖) : ℍ) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)) =
    HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) (exp q.re) 2)
      ((normSq : (a : ℍ) → ℝ) ((↑(Real.cos ‖q.im‖) : ℍ) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) : ℝ)
have rw : HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) (exp q.re) 2)
    ((normSq : (a : ℍ) → ℝ) ((↑(Real.cos ‖q.im‖) : ℍ) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) : ℝ) =
  HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) (exp q.re) 2)
    ((normSq : (a : ℍ) → ℝ) ((↑(Real.cos ‖q.im‖) : ℍ) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) : ℝ)
Tactic: rw [normSq_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
⊢ HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) (exp q.re) 2)
      ((normSq : (a : ℍ) → ℝ) ((↑(Real.cos ‖q.im‖) : ℍ) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) : ℝ) =
    HPow.hPow (β := ℕ) (exp q.re) 2 * (HPow.hPow (β := ℕ) (Real.cos ‖q.im‖) 2 + HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2)
have e_a : (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
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
⊢ (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 : ∀ (hv : ‖q.im‖ = 0),
  (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
Tactic: obtain hv | hv := eq_or_ne ‖q.im‖ 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
e_a :
  ∀ (hv : ‖q.im‖ = 0),
    (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
⊢ (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₁ : ∀ (hv : ‖q.im‖ ≠ 0),
  (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
Tactic: obtain hv | hv := eq_or_ne ‖q.im‖ 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
hv : ‖q.im‖ ≠ 0
⊢ (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 : 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
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)]
-- 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
⊢ (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₁ : 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
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)]
-- 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
⊢ (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₂ : 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
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)]
-- 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
⊢ (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₃ : 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
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)]
-- 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
⊢ (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₄ : 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
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)]
-- 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
⊢ (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₅ : 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
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)]
-- 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
⊢ (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₆ : 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
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)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
⊢ HPow.hPow (β := ℕ) (exp q.re) 2 * (HPow.hPow (β := ℕ) (Real.cos ‖q.im‖) 2 + HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2) =
    HPow.hPow (β := ℕ) (exp q.re) 2
have rw : HPow.hPow (β := ℕ) (exp q.re) 2 * 1 = HPow.hPow (β := ℕ) (exp q.re) 2
Tactic: rw [Real.cos_sq_add_sin_sq, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
rw : HPow.hPow (β := ℕ) (exp q.re) 2 * 1 = HPow.hPow (β := ℕ) (exp q.re) 2
⊢ HPow.hPow (β := ℕ) (exp q.re) 2 * (HPow.hPow (β := ℕ) (Real.cos ‖q.im‖) 2 + HPow.hPow (β := ℕ) (Real.sin ‖q.im‖) 2) =
    HPow.hPow (β := ℕ) (exp q.re) 2
have rw₁ : HPow.hPow (β := ℕ) (exp q.re) 2 = HPow.hPow (β := ℕ) (exp q.re) 2
Tactic: rw [Real.cos_sq_add_sin_sq, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
⊢ ‖exp q‖ = ‖exp q.re‖
have rw : √(inner ℝ (exp q) (exp q)) = ‖exp q.re‖
Tactic: rw [norm_eq_sqrt_real_inner (exp q), inner_self, normSq_exp, Real.sqrt_sq_eq_abs,
    Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
rw : √(inner ℝ (exp q) (exp q)) = ‖exp q.re‖
⊢ ‖exp q‖ = ‖exp q.re‖
have rw₁ : √((normSq : (a : ℍ) → ℝ) (exp q)) = ‖exp q.re‖
Tactic: rw [norm_eq_sqrt_real_inner (exp q), inner_self, normSq_exp, Real.sqrt_sq_eq_abs,
    Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
rw : √(inner ℝ (exp q) (exp q)) = ‖exp q.re‖
rw₁ : √((normSq : (a : ℍ) → ℝ) (exp q)) = ‖exp q.re‖
⊢ ‖exp q‖ = ‖exp q.re‖
have rw₂ : √(HPow.hPow (β := ℕ) (exp q.re) 2) = ‖exp q.re‖
Tactic: rw [norm_eq_sqrt_real_inner (exp q), inner_self, normSq_exp, Real.sqrt_sq_eq_abs,
    Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
rw : √(inner ℝ (exp q) (exp q)) = ‖exp q.re‖
rw₁ : √((normSq : (a : ℍ) → ℝ) (exp q)) = ‖exp q.re‖
rw₂ : √(HPow.hPow (β := ℕ) (exp q.re) 2) = ‖exp q.re‖
⊢ ‖exp q‖ = ‖exp q.re‖
have rw₃ : |exp q.re| = ‖exp q.re‖
Tactic: rw [norm_eq_sqrt_real_inner (exp q), inner_self, normSq_exp, Real.sqrt_sq_eq_abs,
    Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
rw : √(inner ℝ (exp q) (exp q)) = ‖exp q.re‖
rw₁ : √((normSq : (a : ℍ) → ℝ) (exp q)) = ‖exp q.re‖
rw₂ : √(HPow.hPow (β := ℕ) (exp q.re) 2) = ‖exp q.re‖
rw₃ : |exp q.re| = ‖exp q.re‖
⊢ ‖exp q‖ = ‖exp q.re‖
have rw₄ : |exp q.re| = |exp q.re|
Tactic: rw [norm_eq_sqrt_real_inner (exp q), inner_self, normSq_exp, Real.sqrt_sq_eq_abs,
    Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
⊢ spectralRadius.{u_1, u_2} 𝕜 (A := A) 0 = 0
have a : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
n : ℕ
hn : n ≠ 0
⊢ spectralRadius 𝕜 a ^ n ≤ spectralRadius 𝕜 (a ^ n)
have simp : LE.le (α := ℝ≥0∞) (⨆ i ∈ σ a, (↑‖i‖₊ : ℝ≥0∞) ^ n) (⨆ k ∈ σ (a ^ n), (↑‖k‖₊ : ℝ≥0∞))
Tactic: simp only [spectralRadius, ENNReal.iSup₂_pow_of_ne_zero _ hn]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
n : ℕ
hn : n ≠ 0
⊢ LE.le (α := ℝ≥0∞) (⨆ i ∈ σ a, (↑‖i‖₊ : ℝ≥0∞) ^ n) (⨆ k ∈ σ (a ^ n), (↑‖k‖₊ : ℝ≥0∞))
have refine : ∀ (x : 𝕜) (hx : x ∈ σ a), (↑‖x‖₊ : ℝ≥0∞) ^ n ≤ ⨆ k ∈ σ (a ^ n), (↑‖k‖₊ : ℝ≥0∞)
Tactic: refine iSup₂_le fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
n : ℕ
hn : n ≠ 0
x : 𝕜
hx : x ∈ σ a
⊢ (↑‖x‖₊ : ℝ≥0∞) ^ n ≤ ⨆ k ∈ σ (a ^ n), (↑‖k‖₊ : ℝ≥0∞)
have apply : (↑‖x‖₊ : ℝ≥0∞) ^ n ≤ (↑‖x ^ n‖₊ : ℝ≥0∞)
Tactic: apply le_iSup₂_of_le (x ^ n) (spectrum.pow_mem_pow a n hx)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
a : A
n : ℕ
⊢ spectralRadius 𝕜 a ^ n ≤ spectralRadius 𝕜 (a ^ n)
have zero : HPow.hPow (β := ℕ) (spectralRadius 𝕜 a) 0 ≤ spectralRadius 𝕜 (HPow.hPow (β := ℕ) a 0)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
a : A
n : ℕ
zero : HPow.hPow (β := ℕ) (spectralRadius 𝕜 a) 0 ≤ spectralRadius 𝕜 (HPow.hPow (β := ℕ) a 0)
⊢ spectralRadius 𝕜 a ^ n ≤ spectralRadius 𝕜 (a ^ n)
have succ : ∀ (n : ℕ), spectralRadius 𝕜 a ^ (n + 1) ≤ spectralRadius 𝕜 (a ^ (n + 1))
Tactic: cases n
Cleared hypotheses: n