awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NormedCommRing 𝔸
inst_3 : NormedAlgebra ℚ 𝔸
inst_4 : CompleteSpace 𝔸
A : Matrix m m 𝔸
n : ℕ
this : IsUnit (exp A).det
inr : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) A) = (HPow.hPow (β := ℤ) (exp A) (↑n : ℤ))⁻¹
inr₁ : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) A) = (exp A ^ n)⁻¹
inr₂ : exp (-HSMul.hSMul (α := ℤ) (↑n : ℤ) A) = (exp A ^ n)⁻¹
⊢ exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) A) = HPow.hPow (β := ℤ) (exp A) (-(↑n : ℤ))
have inr₃ : (exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) A))⁻¹ = (exp A ^ n)⁻¹
Tactic: rw [Matrix.zpow_neg this, zpow_natCast, neg_smul, exp_neg, natCast_zsmul, exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NormedCommRing 𝔸
inst_3 : NormedAlgebra ℚ 𝔸
inst_4 : CompleteSpace 𝔸
A : Matrix m m 𝔸
n : ℕ
this : IsUnit (exp A).det
inr : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) A) = (HPow.hPow (β := ℤ) (exp A) (↑n : ℤ))⁻¹
inr₁ : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) A) = (exp A ^ n)⁻¹
inr₂ : exp (-HSMul.hSMul (α := ℤ) (↑n : ℤ) A) = (exp A ^ n)⁻¹
inr₃ : (exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) A))⁻¹ = (exp A ^ n)⁻¹
⊢ exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) A) = HPow.hPow (β := ℤ) (exp A) (-(↑n : ℤ))
have inr₄ : (exp (n • A))⁻¹ = (exp A ^ n)⁻¹
Tactic: rw [Matrix.zpow_neg this, zpow_natCast, neg_smul, exp_neg, natCast_zsmul, exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NormedCommRing 𝔸
inst_3 : NormedAlgebra ℚ 𝔸
inst_4 : CompleteSpace 𝔸
A : Matrix m m 𝔸
n : ℕ
this : IsUnit (exp A).det
inr : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) A) = (HPow.hPow (β := ℤ) (exp A) (↑n : ℤ))⁻¹
inr₁ : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) A) = (exp A ^ n)⁻¹
inr₂ : exp (-HSMul.hSMul (α := ℤ) (↑n : ℤ) A) = (exp A ^ n)⁻¹
inr₃ : (exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) A))⁻¹ = (exp A ^ n)⁻¹
inr₄ : (exp (n • A))⁻¹ = (exp A ^ n)⁻¹
⊢ exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) A) = HPow.hPow (β := ℤ) (exp A) (-(↑n : ℤ))
have inr₅ : (exp A ^ n)⁻¹ = (exp A ^ n)⁻¹
Tactic: rw [Matrix.zpow_neg this, zpow_natCast, neg_smul, exp_neg, natCast_zsmul, exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
hq : q.re = 0
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)! : ℝ)) : ℍ)
have rw : HSMul.hSMul (α := ℝ) (↑(2 * n)! : ℝ)⁻¹ (q ^ (2 * n)) =
  (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / (↑(2 * n)! : ℝ)) : ℍ)
Tactic: rw [expSeries_apply_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (hypothesis)
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
⊢ HSMul.hSMul (α := ℝ) (↑(2 * n)! : ℝ)⁻¹ (q ^ (2 * n)) =
    (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / (↑(2 * n)! : ℝ)) : ℍ)
have hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
Tactic: have hq2 : q ^ 2 = -normSq q := sq_eq_neg_normSq.mpr hq
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
⊢ k⁻¹ • q ^ (2 * n) = k⁻¹ • HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n
have rw : k⁻¹ • HPow.hPow (β := ℕ) q 2 ^ n = k⁻¹ • HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n
Tactic: rw [pow_mul, hq2]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
rw : k⁻¹ • HPow.hPow (β := ℕ) q 2 ^ n = k⁻¹ • HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n
⊢ k⁻¹ • q ^ (2 * n) = k⁻¹ • HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n
have rw₁ : k⁻¹ • HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n =
  k⁻¹ • HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n
Tactic: rw [pow_mul, hq2]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
⊢ HSMul.hSMul (α := ℝ) (↑(2 * n)! : ℝ)⁻¹ (q ^ (2 * n)) =
    (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / (↑(2 * n)! : ℝ)) : ℍ)
have calc_1 : k⁻¹ • HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n =
  HSMul.hSMul (β := ℍ) k⁻¹ (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) : ℍ)
