-- Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean
theorem expSeries_odd_of_imaginary {q : Quaternion ℝ} (hq : q.re = 0) (n : ℕ) :
    expSeries ℝ (Quaternion ℝ) (2 * n + 1) (fun _ => q) =
      (((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n + 1) / (2 * n + 1)!) / ‖q‖) • q

Proof state:
case inr.calc_1.e_a
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ (-1) ^ n * ↑(‖q‖ * ‖q‖) ^ n * q = ↑((-1) ^ n * (‖q‖ * ‖q‖) ^ n) * q

Tactic:
norm_cast

Result:
no goals

Proof state:
case inr.calc_2
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ k⁻¹ • ((-1) ^ n * ‖q‖ ^ (2 * n)) • q = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q

Tactic:
rw [smul_smul]

Result:
case inr.calc_2
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ (k⁻¹ * ((-1) ^ n * ‖q‖ ^ (2 * n))) • q = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q

Proof state:
case inl
n : ℕ
hq : QuaternionAlgebra.re 0 = 0
⊢ (↑(2 * n + 1)!)⁻¹ • 0 ^ (2 * n + 1) = ((-1) ^ n * ‖0‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖0‖) • 0

Tactic:
simp

Result:
no goals

Proof state:
case inr.calc_1
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ k⁻¹ • ((-↑(normSq q)) ^ n * q) = k⁻¹ • ((-1) ^ n * ‖q‖ ^ (2 * n)) • q

Tactic:
congr 1

Result:
case inr.calc_1.e_a
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ (-↑(normSq q)) ^ n * q = ((-1) ^ n * ‖q‖ ^ (2 * n)) • q

Proof state:
case inr.calc_1.e_a
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ (-↑(normSq q)) ^ n * q = ((-1) ^ n * ‖q‖ ^ (2 * n)) • q

Tactic:
rw [neg_pow, normSq_eq_norm_mul_self, pow_mul, sq, ← coe_mul_eq_smul]

Result:
case inr.calc_1.e_a
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ (-1) ^ n * ↑(‖q‖ * ‖q‖) ^ n * q = ↑((-1) ^ n * (‖q‖ * ‖q‖) ^ n) * q

Proof state:
case inr
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
⊢ (↑(2 * n + 1)!)⁻¹ • q ^ (2 * n + 1) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q

Tactic:
have hqn := norm_ne_zero_iff.mpr hq0

Result:
case inr
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
⊢ (↑(2 * n + 1)!)⁻¹ • q ^ (2 * n + 1) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q

Proof state:
q : ℍ
hq : q.re = 0
n : ℕ
⊢ (↑(2 * n + 1)!)⁻¹ • q ^ (2 * n + 1) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q

Tactic:
obtain rfl | hq0 := eq_or_ne q 0

Result:
case inl
n : ℕ
hq : QuaternionAlgebra.re 0 = 0
⊢ (↑(2 * n + 1)!)⁻¹ • 0 ^ (2 * n + 1) = ((-1) ^ n * ‖0‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖0‖) • 0

case inr
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
⊢ (↑(2 * n + 1)!)⁻¹ • q ^ (2 * n + 1) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q

Proof state:
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ k⁻¹ • q ^ (2 * n + 1) = k⁻¹ • ((-↑(normSq q)) ^ n * q)

Tactic:
rw [pow_succ, pow_mul, hq2]

Result:
no goals

Proof state:
q : ℍ
hq : q.re = 0
n : ℕ
⊢ ((expSeries ℝ ℍ (2 * n + 1)) fun x => q) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q

Tactic:
rw [expSeries_apply_eq]

Result:
q : ℍ
hq : q.re = 0
n : ℕ
⊢ (↑(2 * n + 1)!)⁻¹ • q ^ (2 * n + 1) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q

Proof state:
case inr.calc_2.e_a
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ k⁻¹ * ((-1) ^ n * ‖q‖ ^ (2 * n)) = (-1) ^ n * (‖q‖ ^ (2 * n) * k⁻¹)

Tactic:
ring

Result:
no goals

Proof state:
case inr.calc_2
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ (k⁻¹ * ((-1) ^ n * ‖q‖ ^ (2 * n))) • q = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q

Tactic:
congr 1

Result:
case inr.calc_2.e_a
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ k⁻¹ * ((-1) ^ n * ‖q‖ ^ (2 * n)) = (-1) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖

Proof state:
case inr
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
⊢ (↑(2 * n + 1)!)⁻¹ • q ^ (2 * n + 1) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q

Tactic:
have hq2 : q ^ 2 = -normSq q := sq_eq_neg_normSq.mpr hq

Result:
case inr
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
⊢ (↑(2 * n + 1)!)⁻¹ • q ^ (2 * n + 1) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q

Proof state:
case inr
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
⊢ (↑(2 * n + 1)!)⁻¹ • q ^ (2 * n + 1) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q

Tactic:
let k : ℝ := ↑(2 * n + 1)!

Result:
case inr
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ (↑(2 * n + 1)!)⁻¹ • q ^ (2 * n + 1) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q

Proof state:
case inr
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ (↑(2 * n + 1)!)⁻¹ • q ^ (2 * n + 1) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖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 := ?_

Result:
case inr.calc_1
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ k⁻¹ • ((-↑(normSq q)) ^ n * q) = k⁻¹ • ((-1) ^ n * ‖q‖ ^ (2 * n)) • q

case inr.calc_2
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ k⁻¹ • ((-1) ^ n * ‖q‖ ^ (2 * n)) • q = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q

Proof state:
case inr.calc_2.e_a
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ k⁻¹ * ((-1) ^ n * ‖q‖ ^ (2 * n)) = (-1) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖

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

Result:
case inr.calc_2.e_a
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ k⁻¹ * ((-1) ^ n * ‖q‖ ^ (2 * n)) = (-1) ^ n * (‖q‖ ^ (2 * n) * k⁻¹)