-- Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean
theorem hasSum_expSeries_of_imaginary {q : Quaternion ℝ} (hq : q.re = 0) {c s : ℝ}
    (hc : HasSum (fun n => (-1 : ℝ) ^ n * ‖q‖ ^ (2 * n) / (2 * n)!) c)
    (hs : HasSum (fun n => (-1 : ℝ) ^ n * ‖q‖ ^ (2 * n + 1) / (2 * n + 1)!) s) :
    HasSum (fun n => expSeries ℝ (Quaternion ℝ) n fun _ => q) (↑c + (s / ‖q‖) • q)

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

Tactic:
replace hc := hasSum_coe.mpr hc

Result:
q : ℍ
hq : q.re = 0
c s : ℝ
hs : HasSum (fun n => (-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)!) s
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
⊢ HasSum (fun n => (expSeries ℝ ℍ n) fun x => q) (↑c + (s / ‖q‖) • q)

Proof state:
case h.e'_5.h
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
n : ℕ
⊢ ((expSeries ℝ ℍ (2 * n + 1)) fun x => q) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q

Tactic:
rw [expSeries_odd_of_imaginary hq]

Result:
no goals

Proof state:
case h.e'_5.h
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
n : ℕ
⊢ ((expSeries ℝ ℍ (2 * n)) fun x => q) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n)!)

Tactic:
rw [expSeries_even_of_imaginary hq]

Result:
no goals

Proof state:
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
⊢ HasSum (fun n => (expSeries ℝ ℍ n) fun x => q) (↑c + (s / ‖q‖) • q)

Tactic:
refine HasSum.even_add_odd ?_ ?_

Result:
case refine_1
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
⊢ HasSum (fun k => (expSeries ℝ ℍ (2 * k)) fun x => q) ↑c

case refine_2
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
⊢ HasSum (fun k => (expSeries ℝ ℍ (2 * k + 1)) fun x => q) ((s / ‖q‖) • q)

Proof state:
case h.e'_5
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
⊢ (fun k => (expSeries ℝ ℍ (2 * k)) fun x => q) = fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)

Tactic:
ext n : 1

Result:
case h.e'_5.h
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
n : ℕ
⊢ ((expSeries ℝ ℍ (2 * n)) fun x => q) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n)!)

Proof state:
case refine_1
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
⊢ HasSum (fun k => (expSeries ℝ ℍ (2 * k)) fun x => q) ↑c

Tactic:
convert hc using 1

Result:
case h.e'_5
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
⊢ (fun k => (expSeries ℝ ℍ (2 * k)) fun x => q) = fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)

Proof state:
case h.e'_5
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
⊢ (fun k => (expSeries ℝ ℍ (2 * k + 1)) fun x => q) = fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q

Tactic:
ext n : 1

Result:
case h.e'_5.h
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
n : ℕ
⊢ ((expSeries ℝ ℍ (2 * n + 1)) fun x => q) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q

Proof state:
case refine_2
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
⊢ HasSum (fun k => (expSeries ℝ ℍ (2 * k + 1)) fun x => q) ((s / ‖q‖) • q)

Tactic:
convert hs using 1

Result:
case h.e'_5
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
⊢ (fun k => (expSeries ℝ ℍ (2 * k + 1)) fun x => q) = fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q

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

Tactic:
replace hs := (hs.div_const ‖q‖).smul_const q

Result:
q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
⊢ HasSum (fun n => (expSeries ℝ ℍ n) fun x => q) (↑c + (s / ‖q‖) • q)