Theorem: deriv_f' (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ deriv (f' d c) z = ↑d * z ^ (d - 1)
Tactic:
have h : HasDerivAt (f' d c) (d * z ^ (d - 1) + 0) z :=
  (hasDerivAt_pow _ _).add (hasDerivAt_const _ _)
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
h : HasDerivAt (f' d c) (↑d * z ^ (d - 1) + 0) z
⊢ deriv (f' d c) z = ↑d * z ^ (d - 1)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
h : HasDerivAt (f' d c) (↑d * z ^ (d - 1) + 0) z
⊢ deriv (f' d c) z = ↑d * z ^ (d - 1)
Tactic:
simp only [add_zero] at h
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
h : HasDerivAt (f' d c) (↑d * z ^ (d - 1)) z
⊢ deriv (f' d c) z = ↑d * z ^ (d - 1)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
h : HasDerivAt (f' d c) (↑d * z ^ (d - 1)) z
⊢ deriv (f' d c) z = ↑d * z ^ (d - 1)
Tactic:
exact h.deriv
State after:
no goals