awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
hqn : ‖q‖ ≠ 0
k : ℝ := (↑(2 * n + 1)! : ℝ)
inr inr₁ inr₂ inr₃ :
  (↑((↑(Int.negSucc 0 ^ n) : ℝ) * (‖q‖ * ‖q‖) ^ n) : ℍ) * q = (↑((↑(Int.negSucc 0 ^ n) : ℝ) * (‖q‖ * ‖q‖) ^ n) : ℍ) * q
⊢ HPow.hPow (α := ℍ) (-1) n * HPow.hPow (α := ℍ) (↑(‖q‖ * ‖q‖) : ℍ) n * q =
    (↑(HPow.hPow (α := ℝ) (-1) n * (‖q‖ * ‖q‖) ^ n) : ℍ) * q

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
hqn : ‖q‖ ≠ 0
k : ℝ := (↑(2 * n + 1)! : ℝ)
inr :
  (k⁻¹ * (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n))) • q =
    (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q
⊢ k⁻¹ • (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) • q = (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q

Tactic:
rw [smul_smul]

Premises used: smul_smul
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
hqn : ‖q‖ ≠ 0
k : ℝ := (↑(2 * n + 1)! : ℝ)
inr : k⁻¹ * (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) = HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖
⊢ (k⁻¹ * (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n))) • q =
    (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q

Tactic:
congr 1
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
hqn : ‖q‖ ≠ 0
k : ℝ := (↑(2 * n + 1)! : ℝ)
inr : k⁻¹ * (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) = HPow.hPow (α := ℝ) (-1) n * (‖q‖ ^ (2 * n) * k⁻¹)
⊢ k⁻¹ * (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) = HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖

Tactic:
simp_rw [pow_succ, mul_div_assoc, div_div_cancel_left' hqn]

Premises used: pow_succ, mul_div_assoc, div_div_cancel_left'
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
hqn : ‖q‖ ≠ 0
k : ℝ := (↑(2 * n + 1)! : ℝ)
⊢ k⁻¹ * (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) = HPow.hPow (α := ℝ) (-1) n * (‖q‖ ^ (2 * n) * k⁻¹)

Tactic:
ring
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / (↑(2 * n)! : ℝ)) c
hs : HasSum (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ)) s
⊢ HasSum (α := ℍ) (fun (a : ℕ) ↦ (↑(HPow.hPow (α := ℝ) (-1) a * ‖q‖ ^ (2 * a) / (↑(2 * a)! : ℝ)) : ℍ)) (↑c : ℍ)

Tactic:
replace hc := hasSum_coe.mpr hc
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
c s : ℝ
hs : HasSum (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ)) s
hc : HasSum (α := ℍ) (fun (a : ℕ) ↦ (↑(HPow.hPow (α := ℝ) (-1) a * ‖q‖ ^ (2 * a) / (↑(2 * a)! : ℝ)) : ℍ)) (↑c : ℍ)
⊢ HasSum (fun (z : ℕ) ↦ (HPow.hPow (α := ℝ) (-1) z * ‖q‖ ^ (2 * z + 1) / (↑(2 * z + 1)! : ℝ) / ‖q‖) • q) ((s / ‖q‖) • q)

Tactic:
replace hs := (hs.div_const ‖q‖).smul_const q
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
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)
⊢ HasSum (fun (n : ℕ) ↦ (expSeries ℝ ℍ n : (a : (i : Fin n) → ℍ) → ℍ) fun (x : Fin n) ↦ q) ((↑c : ℍ) + (s / ‖q‖) • q)

Tactic:
HasSum.even_add_odd ?_ ?_

Premises used: HasSum.even_add_odd
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
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)
refine_1 :
  HasSum (α := ℍ) (fun (k : ℕ) ↦ (expSeries ℝ ℍ (2 * k) : (a : (i : Fin (2 * k)) → ℍ) → ℍ) fun (x : Fin (2 * k)) ↦ q)
    (↑c : ℍ)
refine_2 :
  HasSum (fun (k : ℕ) ↦ (expSeries ℝ ℍ (2 * k + 1) : (a : (i : Fin (2 * k + 1)) → ℍ) → ℍ) fun (x : Fin (2 * k + 1)) ↦ q)
    ((s / ‖q‖) • q)
