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

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
m : c ∈ multibrot d
⊢ Complex.abs c ≤ 2
Tactic:
rw [multibrot_basin' (d := d)] at m
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
m : (c, ↑c) ∉ ⋯.basin
⊢ Complex.abs c ≤ 2

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
m : (c, ↑c) ∉ ⋯.basin
⊢ Complex.abs c ≤ 2
Tactic:
exact julia_le_two m (le_refl _)
State after:
no goals