Tactic: calc
    k⁻¹ • q ^ (2 * n) = k⁻¹ • (-normSq q) ^ n := by rw [pow_mul, hq2]
    _ = k⁻¹ • ↑((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n)) := ?_
    _ = ↑((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n) / k) := ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
calc_1 :
  k⁻¹ • HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n =
    HSMul.hSMul (β := ℍ) k⁻¹ (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) : ℍ)
⊢ HSMul.hSMul (α := ℝ) (↑(2 * n)! : ℝ)⁻¹ (q ^ (2 * n)) =
    (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / (↑(2 * n)! : ℝ)) : ℍ)
have calc_2 : HSMul.hSMul (β := ℍ) k⁻¹ (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) : ℍ) =
  (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / k) : ℍ)
Tactic: calc
    k⁻¹ • q ^ (2 * n) = k⁻¹ • (-normSq q) ^ n := by rw [pow_mul, hq2]
    _ = k⁻¹ • ↑((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n)) := ?_
    _ = ↑((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n) / k) := ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
⊢ k⁻¹ • HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n =
    HSMul.hSMul (β := ℍ) k⁻¹ (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) : ℍ)
have calc_1 : HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n = (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) : ℍ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
⊢ HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n = (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) : ℍ)
have calc_1 : HPow.hPow (α := ℍ) (-1) n * HPow.hPow (α := ℍ) (↑(‖q‖ * ‖q‖) : ℍ) n =
  (↑(HPow.hPow (α := ℝ) (-1) n * (‖q‖ * ‖q‖) ^ n) : ℍ)
Tactic: rw [neg_pow, normSq_eq_norm_mul_self, pow_mul, sq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
⊢ HPow.hPow (α := ℍ) (-1) n * HPow.hPow (α := ℍ) (↑(‖q‖ * ‖q‖) : ℍ) n =
    (↑(HPow.hPow (α := ℝ) (-1) n * (‖q‖ * ‖q‖) ^ n) : ℍ)
have calc_1 : HPow.hPow (α := ℍ) (-1) n * HMul.hMul (α := ℍ) (↑‖q‖ : ℍ) (↑‖q‖ : ℍ) ^ n =
  HPow.hPow (α := ℍ) (-1) n * HMul.hMul (α := ℍ) (↑‖q‖ : ℍ) (↑‖q‖ : ℍ) ^ n
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
⊢ HSMul.hSMul (β := ℍ) k⁻¹ (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) : ℍ) =
    (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / k) : ℍ)
have calc_2 : HMul.hMul (α := ℍ) (↑k⁻¹ : ℍ) (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) : ℍ) =
  (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) * k⁻¹) : ℍ)
Tactic: rw [← coe_mul_eq_smul, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
⊢ HMul.hMul (α := ℍ) (↑k⁻¹ : ℍ) (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) : ℍ) =
    (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) * k⁻¹) : ℍ)