⊢ HasSum (fun (n : ℕ) ↦ (expSeries ℝ ℍ n : (a : (i : Fin n) → ℍ) → ℍ) fun (x : Fin n) ↦ q) ((↑c : ℍ) + (s / ‖q‖) • q)

Tactic:
refine HasSum.even_add_odd ?_ ?_

Premises used: HasSum.even_add_odd
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
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)
⊢ HasSum (α := ℍ) (fun (a : ℕ) ↦ (↑(HPow.hPow (α := ℝ) (-1) a * ‖q‖ ^ (2 * a) / (↑(2 * a)! : ℝ)) : ℍ)) (↑c : ℍ)

Tactic:
hc
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
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)
h :
  Eq (α := ℕ → ℍ) (fun (k : ℕ) ↦ (expSeries ℝ ℍ (2 * k) : (a : (i : Fin (2 * k)) → ℍ) → ℍ) fun (x : Fin (2 * k)) ↦ q)
    fun (a : ℕ) ↦ (↑(HPow.hPow (α := ℝ) (-1) a * ‖q‖ ^ (2 * a) / (↑(2 * a)! : ℝ)) : ℍ)
⊢ HasSum (α := ℍ) (fun (k : ℕ) ↦ (expSeries ℝ ℍ (2 * k) : (a : (i : Fin (2 * k)) → ℍ) → ℍ) fun (x : Fin (2 * k)) ↦ q)
    (↑c : ℍ)

Tactic:
convert! hc using 1
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
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)
h :
  ∀ (n : ℕ),
    Eq (α := ℍ) ((expSeries ℝ ℍ (2 * n) : (a : (i : Fin (2 * n)) → ℍ) → ℍ) fun (x : Fin (2 * n)) ↦ q)
      (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / (↑(2 * n)! : ℝ)) : ℍ)
⊢ Eq (α := ℕ → ℍ) (fun (k : ℕ) ↦ (expSeries ℝ ℍ (2 * k) : (a : (i : Fin (2 * k)) → ℍ) → ℍ) fun (x : Fin (2 * k)) ↦ q)
    fun (a : ℕ) ↦ (↑(HPow.hPow (α := ℝ) (-1) a * ‖q‖ ^ (2 * a) / (↑(2 * a)! : ℝ)) : ℍ)

Tactic:
ext n : 1
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
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 : ℕ
h h₁ :
  Eq (α := ℍ) (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / (↑(2 * n)! : ℝ)) : ℍ)
    (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / (↑(2 * n)! : ℝ)) : ℍ)
⊢ Eq (α := ℍ) ((expSeries ℝ ℍ (2 * n) : (a : (i : Fin (2 * n)) → ℍ) → ℍ) fun (x : Fin (2 * n)) ↦ q)
    (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / (↑(2 * n)! : ℝ)) : ℍ)

Tactic:
rw [expSeries_even_of_imaginary hq]

Premises used: Quaternion.expSeries_even_of_imaginary
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
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)
⊢ HasSum (fun (z : ℕ) ↦ (HPow.hPow (α := ℝ) (-1) z * ‖q‖ ^ (2 * z + 1) / (↑(2 * z + 1)! : ℝ) / ‖q‖) • q) ((s / ‖q‖) • q)

Tactic:
hs
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
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)
h :
  Eq (α := ℕ → ℍ)
    (fun (k : ℕ) ↦ (expSeries ℝ ℍ (2 * k + 1) : (a : (i : Fin (2 * k + 1)) → ℍ) → ℍ) fun (x : Fin (2 * k + 1)) ↦ q)
    fun (z : ℕ) ↦ (HPow.hPow (α := ℝ) (-1) z * ‖q‖ ^ (2 * z + 1) / (↑(2 * z + 1)! : ℝ) / ‖q‖) • q
⊢ HasSum (fun (k : ℕ) ↦ (expSeries ℝ ℍ (2 * k + 1) : (a : (i : Fin (2 * k + 1)) → ℍ) → ℍ) fun (x : Fin (2 * k + 1)) ↦ q)
    ((s / ‖q‖) • q)

