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

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a : 2 < Complex.abs c
⊢ c ∉ multibrot d
Tactic:
contrapose a
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a : ¬c ∉ multibrot d
⊢ ¬2 < Complex.abs c

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a : ¬c ∉ multibrot d
⊢ ¬2 < Complex.abs c
Tactic:
simp only [not_lt, not_not] at a ⊢
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a : c ∈ multibrot d
⊢ Complex.abs c ≤ 2

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a : c ∈ multibrot d
⊢ Complex.abs c ≤ 2
Tactic:
exact multibrot_le_two a
State after:
no goals