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

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ c ∈ multibrot d ↔ ¬Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Tactic:
simp only [multibrot, mem_setOf, f_f'_iter, not_iff_not, tendsto_inf_iff_tendsto_atInf]
State after:
no goals