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

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
m : (c, ↑z) ∉ ⋯.basin
cz : Complex.abs c ≤ Complex.abs z
⊢ Complex.abs z ≤ 2
Tactic:
contrapose m
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
cz : Complex.abs c ≤ Complex.abs z
m : ¬Complex.abs z ≤ 2
⊢ ¬(c, ↑z) ∉ ⋯.basin

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
cz : Complex.abs c ≤ Complex.abs z
m : ¬Complex.abs z ≤ 2
⊢ ¬(c, ↑z) ∉ ⋯.basin
Tactic:
simp only [not_le, not_not] at m ⊢
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
cz : Complex.abs c ≤ Complex.abs z
m : 2 < Complex.abs z
⊢ (c, ↑z) ∈ ⋯.basin

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
cz : Complex.abs c ≤ Complex.abs z
m : 2 < Complex.abs z
⊢ (c, ↑z) ∈ ⋯.basin
Tactic:
exact julia_two_lt m cz
State after:
no goals