Tactic:
convert! hs using 1
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
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)
h :
  ∀ (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
⊢ Eq (α := ℕ → ℍ)
    (fun (k : ℕ) ↦ (expSeries ℝ ℍ (2 * k + 1) : (a : (i : Fin (2 * k + 1)) → ℍ) → ℍ) fun (x : Fin (2 * k + 1)) ↦ q)
    fun (z : ℕ) ↦ (HPow.hPow (α := ℝ) (-1) z * ‖q‖ ^ (2 * z + 1) / (↑(2 * z + 1)! : ℝ) / ‖q‖) • q

Tactic:
ext n : 1
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
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 : ℕ
h 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
⊢ ((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

Tactic:
rw [expSeries_odd_of_imaginary hq]

Premises used: Quaternion.expSeries_odd_of_imaginary
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
rw :
  (fun (x : ℍ) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℝ) (↑n ! : ℝ)⁻¹ (x ^ n) : ℍ)) q =
    (↑(Real.cos ‖q‖) : ℍ) + (Real.sin ‖q‖ / ‖q‖) • q
⊢ exp q = (↑(Real.cos ‖q‖) : ℍ) + (Real.sin ‖q‖ / ‖q‖) • q

Tactic:
rw [exp_eq_tsum ℝ]

Premises used: Real, NormedSpace.exp_eq_tsum
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
⊢ (fun (x : ℍ) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℝ) (↑n ! : ℝ)⁻¹ (x ^ n) : ℍ)) q =
    (↑(Real.cos ‖q‖) : ℍ) + (Real.sin ‖q‖ / ‖q‖) • q

Tactic:
HasSum.tsum_eq ?_

Premises used: HasSum.tsum_eq
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
refine :
  HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (↑n ! : ℝ)⁻¹ (q ^ n)) ((↑(Real.cos ‖q‖) : ℍ) + (Real.sin ‖q‖ / ‖q‖) • q)
⊢ (fun (x : ℍ) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℝ) (↑n ! : ℝ)⁻¹ (x ^ n) : ℍ)) q =
    (↑(Real.cos ‖q‖) : ℍ) + (Real.sin ‖q‖ / ‖q‖) • q

Tactic:
refine HasSum.tsum_eq ?_

Premises used: HasSum.tsum_eq
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
simp_rw :
  HasSum (fun (n : ℕ) ↦ (expSeries ℝ ℍ n : (a : (i : Fin n) → ℍ) → ℍ) fun (x : Fin n) ↦ q)
    ((↑(Real.cos ‖q‖) : ℍ) + (Real.sin ‖q‖ / ‖q‖) • q)
⊢ HasSum (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (↑n ! : ℝ)⁻¹ (q ^ n)) ((↑(Real.cos ‖q‖) : ℍ) + (Real.sin ‖q‖ / ‖q‖) • q)

Tactic:
simp_rw [← expSeries_apply_eq]

Premises used: NormedSpace.expSeries_apply_eq
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
⊢ HasSum (fun (n : ℕ) ↦ (expSeries ℝ ℍ n : (a : (i : Fin n) → ℍ) → ℍ) fun (x : Fin n) ↦ q)
    ((↑(Real.cos ‖q‖) : ℍ) + (Real.sin ‖q‖ / ‖q‖) • q)

Tactic:
hasSum_expSeries_of_imaginary hq (Real.hasSum_cos _) (Real.hasSum_sin _)

Premises used: Real.hasSum_cos, Real.hasSum_sin, Quaternion.hasSum_expSeries_of_imaginary
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
⊢ HasSum (fun (n : ℕ) ↦ (expSeries ℝ ℍ n : (a : (i : Fin n) → ℍ) → ℍ) fun (x : Fin n) ↦ q)
    ((↑(Real.cos ‖q‖) : ℍ) + (Real.sin ‖q‖ / ‖q‖) • q)

Tactic:
exact hasSum_expSeries_of_imaginary hq (Real.hasSum_cos _) (Real.hasSum_sin _)

