Theorem: mandelbrot_eq_multibrot (Ray/Dynamics/Mandelbrot.lean)

State before:
⊢ mandelbrot = multibrot 2
Tactic:
ext c
State after:
case h
c : ℂ
⊢ c ∈ mandelbrot ↔ c ∈ multibrot 2

State before:
case h
c : ℂ
⊢ c ∈ mandelbrot ↔ c ∈ multibrot 2
Tactic:
simp only [mandelbrot, mem_setOf_eq, multibrot, f_f'_iter, tendsto_inf_iff_tendsto_atInf,
  tendsto_atInf_iff_norm_tendsto_atTop, Complex.norm_eq_abs]
State after:
case h
c : ℂ
⊢ ¬Tendsto (fun n => Complex.abs ((fun z => z ^ 2 + c)^[n] c)) atTop atTop ↔
    ¬Tendsto (fun x => Complex.abs ((f' 2 c)^[x] c)) atTop atTop

State before:
case h
c : ℂ
⊢ ¬Tendsto (fun n => Complex.abs ((fun z => z ^ 2 + c)^[n] c)) atTop atTop ↔
    ¬Tendsto (fun x => Complex.abs ((f' 2 c)^[x] c)) atTop atTop
Tactic:
rfl
State after:
no goals