have calc_2 : Eq (α := ℍ) (↑(k⁻¹ * ((↑(Int.negSucc 0 ^ n) : ℝ) * ‖q‖ ^ (2 * n))) : ℍ)
  (↑((↑(Int.negSucc 0 ^ n) : ℝ) * ‖q‖ ^ (2 * n) * k⁻¹) : ℍ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
hq : q.re = 0
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 rw : HSMul.hSMul (α := ℝ) (↑(2 * n + 1)! : ℝ)⁻¹ (q ^ (2 * n + 1)) =
  (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / ‖q‖) • q
Tactic: rw [expSeries_apply_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
⊢ HSMul.hSMul (α := ℝ) (↑(2 * n + 1)! : ℝ)⁻¹ (q ^ (2 * n + 1)) =
    (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / ‖q‖) • q
have inl : ∀ (hq : Eq (α := ℝ) (QuaternionAlgebra.re (a := -1) (b := 0) (c := -1) 0) 0),
  HSMul.hSMul (α := ℝ) (↑(2 * n + 1)! : ℝ)⁻¹ (HPow.hPow (α := ℍ) 0 (2 * n + 1)) =
    HSMul.hSMul (β := ℍ)
      (HPow.hPow (α := ℝ) (-1) n * norm (E := ℍ) 0 ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / norm (E := ℍ) 0) 0
Tactic: obtain rfl | hq0 := eq_or_ne q 0
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
inl :
  ∀ (hq : Eq (α := ℝ) (QuaternionAlgebra.re (a := -1) (b := 0) (c := -1) 0) 0),
    HSMul.hSMul (α := ℝ) (↑(2 * n + 1)! : ℝ)⁻¹ (HPow.hPow (α := ℍ) 0 (2 * n + 1)) =
      HSMul.hSMul (β := ℍ)
        (HPow.hPow (α := ℝ) (-1) n * norm (E := ℍ) 0 ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / norm (E := ℍ) 0) 0
⊢ HSMul.hSMul (α := ℝ) (↑(2 * n + 1)! : ℝ)⁻¹ (q ^ (2 * n + 1)) =
    (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / ‖q‖) • q
have inr : ∀ (hq0 : q ≠ 0),
  HSMul.hSMul (α := ℝ) (↑(2 * n + 1)! : ℝ)⁻¹ (q ^ (2 * n + 1)) =
    (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / ‖q‖) • q
Tactic: obtain rfl | hq0 := eq_or_ne q 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (hypothesis)
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
⊢ HSMul.hSMul (α := ℝ) (↑(2 * n + 1)! : ℝ)⁻¹ (q ^ (2 * n + 1)) =
    (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / ‖q‖) • q
have hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
Tactic: have hq2 : q ^ 2 = -normSq q := sq_eq_neg_normSq.mpr hq
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (hypothesis)
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
⊢ HSMul.hSMul (α := ℝ) (↑(2 * n + 1)! : ℝ)⁻¹ (q ^ (2 * n + 1)) =
    (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / ‖q‖) • q
have hqn : ‖q‖ ≠ 0
Tactic: have hqn := norm_ne_zero_iff.mpr hq0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
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⁻¹ • q ^ (2 * n + 1) = k⁻¹ • (HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q)
have rw : k⁻¹ • (q ^ (2 * n) * q) = k⁻¹ • (HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q)
Tactic: rw [pow_succ, pow_mul, hq2]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
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)! : ℝ)
rw : k⁻¹ • (q ^ (2 * n) * q) = k⁻¹ • (HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q)
⊢ k⁻¹ • q ^ (2 * n + 1) = k⁻¹ • (HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q)
have rw₁ : k⁻¹ • (HPow.hPow (β := ℕ) q 2 ^ n * q) = k⁻¹ • (HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q)
Tactic: rw [pow_succ, pow_mul, hq2]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
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)! : ℝ)
rw : k⁻¹ • (q ^ (2 * n) * q) = k⁻¹ • (HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q)
rw₁ : k⁻¹ • (HPow.hPow (β := ℕ) q 2 ^ n * q) = k⁻¹ • (HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q)
⊢ k⁻¹ • q ^ (2 * n + 1) = k⁻¹ • (HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q)
have rw₂ : k⁻¹ • (HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q) =
  k⁻¹ • (HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q)
Tactic: rw [pow_succ, pow_mul, hq2]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
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)! : ℝ)
⊢ HSMul.hSMul (α := ℝ) (↑(2 * n + 1)! : ℝ)⁻¹ (q ^ (2 * n + 1)) =
    (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / ‖q‖) • q
have inr : k⁻¹ • (HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q) =
  k⁻¹ • (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) • q
