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

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ 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)
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)
e : multibrot d = (fun z => z.toComplex) '' (multibrotExt d)ᶜ
⊢ IsConnected ((fun z => z.toComplex) '' (multibrotExt d)ᶜ)
Tactic:
apply (isConnected_compl_multibrotExt d).image
State after:
case hf
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ 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)
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)
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)
e : multibrot d = (fun z => z.toComplex) '' (multibrotExt d)ᶜ
⊢ (multibrotExt d)ᶜ ⊆ {∞}ᶜ
Tactic:
intro z m
State after:
case hf
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : multibrot d = (fun z => z.toComplex) '' (multibrotExt d)ᶜ
z : 𝕊
m : z ∈ (multibrotExt d)ᶜ
⊢ z ∈ {∞}ᶜ

State before:
case hf
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : multibrot d = (fun z => z.toComplex) '' (multibrotExt d)ᶜ
z : 𝕊
m : z ∈ (multibrotExt d)ᶜ
⊢ z ∈ {∞}ᶜ
Tactic:
contrapose m
State after:
case hf
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : multibrot d = (fun z => z.toComplex) '' (multibrotExt d)ᶜ
z : 𝕊
m : z ∉ {∞}ᶜ
⊢ z ∉ (multibrotExt d)ᶜ

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

State before:
case hf
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : multibrot d = (fun z => z.toComplex) '' (multibrotExt d)ᶜ
z : 𝕊
m : z = ∞
⊢ z ∉ (multibrotExt d)ᶜ
Tactic:
simp only [m, not_mem_compl_iff, multibrotExt_inf]
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ 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)
⊢ ∀ (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)
⊢ ∀ (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)
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)
z : ℂ
⊢ z ∈ multibrot d ↔ z ∈ (fun z => z.toComplex) '' (multibrotExt d)ᶜ
Tactic:
simp only [mem_image, mem_compl_iff]
State after:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ 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)
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)
z : ℂ
⊢ z ∈ multibrot d → ∃ x ∉ multibrotExt d, x.toComplex = z

case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ 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)
z : ℂ
⊢ z ∈ multibrot d → ∃ x ∉ multibrotExt d, x.toComplex = z

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

case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ 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)
z : ℂ
m : z ∈ multibrot d
⊢ ∃ x ∉ multibrotExt d, x.toComplex = z

case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ (∃ x ∉ multibrotExt d, x.toComplex = z) → z ∈ multibrot d
Tactic:
use z
State after:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
m : z ∈ multibrot d
⊢ ↑z ∉ multibrotExt d ∧ (↑z).toComplex = z

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

State before:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
m : z ∈ multibrot d
⊢ ↑z ∉ multibrotExt d ∧ (↑z).toComplex = z

case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ (∃ x ∉ multibrotExt d, x.toComplex = z) → z ∈ multibrot d
Tactic:
simp only [multibrotExt_coe, not_not, m, toComplex_coe, true_and_iff,
  eq_self_iff_true]
State after:
case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ (∃ x ∉ multibrotExt d, x.toComplex = z) → z ∈ multibrot d

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

State before:
case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
w : 𝕊
m : w ∉ multibrotExt d
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)
z : ℂ
m : ∞ ∉ multibrotExt d
wz : ∞.toComplex = z
⊢ z ∈ multibrot d

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

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

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

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

State before:
case h.mpr.h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z x✝ : ℂ
m : ↑x✝ ∉ multibrotExt d
wz : (↑x✝).toComplex = z
⊢ z ∈ multibrot d
Tactic:
simp only [multibrotExt_coe, not_not, toComplex_coe] at m wz
State after:
case h.mpr.h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z 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)
z x✝ : ℂ
wz : x✝ = z
m : x✝ ∈ multibrot d
⊢ z ∈ multibrot d
Tactic:
rwa [← wz]
State after:
no goals