Theorem: isConnected_compl_multibrot (Ray/Dynamics/Multibrot/Connected.lean)

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
e : (multibrot d)ᶜ = (fun z => z.toComplex) '' (multibrotExt d \ {∞})
⊢ IsConnected (multibrot d)ᶜ
Tactic:
rw [e]
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
e : (multibrot d)ᶜ = (fun z => z.toComplex) '' (multibrotExt d \ {∞})
⊢ IsConnected ((fun z => z.toComplex) '' (multibrotExt d \ {∞}))

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
e : (multibrot d)ᶜ = (fun z => z.toComplex) '' (multibrotExt d \ {∞})
⊢ IsConnected ((fun z => z.toComplex) '' (multibrotExt d \ {∞}))
Tactic:
apply dc.image
State after:
case hf
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
e : (multibrot d)ᶜ = (fun z => z.toComplex) '' (multibrotExt d \ {∞})
⊢ ContinuousOn (fun z => z.toComplex) (multibrotExt d \ {∞})

State before:
case hf
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
e : (multibrot d)ᶜ = (fun z => z.toComplex) '' (multibrotExt d \ {∞})
⊢ ContinuousOn (fun z => z.toComplex) (multibrotExt d \ {∞})
Tactic:
refine continuousOn_toComplex.mono ?_
State after:
case hf
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
e : (multibrot d)ᶜ = (fun z => z.toComplex) '' (multibrotExt d \ {∞})
⊢ multibrotExt d \ {∞} ⊆ {∞}ᶜ

State before:
case hf
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
e : (multibrot d)ᶜ = (fun z => z.toComplex) '' (multibrotExt d \ {∞})
⊢ multibrotExt d \ {∞} ⊆ {∞}ᶜ
Tactic:
intro z ⟨_, i⟩
State after:
case hf
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
e : (multibrot d)ᶜ = (fun z => z.toComplex) '' (multibrotExt d \ {∞})
z : 𝕊
left✝ : z ∈ multibrotExt d
i : z ∉ {∞}
⊢ z ∈ {∞}ᶜ

State before:
case hf
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
e : (multibrot d)ᶜ = (fun z => z.toComplex) '' (multibrotExt d \ {∞})
z : 𝕊
left✝ : z ∈ multibrotExt d
i : z ∉ {∞}
⊢ z ∈ {∞}ᶜ
Tactic:
simp only [mem_singleton_iff, mem_compl_iff] at i ⊢
State after:
case hf
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
e : (multibrot d)ᶜ = (fun z => z.toComplex) '' (multibrotExt d \ {∞})
z : 𝕊
left✝ : z ∈ multibrotExt d
i : ¬z = ∞
⊢ ¬z = ∞

State before:
case hf
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
e : (multibrot d)ᶜ = (fun z => z.toComplex) '' (multibrotExt d \ {∞})
z : 𝕊
left✝ : z ∈ multibrotExt d
i : ¬z = ∞
⊢ ¬z = ∞
Tactic:
exact i
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsConnected (multibrotExt d \ {∞})
Tactic:
refine ⟨⟨(((3 : ℝ) : ℂ) : 𝕊),?_⟩,?_⟩
State after:
case refine_1
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ↑↑3 ∈ multibrotExt d \ {∞}

case refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsPreconnected (multibrotExt d \ {∞})

State before:
case refine_1
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ↑↑3 ∈ multibrotExt d \ {∞}

case refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsPreconnected (multibrotExt d \ {∞})
Tactic:
constructor
State after:
case refine_1.left
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ↑↑3 ∈ multibrotExt d

case refine_1.right
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ↑↑3 ∉ {∞}

case refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsPreconnected (multibrotExt d \ {∞})

State before:
case refine_1.left
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ↑↑3 ∈ multibrotExt d
Tactic:
simp only [multibrotExt_coe, mem_compl_iff]
State after:
case refine_1.left
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ↑3 ∉ multibrot d

State before:
case refine_1.left
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ↑3 ∉ multibrot d
Tactic:
apply multibrot_two_lt
State after:
case refine_1.left.a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 2 < Complex.abs ↑3

State before:
case refine_1.left.a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 2 < Complex.abs ↑3
Tactic:
rw [Complex.abs_ofReal, abs_of_pos]
State after:
case refine_1.left.a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 2 < 3

case refine_1.left.a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 0 < 3

State before:
case refine_1.left.a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 2 < 3

case refine_1.left.a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 0 < 3
Tactic:
norm_num
State after:
case refine_1.left.a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 0 < 3

State before:
case refine_1.left.a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 0 < 3
Tactic:
norm_num
State after:
no goals

State before:
case refine_1.right
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ↑↑3 ∉ {∞}
Tactic:
simp only [mem_singleton_iff, coe_ne_inf, not_false_iff]
State after:
no goals

State before:
case refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsPreconnected (multibrotExt d \ {∞})
Tactic:
exact (isPathConnected_multibrotExt d).isConnected.isPreconnected.open_diff_singleton
  isOpen_multibrotExt _
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
⊢ (multibrot d)ᶜ = (fun z => z.toComplex) '' (multibrotExt d \ {∞})
Tactic:
apply Set.ext
State after:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
⊢ ∀ (x : ℂ), x ∈ (multibrot d)ᶜ ↔ x ∈ (fun z => z.toComplex) '' (multibrotExt d \ {∞})