Tactic: calc
    k⁻¹ • q ^ (2 * n + 1) = k⁻¹ • ((-normSq q) ^ n * q) := by rw [pow_succ, pow_mul, hq2]
    _ = k⁻¹ • ((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n)) • q := ?_
    _ = ((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q := ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
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 (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q) =
    k⁻¹ • (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) • q
⊢ HSMul.hSMul (α := ℝ) (↑(2 * n + 1)! : ℝ)⁻¹ (q ^ (2 * n + 1)) =
    (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / ‖q‖) • q
have inr₁ : k⁻¹ • (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) • q = (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q
Tactic: calc
    k⁻¹ • q ^ (2 * n + 1) = k⁻¹ • ((-normSq q) ^ n * q) := by rw [pow_succ, pow_mul, hq2]
    _ = k⁻¹ • ((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n)) • q := ?_
    _ = ((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q := ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
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 (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q) =
    k⁻¹ • (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) • q
have inr : HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q = (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) • q
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
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)! : ℝ)
⊢ HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q = (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) • q
have inr : HPow.hPow (α := ℍ) (-1) n * HPow.hPow (α := ℍ) (↑(‖q‖ * ‖q‖) : ℍ) n * q =
  (↑(HPow.hPow (α := ℝ) (-1) n * (‖q‖ * ‖q‖) ^ n) : ℍ) * q
Tactic: rw [neg_pow, normSq_eq_norm_mul_self, pow_mul, sq, ← coe_mul_eq_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
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)! : ℝ)
⊢ HPow.hPow (α := ℍ) (-1) n * HPow.hPow (α := ℍ) (↑(‖q‖ * ‖q‖) : ℍ) n * q =
    (↑(HPow.hPow (α := ℝ) (-1) n * (‖q‖ * ‖q‖) ^ n) : ℍ) * q
have inr : (↑((↑(Int.negSucc 0 ^ n) : ℝ) * (‖q‖ * ‖q‖) ^ n) : ℍ) * q = (↑((↑(Int.negSucc 0 ^ n) : ℝ) * (‖q‖ * ‖q‖) ^ n) : ℍ) * q
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
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)) • q = (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q
have inr : (k⁻¹ * (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n))) • q = (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q
Tactic: rw [smul_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
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))) • q =
    (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q
have inr : k⁻¹ * (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) = HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (goal)
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 + 1) / k / ‖q‖
have inr : k⁻¹ * (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) = HPow.hPow (α := ℝ) (-1) n * (‖q‖ ^ (2 * n) * k⁻¹)
Tactic: simp_rw [pow_succ, mul_div_assoc, div_div_cancel_left' hqn]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (hypothesis)
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 (n : ℕ) ↦ (expSeries ℝ ℍ n : (a : (i : Fin n) → ℍ) → ℍ) fun (x : Fin n) ↦ q) ((↑c : ℍ) + (s / ‖q‖) • q)
have hc₁ : HasSum (α := ℍ) (fun (a : ℕ) ↦ (↑(HPow.hPow (α := ℝ) (-1) a * ‖q‖ ^ (2 * a) / (↑(2 * a)! : ℝ)) : ℍ)) (↑c : ℍ)
Tactic: replace hc := hasSum_coe.mpr hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.QuaternionExponential (hypothesis)
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 (n : ℕ) ↦ (expSeries ℝ ℍ n : (a : (i : Fin n) → ℍ) → ℍ) fun (x : Fin n) ↦ q) ((↑c : ℍ) + (s / ‖q‖) • q)
have hs₁ : 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
Cleared hypotheses: hs
-- 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)
⊢ HasSum (fun (n : ℕ) ↦ (expSeries ℝ ℍ n : (a : (i : Fin n) → ℍ) → ℍ) fun (x : Fin n) ↦ q) ((↑c : ℍ) + (s / ‖q‖) • q)
have refine_1 : HasSum (α := ℍ) (fun (k : ℕ) ↦ (expSeries ℝ ℍ (2 * k) : (a : (i : Fin (2 * k)) → ℍ) → ℍ) fun (x : Fin (2 * k)) ↦ q)
  (↑c : ℍ)
Tactic: refine HasSum.even_add_odd ?_ ?_
-- 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)
refine_1 :
  HasSum (α := ℍ) (fun (k : ℕ) ↦ (expSeries ℝ ℍ (2 * k) : (a : (i : Fin (2 * k)) → ℍ) → ℍ) fun (x : Fin (2 * k)) ↦ q)
    (↑c : ℍ)
⊢ HasSum (fun (n : ℕ) ↦ (expSeries ℝ ℍ n : (a : (i : Fin n) → ℍ) → ℍ) fun (x : Fin n) ↦ q) ((↑c : ℍ) + (s / ‖q‖) • q)
have 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)
Tactic: refine HasSum.even_add_odd ?_ ?_
-- 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)
⊢ HasSum (α := ℍ) (fun (k : ℕ) ↦ (expSeries ℝ ℍ (2 * k) : (a : (i : Fin (2 * k)) → ℍ) → ℍ) fun (x : Fin (2 * k)) ↦ q)
    (↑c : ℍ)
have 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)! : ℝ)) : ℍ)
Tactic: convert! hc using 1
-- 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)
⊢ 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)! : ℝ)) : ℍ)
have 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)! : ℝ)) : ℍ)
Tactic: ext n : 1
-- 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 : ℕ
⊢ Eq (α := ℍ) ((expSeries ℝ ℍ (2 * n) : (a : (i : Fin (2 * n)) → ℍ) → ℍ) fun (x : Fin (2 * n)) ↦ q)
    (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / (↑(2 * n)! : ℝ)) : ℍ)
have h : Eq (α := ℍ) (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / (↑(2 * n)! : ℝ)) : ℍ)
  (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / (↑(2 * n)! : ℝ)) : ℍ)
Tactic: rw [expSeries_even_of_imaginary hq]
-- 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)
⊢ HasSum (fun (k : ℕ) ↦ (expSeries ℝ ℍ (2 * k + 1) : (a : (i : Fin (2 * k + 1)) → ℍ) → ℍ) fun (x : Fin (2 * k + 1)) ↦ q)
    ((s / ‖q‖) • q)
have 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
Tactic: convert! hs using 1
-- 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)
⊢ 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
have 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
Tactic: ext n : 1