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

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ fl (f d) ∞ = fun c z => (z - 0) ^ d • gl d c z
Tactic:
funext c z
State after:
case h.h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
⊢ fl (f d) ∞ c z = (z - 0) ^ d • gl d c z

State before:
case h.h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
⊢ fl (f d) ∞ c z = (z - 0) ^ d • gl d c z
Tactic:
simp only [fl_f, gl, sub_zero, Algebra.id.smul_eq_mul, div_eq_mul_inv]
State after:
no goals