State before:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
⊢ ∀ (x : ℂ), x ∈ (multibrot d)ᶜ ↔ x ∈ (fun z => z.toComplex) '' (multibrotExt d \ {∞})
Tactic:
intro z
State after:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
⊢ z ∈ (multibrot d)ᶜ ↔ z ∈ (fun z => z.toComplex) '' (multibrotExt d \ {∞})

State before:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
⊢ z ∈ (multibrot d)ᶜ ↔ z ∈ (fun z => z.toComplex) '' (multibrotExt d \ {∞})
Tactic:
simp only [mem_compl_iff, mem_image]
State after:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
⊢ z ∉ multibrot d ↔ ∃ x ∈ multibrotExt d \ {∞}, x.toComplex = z

State before:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
⊢ z ∉ multibrot d ↔ ∃ x ∈ multibrotExt d \ {∞}, x.toComplex = z
Tactic:
constructor
State after:
case h.mp
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
⊢ z ∉ multibrot d → ∃ x ∈ multibrotExt d \ {∞}, x.toComplex = z

case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
⊢ (∃ x ∈ multibrotExt d \ {∞}, x.toComplex = z) → z ∉ multibrot d

State before:
case h.mp
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
⊢ z ∉ multibrot d → ∃ x ∈ multibrotExt d \ {∞}, x.toComplex = z
Tactic:
intro m
State after:
case h.mp
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
m : z ∉ multibrot d
⊢ ∃ x ∈ multibrotExt d \ {∞}, x.toComplex = z

State before:
case h.mp
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
m : z ∉ multibrot d
⊢ ∃ x ∈ multibrotExt d \ {∞}, x.toComplex = z
Tactic:
use z
State after:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
m : z ∉ multibrot d
⊢ ↑z ∈ multibrotExt d \ {∞} ∧ (↑z).toComplex = z

State before:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
m : z ∉ multibrot d
⊢ ↑z ∈ multibrotExt d \ {∞} ∧ (↑z).toComplex = z
Tactic:
simp only [multibrotExt_coe, m, true_and_iff, toComplex_coe, not_false_iff, true_and_iff,
  mem_diff, eq_self_iff_true, and_true_iff, mem_singleton_iff, coe_ne_inf]
State after:
no goals

State before:
case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
⊢ (∃ x ∈ multibrotExt d \ {∞}, x.toComplex = z) → z ∉ multibrot d
Tactic:
intro ⟨w, ⟨m, wi⟩, wz⟩
State after:
case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
w : 𝕊
m : w ∈ multibrotExt d
wi : w ∉ {∞}
wz : w.toComplex = z
⊢ z ∉ multibrot d

State before:
case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
w : 𝕊
m : w ∈ multibrotExt d
wi : w ∉ {∞}
wz : w.toComplex = z
⊢ z ∉ multibrot d
Tactic:
induction w using OnePoint.rec
State after:
case h.mpr.h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
m : ∞ ∈ multibrotExt d
wi : ∞ ∉ {∞}
wz : ∞.toComplex = z
⊢ z ∉ multibrot d

case h.mpr.h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
wi : ↑x✝ ∉ {∞}
wz : (↑x✝).toComplex = z
⊢ z ∉ multibrot d

State before:
case h.mpr.h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
m : ∞ ∈ multibrotExt d
wi : ∞ ∉ {∞}
wz : ∞.toComplex = z
⊢ z ∉ multibrot d
Tactic:
contrapose wi
State after:
case h.mpr.h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
m : ∞ ∈ multibrotExt d
wz : ∞.toComplex = z
wi : ¬z ∉ multibrot d
⊢ ¬∞ ∉ {∞}

State before:
case h.mpr.h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
m : ∞ ∈ multibrotExt d
wz : ∞.toComplex = z
wi : ¬z ∉ multibrot d
⊢ ¬∞ ∉ {∞}
Tactic:
clear wi
State after:
case h.mpr.h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
m : ∞ ∈ multibrotExt d
wz : ∞.toComplex = z
⊢ ¬∞ ∉ {∞}

State before:
case h.mpr.h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
m : ∞ ∈ multibrotExt d
wz : ∞.toComplex = z
⊢ ¬∞ ∉ {∞}
Tactic:
simp only [mem_singleton_iff, not_not]
State after:
no goals

State before:
case h.mpr.h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
wi : ↑x✝ ∉ {∞}
wz : (↑x✝).toComplex = z
⊢ z ∉ multibrot d
Tactic:
simp only [multibrotExt_coe, toComplex_coe, mem_diff] at m wz
State after:
case h.mpr.h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z x✝ : ℂ
wi : ↑x✝ ∉ {∞}
wz : x✝ = z
m : x✝ ∉ multibrot d
⊢ z ∉ multibrot d

State before:
case h.mpr.h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z x✝ : ℂ
wi : ↑x✝ ∉ {∞}
wz : x✝ = z
m : x✝ ∉ multibrot d
⊢ z ∉ multibrot d
Tactic:
rwa [← wz]
State after:
no goals