-- Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean
theorem hasSum_arctan {z : ℂ} (hz : ‖z‖ < 1) :
    HasSum (fun n : ℕ ↦ (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) (arctan z)

Proof state:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ Odd (2 * k + 0 + 1)

Tactic:
simp

Result:
no goals

Proof state:
z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan

Tactic:
have := ((hasSum_taylorSeries_log (z := z * I) (by simpa)).add
  (hasSum_taylorSeries_neg_log (z := z * I) (by simpa))).mul_left (-I / 2)

Result:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun i => -I / 2 * ((-1) ^ (i + 1) * (z * I) ^ i / ↑i + (z * I) ^ i / ↑i))
    (-I / 2 * (log (1 + z * I) + -log (1 - z * I)))
⊢ HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan

Proof state:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ -I / 2 * (1 + 1) = -I

Tactic:
ring

Result:
no goals

Proof state:
z : ℂ
hz : ‖z‖ < 1
⊢ ‖z * I‖ < 1

Tactic:
simpa

Result:
no goals

Proof state:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ HasSum
    (fun c =>
      -I / 2 *
        (((-1) ^ (2 * (k, c).1 + ↑(k, c).2 + 1) + 1) * (z * I) ^ (2 * (k, c).1 + ↑(k, c).2) /
          ↑(2 * (k, c).1 + ↑(k, c).2)))
    ((-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1))

Tactic:
dsimp only

Result:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ HasSum (fun c => -I / 2 * (((-1) ^ (2 * k + ↑c + 1) + 1) * (z * I) ^ (2 * k + ↑c) / ↑(2 * k + ↑c)))
    ((-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1))

Proof state:
z : ℂ
hz : ‖z‖ < 1
this : HasSum (fun i => -I / 2 * (((-1) ^ (i + 1) + 1) * (z * I) ^ i / ↑i)) (-I / 2 * log ((1 + z * I) / (1 - z * I)))
⊢ HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan

Tactic:
replace := (Nat.divModEquiv 2).symm.hasSum_iff.mpr this

Result:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum ((fun i => -I / 2 * (((-1) ^ (i + 1) + 1) * (z * I) ^ i / ↑i)) ∘ ⇑(Nat.divModEquiv 2).symm)
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
⊢ HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan

Proof state:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ 2 * k + 1 + 1 = 2 * (k + 1)

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_6.e_a
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ (-1) ^ k * z ^ (2 * k + 1) = -I * (z * I) ^ (2 * k + 1)

Tactic:
rw [mul_pow, pow_succ' I, pow_mul, I_sq,
  show -I * _ = -(I * I) * (-1) ^ k * z ^ (2 * k + 1) by ring, I_mul_I, neg_neg, one_mul]

Result:
no goals

Proof state:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ Even (2 * (k + 1))

Tactic:
simp

Result:
no goals

Proof state:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun i => -I / 2 * ((-1) ^ (i + 1) * (z * I) ^ i / ↑i + (z * I) ^ i / ↑i))
    (-I / 2 * (log (1 + z * I) + -log (1 - z * I)))
⊢ HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan

Tactic:
simp_rw [← add_div, ← add_one_mul, hasSum_arctan_aux hz] at this

Result:
z : ℂ
hz : ‖z‖ < 1
this : HasSum (fun i => -I / 2 * (((-1) ^ (i + 1) + 1) * (z * I) ^ i / ↑i)) (-I / 2 * log ((1 + z * I) / (1 - z * I)))
⊢ HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan

Proof state:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum ((fun i => -I / 2 * (((-1) ^ (i + 1) + 1) * (z * I) ^ i / ↑i)) ∘ ⇑(Nat.divModEquiv 2).symm)
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
⊢ HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan

Tactic:
dsimp [Function.comp_def] at this

Result:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x => -I / 2 * (((-1) ^ (x.1 * 2 + ↑x.2 + 1) + 1) * (z * I) ^ (x.1 * 2 + ↑x.2) / ↑(x.1 * 2 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
⊢ HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan

Proof state:
case h.e'_6
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ (-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1) =
    ∑ b : Fin 2, -I / 2 * (((-1) ^ (2 * k + ↑b + 1) + 1) * (z * I) ^ (2 * k + ↑b) / ↑(2 * k + ↑b))

Tactic:
rw [Fin.sum_univ_two, Fin.val_zero, Fin.val_one, Odd.neg_one_pow (n := 2 * k + 0 + 1) (by simp),
  neg_add_cancel, zero_mul, zero_div, mul_zero, zero_add,
  show 2 * k + 1 + 1 = 2 * (k + 1) by ring, Even.neg_one_pow (n := 2 * (k + 1)) (by simp),
  ← mul_div_assoc (_ / _), ← mul_assoc, show -I / 2 * (1 + 1) = -I by ring]

Result:
case h.e'_6
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ (-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1) = -I * (z * I) ^ (2 * k + 1) / ↑(2 * k + 1)

Proof state:
case h.e'_6
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ (-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1) = -I * (z * I) ^ (2 * k + 1) / ↑(2 * k + 1)

Tactic:
congr 1

Result:
case h.e'_6.e_a
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ (-1) ^ k * z ^ (2 * k + 1) = -I * (z * I) ^ (2 * k + 1)

Proof state:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ HasSum (fun c => -I / 2 * (((-1) ^ (2 * k + ↑c + 1) + 1) * (z * I) ^ (2 * k + ↑c) / ↑(2 * k + ↑c)))
    ((-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1))

Tactic:
convert hasSum_fintype (_ : Fin 2 → ℂ) using 1

Result:
case h.e'_6
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ (-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1) =
    ∑ b : Fin 2, -I / 2 * (((-1) ^ (2 * k + ↑b + 1) + 1) * (z * I) ^ (2 * k + ↑b) / ↑(2 * k + ↑b))

Proof state:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
⊢ HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan

Tactic:
refine this.prod_fiberwise fun k => ?_

Result:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ HasSum
    (fun c =>
      -I / 2 *
        (((-1) ^ (2 * (k, c).1 + ↑(k, c).2 + 1) + 1) * (z * I) ^ (2 * (k, c).1 + ↑(k, c).2) /
          ↑(2 * (k, c).1 + ↑(k, c).2)))
    ((-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1))