Premises used: Real.hasSum_cos, Real.hasSum_sin, Quaternion.hasSum_expSeries_of_imaginary
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
let : ∀ (this : NormedAlgebra ℚ ℍ), exp q = exp q.re • ((↑(Real.cos ‖q.im‖) : ℍ) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)
⊢ exp q = exp q.re • ((↑(Real.cos ‖q.im‖) : ℍ) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)

Tactic:
let +nondep : NormedAlgebra ℚ ℍ := .restrictScalars ℚ ℝ ℍ
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
this : NormedAlgebra ℚ ℍ
rw : Commute (↑q.re : ℍ) q.im
⊢ exp q = exp q.re • ((↑(Real.cos ‖q.im‖) : ℍ) + (Real.sin ‖q.im‖ / ‖q.im‖) • 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]

Premises used: Quaternion.re_add_im, Quaternion.exp_of_re_eq_zero, Quaternion.coe_mul_eq_smul, Quaternion.re_im, Quaternion.im, NormedSpace.exp_add_of_commute, Quaternion.exp_coe
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
this : NormedAlgebra ℚ ℍ
⊢ Commute (↑q.re : ℍ) q.im

Tactic:
Algebra.commutes q.re (_ : ℍ[ℝ])

Premises used: Quaternion.coe, SemiconjBy, QuaternionAlgebra.re, Commute, QuaternionAlgebra.coe, Algebra.commutes
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
this : NormedAlgebra ℚ ℍ
⊢ Commute (↑q.re : ℍ) q.im

Tactic:
exact Algebra.commutes q.re (_ : ℍ[ℝ])

Premises used: QuaternionAlgebra.re, Algebra.commutes
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
⊢ (exp q).re = exp q.re * Real.cos ‖q - (↑q.re : ℍ)‖

Tactic:
simp [exp_eq]

Premises used: Quaternion.exp_eq
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
⊢ (exp q).im = (exp q.re * (Real.sin ‖q.im‖ / ‖q.im‖)) • q.im

Tactic:
simp [exp_eq, smul_smul]

Premises used: smul_smul, Quaternion.exp_eq
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
rw 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)) : ℝ)
⊢ Eq (α := ℝ) ((normSq : (a : ℍ) → ℝ) (exp q) : ℝ)
    ((normSq : (a : ℍ) → ℝ) (exp q.re • ((↑(Real.cos ‖q.im‖) : ℍ) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)) : ℝ)

Tactic:
rw [exp_eq]

Premises used: Quaternion.exp_eq
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
rw 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) : ℝ)
⊢ (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) : ℝ)

Tactic:
rw [normSq_smul]

Premises used: Quaternion.normSq_smul
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
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
⊢ 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)

Tactic:
congr 1
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
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
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

Tactic:
obtain hv | hv := eq_or_ne ‖q.im‖ 0

Premises used: Norm.norm, eq_or_ne, Quaternion.im, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
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

Tactic:
simp [hv]
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
rw : HPow.hPow (β := ℕ) (exp q.re) 2 * 1 = HPow.hPow (β := ℕ) (exp q.re) 2
rw₁ rw₂ : HPow.hPow (β := ℕ) (exp q.re) 2 = 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

Tactic:
rw [Real.cos_sq_add_sin_sq, mul_one]

Premises used: Real.cos_sq_add_sin_sq, mul_one
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
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‖
rw₄ rw₅ : |exp q.re| = |exp q.re|
⊢ ‖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]

Premises used: NormedSpace.exp, Real.sqrt_sq_eq_abs, Quaternion.normSq_exp, Quaternion.inner_self, Real.norm_eq_abs, norm_eq_sqrt_real_inner
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Subsingleton A
a : A
⊢ spectralRadius 𝕜 a = 0

Tactic:
simp [spectralRadius]

Premises used: spectralRadius
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
h : Nontrivial A
⊢ spectralRadius.{u_1, u_2} 𝕜 (A := A) 0 = 0

Tactic:
simp [spectralRadius]

Premises used: spectralRadius
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
⊢ spectralRadius.{u_1, u_2} 𝕜 (A := A) 1 = 1

