internlm/Lean-Github huggingface dataset:
Theorem: isConnected_compl_multibrotExt
Proof state before:
case refine_2.refine_3
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsPreconnected (potential d ⁻¹' Ici ↑⟨p, m⟩)
Tactic:
simp only [Subtype.coe_mk]
Proof state after:
case refine_2.refine_3
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsPreconnected (potential d ⁻¹' Ici p)
Theorem: isConnected_compl_multibrotExt
Proof state before:
case refine_2.refine_3
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsPreconnected (potential d ⁻¹' Ici p)
Tactic:
refine IsConnected.isPreconnected (IsPathConnected.isConnected ?_)
Proof state after:
case refine_2.refine_3
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsPathConnected (potential d ⁻¹' Ici p)
Theorem: isConnected_compl_multibrotExt
Proof state before:
case refine_2.refine_3
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsPathConnected (potential d ⁻¹' Ici p)
Tactic:
apply IsPathConnected.of_frontier
Proof state after:
case refine_2.refine_3.pc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsPathConnected (potential d ⁻¹' frontier (Ici p))

case refine_2.refine_3.fc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ Continuous (potential d)

case refine_2.refine_3.sc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsClosed (Ici p)
Theorem: isConnected_compl_multibrotExt
Proof state before:
case refine_2.refine_3.pc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsPathConnected (potential d ⁻¹' frontier (Ici p))
Tactic:
rw [frontier_Ici]
Proof state after:
case refine_2.refine_3.pc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsPathConnected (potential d ⁻¹' {p})
Theorem: isConnected_compl_multibrotExt
Proof state before:
case refine_2.refine_3.pc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsPathConnected (potential d ⁻¹' {p})
Tactic:
exact isPathConnected_potential_levelset _ m.1 m.2
Proof state after:
no goals
Theorem: isConnected_compl_multibrotExt
Proof state before:
case refine_2.refine_3.fc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ Continuous (potential d)
Tactic:
exact potential_continuous
Proof state after:
no goals
Theorem: isConnected_compl_multibrotExt
Proof state before:
case refine_2.refine_3.sc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsClosed (Ici p)
Tactic:
exact isClosed_Ici
Proof state after:
no goals
Theorem: isConnected_compl_multibrotExt
Proof state before:
case refine_2.refine_4
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
⊢ ∀ (a : ↑(Ico 0 1)), IsCompact (potential d ⁻¹' Ici ↑a)
Tactic:
intro ⟨p, m⟩
Proof state after:
case refine_2.refine_4
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsCompact (potential d ⁻¹' Ici ↑⟨p, m⟩)
Theorem: isConnected_compl_multibrotExt
Proof state before:
case refine_2.refine_4
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsCompact (potential d ⁻¹' Ici ↑⟨p, m⟩)
Tactic:
exact (isClosed_Ici.preimage potential_continuous).isCompact
Proof state after:
no goals
Theorem: isConnected_multibrot
Proof 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]
Proof 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)ᶜ)
Theorem: isConnected_multibrot
Proof 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
Proof 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)ᶜ
Theorem: isConnected_multibrot
Proof 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 ?_
Proof 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)ᶜ ⊆ {∞}ᶜ
Theorem: isConnected_multibrot
Proof 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
Proof 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 ∈ {∞}ᶜ
Theorem: isConnected_multibrot
Proof 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
Proof 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)ᶜ
Theorem: isConnected_multibrot
Proof 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
Proof 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)ᶜ
Theorem: isConnected_multibrot
Proof 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]
Proof state after:
no goals
Theorem: isConnected_multibrot
Proof 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
Proof 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)ᶜ
Theorem: isConnected_multibrot
Proof 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
Proof 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)ᶜ
Theorem: isConnected_multibrot
Proof 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]
Proof 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
Theorem: isConnected_multibrot
Proof 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
Proof 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
Theorem: isConnected_multibrot
Proof 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
Proof 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
Theorem: isConnected_multibrot
Proof 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
Proof 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
Theorem: isConnected_multibrot
Proof 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]
Proof 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
Theorem: isConnected_multibrot
Proof 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⟩
Proof 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
Theorem: isConnected_multibrot
Proof 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
Proof 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
Theorem: isConnected_multibrot
Proof 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
Proof 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
Theorem: isConnected_multibrot
Proof 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
Proof state after:
case h.mpr.h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
wz : ∞.toComplex = z
⊢ ¬∞ ∉ multibrotExt d
Theorem: isConnected_multibrot
Proof 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]
Proof state after:
no goals
Theorem: isConnected_multibrot
Proof 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
Proof 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
Theorem: isConnected_multibrot
Proof 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]
Proof state after:
no goals
Theorem: isConnected_compl_multibrot
Proof 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]
Proof 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 \ {∞}))
Theorem: isConnected_compl_multibrot
Proof 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
Proof 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 \ {∞})
Theorem: isConnected_compl_multibrot
Proof 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 ?_
Proof 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 \ {∞} ⊆ {∞}ᶜ
Theorem: isConnected_compl_multibrot
Proof 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⟩
Proof 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 ∈ {∞}ᶜ
Theorem: isConnected_compl_multibrot
Proof 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 ⊢
Proof 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 = ∞
Theorem: isConnected_compl_multibrot
Proof 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
Proof state after:
no goals
Theorem: isConnected_compl_multibrot
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsConnected (multibrotExt d \ {∞})
Tactic:
refine ⟨⟨(((3 : ℝ) : ℂ) : 𝕊),?_⟩,?_⟩
Proof 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 \ {∞})
Theorem: isConnected_compl_multibrot
Proof 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
Proof 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 \ {∞})
Theorem: isConnected_compl_multibrot
Proof 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]
Proof state after:
case refine_1.left
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ↑3 ∉ multibrot d
Theorem: isConnected_compl_multibrot
Proof 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
Proof state after:
case refine_1.left.a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 2 < Complex.abs ↑3
Theorem: isConnected_compl_multibrot
Proof 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]
Proof 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
Theorem: isConnected_compl_multibrot
Proof 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
Proof state after:
case refine_1.left.a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 0 < 3
Theorem: isConnected_compl_multibrot
Proof state before:
case refine_1.left.a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 0 < 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: isConnected_compl_multibrot
Proof 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]
Proof state after:
no goals
Theorem: isConnected_compl_multibrot
Proof 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 _
Proof state after:
no goals
Theorem: isConnected_compl_multibrot
Proof 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
Proof 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 \ {∞})
Theorem: isConnected_compl_multibrot
Proof 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
Proof 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 \ {∞})
Theorem: isConnected_compl_multibrot
Proof 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]
Proof 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
Theorem: isConnected_compl_multibrot
Proof 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
Proof 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
Theorem: isConnected_compl_multibrot
Proof 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
Proof 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
Theorem: isConnected_compl_multibrot
Proof 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
Proof 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
Theorem: isConnected_compl_multibrot
Proof 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]
Proof state after:
no goals
Theorem: isConnected_compl_multibrot
Proof 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⟩
Proof 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