Theorem: writtenInExtChartAt_coe_f (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ writtenInExtChartAt I I (↑z) (f d c) = f' d c
Tactic:
simp only [writtenInExtChartAt, f, Function.comp, lift_coe', RiemannSphere.extChartAt_coe,
  PartialEquiv.symm_symm, coePartialEquiv_apply, coePartialEquiv_symm_apply, toComplex_coe]
State after:
no goals