Tactic:
simp [spectralRadius]

Premises used: spectralRadius
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
k : 𝕜
h : spectralRadius 𝕜 a < (↑‖k‖₊ : ℝ≥0∞)
⊢ k ∈ ρ a

Tactic:
Classical.not_not.mp fun hn => h.not_ge <| le_iSup₂ (α := ℝ≥0∞) k hn

Premises used: Classical.not_not, le_iSup₂, Iff.mp, LT.lt.not_ge
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
n : ℕ
hn : n ≠ 0
simp : LE.le (α := ℝ≥0∞) (⨆ i ∈ σ a, (↑‖i‖₊ : ℝ≥0∞) ^ n) (⨆ k ∈ σ (a ^ n), (↑‖k‖₊ : ℝ≥0∞))
⊢ spectralRadius 𝕜 a ^ n ≤ spectralRadius 𝕜 (a ^ n)

Tactic:
simp only [spectralRadius, ENNReal.iSup₂_pow_of_ne_zero _ hn]

Premises used: spectralRadius, ENNReal.iSup₂_pow_of_ne_zero
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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∞))

Tactic:
iSup₂_le fun x hx ↦ ?_

Premises used: iSup₂_le
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
n : ℕ
hn : n ≠ 0
refine : ∀ (x : 𝕜) (hx : x ∈ σ a), (↑‖x‖₊ : ℝ≥0∞) ^ n ≤ ⨆ k ∈ σ (a ^ n), (↑‖k‖₊ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (⨆ i ∈ σ a, (↑‖i‖₊ : ℝ≥0∞) ^ n) (⨆ k ∈ σ (a ^ n), (↑‖k‖₊ : ℝ≥0∞))

Tactic:
refine iSup₂_le fun x hx ↦ ?_

Premises used: iSup₂_le
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
apply : (↑‖x‖₊ : ℝ≥0∞) ^ n ≤ (↑‖x ^ n‖₊ : ℝ≥0∞)
⊢ (↑‖x‖₊ : ℝ≥0∞) ^ n ≤ ⨆ k ∈ σ (a ^ n), (↑‖k‖₊ : ℝ≥0∞)

Tactic:
apply le_iSup₂_of_le (x ^ n) (spectrum.pow_mem_pow a n hx)

Premises used: spectrum.pow_mem_pow, HPow.hPow, le_iSup₂_of_le
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 ≤ (↑‖x ^ n‖₊ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
succ : ∀ (n : ℕ), spectralRadius 𝕜 a ^ (n + 1) ≤ spectralRadius 𝕜 (a ^ (n + 1))
⊢ spectralRadius 𝕜 a ^ n ≤ spectralRadius 𝕜 (a ^ n)

Tactic:
cases n
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
a : A
⊢ HPow.hPow (β := ℕ) (spectralRadius 𝕜 a) 0 ≤ spectralRadius 𝕜 (HPow.hPow (β := ℕ) a 0)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : ℕ
⊢ n + 1 ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 + 1) ≤ spectralRadius 𝕜 (a ^ (n + 1))

Tactic:
exact spectralRadius_pow_le a _ (by simp)

Premises used: spectrum.spectralRadius_pow_le
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (r : 𝕜) ↦ HSub.hSub (α := A) ((↑ₐ : (a : 𝕜) → A) r : A) a

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ a)

Tactic:
(isOpen_resolventSet a).isClosed_compl

Premises used: spectrum, spectrum.isOpen_resolventSet, IsOpen.isClosed_compl
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
k : 𝕜
h : ‖a‖ * norm.{u_2} (E := A) 1 < ‖k‖
rw : IsUnit (HSMul.hSMul (β := A) k 1 - a)
⊢ k ∈ ρ a

Tactic:
rw [resolventSet, Set.mem_setOf_eq, Algebra.algebraMap_eq_smul_one]

Premises used: Set.mem_setOf_eq, Algebra.algebraMap_eq_smul_one, resolventSet
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
k : 𝕜
h : ‖a‖ * norm.{u_2} (E := A) 1 < ‖k‖
⊢ Nontrivial A

Tactic:
nontriviality A