-- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
lemma hasDerivAt_logTaylor (n : ℕ) (z : ℂ) :
    HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z

Proof state:
case succ
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ HasDerivAt (logTaylor (n + 1) + fun z => (-1) ^ (n + 1 + 1) * z ^ (n + 1) / ↑(n + 1))
    (∑ j ∈ Finset.range (n + 1), (-1) ^ j * z ^ j) z

Tactic:
simp only [cpow_natCast, Nat.cast_add, Nat.cast_one, ← Nat.not_even_iff_odd,
  Finset.sum_range_succ, (show (-1) ^ (n + 1 + 1) = (-1) ^ n by ring)]

Result:
case succ
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ HasDerivAt (logTaylor (n + 1) + fun z => (-1) ^ (n + 1 + 1) * z ^ (n + 1) / (↑n + 1))
    (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j + (-1) ^ n * z ^ n) z

Proof state:
case h.e'_9
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ z ^ n = ↑(n + 1) * z ^ (n + 1 - 1) * (↑n + 1)⁻¹

Tactic:
field_simp [Nat.cast_add_one_ne_zero n]

Result:
no goals

Proof state:
case succ
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
this : HasDerivAt (fun x => x ^ (n + 1) / (↑n + 1)) (z ^ n) z
⊢ HasDerivAt (fun z => (-1) ^ (n + 1 + 1) * (z ^ (n + 1) / (↑n + 1))) ((-1) ^ n * z ^ n) z

Tactic:
convert HasDerivAt.const_mul _ this using 2

Result:
case h.e'_9.h.e'_5
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
this : HasDerivAt (fun x => x ^ (n + 1) / (↑n + 1)) (z ^ n) z
⊢ (-1) ^ n = (-1) ^ (n + 1 + 1)

Proof state:
case h.e'_9.h.e'_5
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
this : HasDerivAt (fun x => x ^ (n + 1) / (↑n + 1)) (z ^ n) z
⊢ (-1) ^ n = (-1) ^ (n + 1 + 1)

Tactic:
ring

Result:
no goals

Proof state:
case succ
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ HasDerivAt (fun z => (-1) ^ (n + 1 + 1) * z ^ (n + 1) / (↑n + 1)) ((-1) ^ n * z ^ n) z

Tactic:
simp only [← Nat.not_even_iff_odd, Int.cast_pow, Int.cast_neg, Int.cast_one, mul_div_assoc]

Result:
case succ
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ HasDerivAt (fun z => (-1) ^ (n + 1 + 1) * (z ^ (n + 1) / (↑n + 1))) ((-1) ^ n * z ^ n) z

Proof state:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ HasDerivAt (fun x => x ^ (n + 1) / (↑n + 1)) (z ^ n) z

Tactic:
simp_rw [div_eq_mul_inv]

Result:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ HasDerivAt (fun x => x ^ (n + 1) * (↑n + 1)⁻¹) (z ^ n) z

Proof state:
n : ℕ
z : ℂ
⊢ HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z

Tactic:
induction n with
| zero => simp [logTaylor_succ, logTaylor_zero, Pi.add_def, hasDerivAt_const]
| succ n ih =>
  rw [logTaylor_succ]
  simp only [cpow_natCast, Nat.cast_add, Nat.cast_one, ← Nat.not_even_iff_odd,
    Finset.sum_range_succ, (show (-1) ^ (n + 1 + 1) = (-1) ^ n by ring)]
  refine HasDerivAt.add ih ?_
  simp only [← Nat.not_even_iff_odd, Int.cast_pow, Int.cast_neg, Int.cast_one, mul_div_assoc]
  have : HasDerivAt (fun x : ℂ ↦ (x ^ (n + 1) / (n + 1))) (z ^ n) z := by
    simp_rw [div_eq_mul_inv]
    convert HasDerivAt.mul_const (hasDerivAt_pow (n + 1) z) (((n : ℂ) + 1)⁻¹) using 1
    field_simp [Nat.cast_add_one_ne_zero n]
  convert HasDerivAt.const_mul _ this using 2
  ring

Result:
no goals

Proof state:
case succ
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ HasDerivAt (logTaylor (n + 1) + fun z => (-1) ^ (n + 1 + 1) * z ^ (n + 1) / (↑n + 1))
    (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j + (-1) ^ n * z ^ n) z

Tactic:
refine HasDerivAt.add ih ?_

Result:
case succ
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ HasDerivAt (fun z => (-1) ^ (n + 1 + 1) * z ^ (n + 1) / (↑n + 1)) ((-1) ^ n * z ^ n) z

Proof state:
case succ
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ HasDerivAt (fun z => (-1) ^ (n + 1 + 1) * (z ^ (n + 1) / (↑n + 1))) ((-1) ^ n * z ^ n) z

Tactic:
have : HasDerivAt (fun x : ℂ ↦ (x ^ (n + 1) / (n + 1))) (z ^ n) z := by
  simp_rw [div_eq_mul_inv]
  convert HasDerivAt.mul_const (hasDerivAt_pow (n + 1) z) (((n : ℂ) + 1)⁻¹) using 1
  field_simp [Nat.cast_add_one_ne_zero n]

Result:
case succ
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
this : HasDerivAt (fun x => x ^ (n + 1) / (↑n + 1)) (z ^ n) z
⊢ HasDerivAt (fun z => (-1) ^ (n + 1 + 1) * (z ^ (n + 1) / (↑n + 1))) ((-1) ^ n * z ^ n) z

Proof state:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ (-1) ^ (n + 1 + 1) = (-1) ^ n

Tactic:
ring

Result:
no goals

Proof state:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ HasDerivAt (fun x => x ^ (n + 1) * (↑n + 1)⁻¹) (z ^ n) z

Tactic:
convert HasDerivAt.mul_const (hasDerivAt_pow (n + 1) z) (((n : ℂ) + 1)⁻¹) using 1

Result:
case h.e'_9
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ z ^ n = ↑(n + 1) * z ^ (n + 1 - 1) * (↑n + 1)⁻¹

Proof state:
case zero
z : ℂ
⊢ HasDerivAt (logTaylor (0 + 1)) (∑ j ∈ Finset.range 0, (-1) ^ j * z ^ j) z

Tactic:
simp [logTaylor_succ, logTaylor_zero, Pi.add_def, hasDerivAt_const]

Result:
no goals

Proof state:
case succ
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ HasDerivAt (logTaylor (n + 1 + 1)) (∑ j ∈ Finset.range (n + 1), (-1) ^ j * z ^ j) z

Tactic:
rw [logTaylor_succ]

Result:
case succ
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ HasDerivAt (logTaylor (n + 1) + fun z => (-1) ^ (n + 1 + 1) * z ^ (n + 1) / ↑(n + 1))
    (∑ j ∈ Finset.range (n + 1), (-1) ^ j * z ^ j) z