internlm/Lean-Github huggingface dataset:
Theorem: bottcherNontrivial
Proof state before:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m✝ : c ∈ multibrotExt d
b : ℂ := bottcher d c
h✝ : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
b1 : Complex.abs b < 1
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
e : 𝕊
m : e ∈ multibrotExt d
h : ∀ᶠ (e : 𝕊) in 𝓝 e, bottcher d e = b
⊢ ∀ᶠ (y : 𝕊) in 𝓝 e, y ∈ t
Tactic:
apply (isOpen_multibrotExt.eventually_mem m).mp
Proof state after:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m✝ : c ∈ multibrotExt d
b : ℂ := bottcher d c
h✝ : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
b1 : Complex.abs b < 1
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
e : 𝕊
m : e ∈ multibrotExt d
h : ∀ᶠ (e : 𝕊) in 𝓝 e, bottcher d e = b
⊢ ∀ᶠ (x : 𝕊) in 𝓝 e, x ∈ multibrotExt d → x ∈ t
Theorem: bottcherNontrivial
Proof state before:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m✝ : c ∈ multibrotExt d
b : ℂ := bottcher d c
h✝ : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
b1 : Complex.abs b < 1
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
e : 𝕊
m : e ∈ multibrotExt d
h : ∀ᶠ (e : 𝕊) in 𝓝 e, bottcher d e = b
⊢ ∀ᶠ (x : 𝕊) in 𝓝 e, x ∈ multibrotExt d → x ∈ t
Tactic:
apply (eventually_eventually_nhds.mpr h).mp
Proof state after:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m✝ : c ∈ multibrotExt d
b : ℂ := bottcher d c
h✝ : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
b1 : Complex.abs b < 1
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
e : 𝕊
m : e ∈ multibrotExt d
h : ∀ᶠ (e : 𝕊) in 𝓝 e, bottcher d e = b
⊢ ∀ᶠ (x : 𝕊) in 𝓝 e, (∀ᶠ (x : 𝕊) in 𝓝 x, bottcher d x = b) → x ∈ multibrotExt d → x ∈ t
Theorem: bottcherNontrivial
Proof state before:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m✝ : c ∈ multibrotExt d
b : ℂ := bottcher d c
h✝ : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
b1 : Complex.abs b < 1
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
e : 𝕊
m : e ∈ multibrotExt d
h : ∀ᶠ (e : 𝕊) in 𝓝 e, bottcher d e = b
⊢ ∀ᶠ (x : 𝕊) in 𝓝 e, (∀ᶠ (x : 𝕊) in 𝓝 x, bottcher d x = b) → x ∈ multibrotExt d → x ∈ t
Tactic:
exact eventually_of_forall fun f h m ↦ ⟨m, h⟩
Proof state after:
no goals
Theorem: bottcherNontrivial
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
b1 : Complex.abs b < 1
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
tu : t = univ
⊢ 0 ∈ t
Tactic:
simp only [tu, mem_univ]
Proof state after:
no goals
Theorem: bottcher_surj
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ bottcher d '' multibrotExt d = ball 0 1
Tactic:
set s := superF d
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ bottcher d '' multibrotExt d = ball 0 1
Theorem: bottcher_surj
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ bottcher d '' multibrotExt d = ball 0 1
Tactic:
apply subset_antisymm
Proof state after:
case a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ bottcher d '' multibrotExt d ⊆ ball 0 1

case a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ball 0 1 ⊆ bottcher d '' multibrotExt d
Theorem: bottcher_surj
Proof state before:
case a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ bottcher d '' multibrotExt d ⊆ ball 0 1
Tactic:
intro w
Proof state after:
case a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
w : ℂ
⊢ w ∈ bottcher d '' multibrotExt d → w ∈ ball 0 1
Theorem: bottcher_surj
Proof state before:
case a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
w : ℂ
⊢ w ∈ bottcher d '' multibrotExt d → w ∈ ball 0 1
Tactic:
simp only [mem_image]
Proof state after:
case a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
w : ℂ
⊢ (∃ x ∈ multibrotExt d, bottcher d x = w) → w ∈ ball 0 1
Theorem: bottcher_surj
Proof state before:
case a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
w : ℂ
⊢ (∃ x ∈ multibrotExt d, bottcher d x = w) → w ∈ ball 0 1
Tactic:
intro ⟨c, m, e⟩
Proof state after:
case a
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
w : ℂ
c : 𝕊
m : c ∈ multibrotExt d
e : bottcher d c = w
⊢ w ∈ ball 0 1
Theorem: bottcher_surj
Proof state before:
case a
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
w : ℂ
c : 𝕊
m : c ∈ multibrotExt d
e : bottcher d c = w
⊢ w ∈ ball 0 1
Tactic:
rw [← e]
Proof state after:
case a
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
w : ℂ
c : 𝕊
m : c ∈ multibrotExt d
e : bottcher d c = w
⊢ bottcher d c ∈ ball 0 1
Theorem: bottcher_surj
Proof state before:
case a
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
w : ℂ
c : 𝕊
m : c ∈ multibrotExt d
e : bottcher d c = w
⊢ bottcher d c ∈ ball 0 1
Tactic:
clear e w
Proof state after:
case a
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
c : 𝕊
m : c ∈ multibrotExt d
⊢ bottcher d c ∈ ball 0 1
Theorem: bottcher_surj
Proof state before:
case a
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
c : 𝕊
m : c ∈ multibrotExt d
⊢ bottcher d c ∈ ball 0 1
Tactic:
induction c using OnePoint.rec
Proof state after:
case a.h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
m : ∞ ∈ multibrotExt d
⊢ bottcher d ∞ ∈ ball 0 1

case a.h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
⊢ bottcher d ↑x✝ ∈ ball 0 1
Theorem: bottcher_surj
Proof state before:
case a.h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
m : ∞ ∈ multibrotExt d
⊢ bottcher d ∞ ∈ ball 0 1
Tactic:
simp only [bottcher, fill_inf]
Proof state after:
case a.h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
m : ∞ ∈ multibrotExt d
⊢ 0 ∈ ball 0 1
Theorem: bottcher_surj
Proof state before:
case a.h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
m : ∞ ∈ multibrotExt d
⊢ 0 ∈ ball 0 1
Tactic:
exact mem_ball_self one_pos
Proof state after:
no goals
Theorem: bottcher_surj
Proof state before:
case a.h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
⊢ bottcher d ↑x✝ ∈ ball 0 1
Tactic:
simp only [multibrotExt_coe] at m
Proof state after:
case a.h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : x✝ ∉ multibrot d
⊢ bottcher d ↑x✝ ∈ ball 0 1
Theorem: bottcher_surj
Proof state before:
case a.h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : x✝ ∉ multibrot d
⊢ bottcher d ↑x✝ ∈ ball 0 1
Tactic:
simp only [bottcher, fill_coe, bottcher', mem_ball, Complex.dist_eq, sub_zero]
Proof state after:
case a.h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : x✝ ∉ multibrot d
⊢ Complex.abs (⋯.bottcher x✝ ↑x✝) < 1
Theorem: bottcher_surj
Proof state before:
case a.h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : x✝ ∉ multibrot d
⊢ Complex.abs (⋯.bottcher x✝ ↑x✝) < 1
Tactic:
exact s.bottcher_lt_one (multibrotPost m)
Proof state after:
no goals
Theorem: bottcher_surj
Proof state before:
case a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ball 0 1 ⊆ bottcher d '' multibrotExt d
Tactic:
refine _root_.trans ?_ interior_subset
Proof state after:
case a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ball 0 1 ⊆ interior (bottcher d '' multibrotExt d)
Theorem: bottcher_surj
Proof state before:
case a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ball 0 1 ⊆ interior (bottcher d '' multibrotExt d)
Tactic:
refine IsPreconnected.relative_clopen (convex_ball _ _).isPreconnected ?_ ?_ ?_
Proof state after:
case a.refine_1
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ (ball 0 1 ∩ bottcher d '' multibrotExt d).Nonempty

case a.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ball 0 1 ∩ bottcher d '' multibrotExt d ⊆ interior (bottcher d '' multibrotExt d)

case a.refine_3
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ball 0 1 ∩ closure (bottcher d '' multibrotExt d) ⊆ bottcher d '' multibrotExt d
Theorem: bottcher_surj
Proof state before:
case a.refine_1
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ (ball 0 1 ∩ bottcher d '' multibrotExt d).Nonempty
Tactic:
use 0, mem_ball_self one_pos, ∞
Proof state after:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ∞ ∈ multibrotExt d ∧ bottcher d ∞ = 0
Theorem: bottcher_surj
Proof state before:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ∞ ∈ multibrotExt d ∧ bottcher d ∞ = 0
Tactic:
simp only [multibrotExt_inf, bottcher, fill_inf, true_and_iff]
Proof state after:
no goals
Theorem: bottcher_surj
Proof state before:
case a.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ball 0 1 ∩ bottcher d '' multibrotExt d ⊆ interior (bottcher d '' multibrotExt d)
Tactic:
rw [IsOpen.interior_eq]
Proof state after:
case a.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ball 0 1 ∩ bottcher d '' multibrotExt d ⊆ bottcher d '' multibrotExt d

case a.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ IsOpen (bottcher d '' multibrotExt d)
Theorem: bottcher_surj
Proof state before:
case a.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ball 0 1 ∩ bottcher d '' multibrotExt d ⊆ bottcher d '' multibrotExt d

case a.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ IsOpen (bottcher d '' multibrotExt d)
Tactic:
exact inter_subset_right _ _
Proof state after:
case a.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ IsOpen (bottcher d '' multibrotExt d)
Theorem: bottcher_surj
Proof state before:
case a.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ IsOpen (bottcher d '' multibrotExt d)
Tactic:
rw [isOpen_iff_eventually]
Proof state after:
case a.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ∀ x ∈ bottcher d '' multibrotExt d, ∀ᶠ (y : ℂ) in 𝓝 x, y ∈ bottcher d '' multibrotExt d
Theorem: bottcher_surj
Proof state before:
case a.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ∀ x ∈ bottcher d '' multibrotExt d, ∀ᶠ (y : ℂ) in 𝓝 x, y ∈ bottcher d '' multibrotExt d
Tactic:
intro z ⟨c, m, e⟩
Proof state after:
case a.refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
z : ℂ
c : 𝕊
m : c ∈ multibrotExt d
e : bottcher d c = z
⊢ ∀ᶠ (y : ℂ) in 𝓝 z, y ∈ bottcher d '' multibrotExt d
Theorem: bottcher_surj
Proof state before:
case a.refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
z : ℂ
c : 𝕊
m : c ∈ multibrotExt d
e : bottcher d c = z
⊢ ∀ᶠ (y : ℂ) in 𝓝 z, y ∈ bottcher d '' multibrotExt d
Tactic:
rw [← e, (bottcherNontrivial m).nhds_eq_map_nhds, Filter.eventually_map]
Proof state after:
case a.refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
z : ℂ
c : 𝕊
m : c ∈ multibrotExt d
e : bottcher d c = z
⊢ ∀ᶠ (a : 𝕊) in 𝓝 c, bottcher d a ∈ bottcher d '' multibrotExt d
Theorem: bottcher_surj
Proof state before:
case a.refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
z : ℂ
c : 𝕊
m : c ∈ multibrotExt d
e : bottcher d c = z
⊢ ∀ᶠ (a : 𝕊) in 𝓝 c, bottcher d a ∈ bottcher d '' multibrotExt d
Tactic:
exact
  (isOpen_multibrotExt.eventually_mem m).mp (eventually_of_forall fun e m ↦ by use e, m)
Proof state after:
no goals
Theorem: bottcher_surj
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
z : ℂ
c : 𝕊
m✝ : c ∈ multibrotExt d
e✝ : bottcher d c = z
e : 𝕊
m : e ∈ multibrotExt d
⊢ bottcher d e ∈ bottcher d '' multibrotExt d
Tactic:
use e, m
Proof state after:
no goals
Theorem: bottcher_surj
Proof state before:
case a.refine_3
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ball 0 1 ∩ closure (bottcher d '' multibrotExt d) ⊆ bottcher d '' multibrotExt d
Tactic:
intro x ⟨x1, m⟩
Proof state after:
case a.refine_3
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
x1 : x ∈ ball 0 1
m : x ∈ closure (bottcher d '' multibrotExt d)
⊢ x ∈ bottcher d '' multibrotExt d
Theorem: bottcher_surj
Proof state before:
case a.refine_3
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
x1 : x ∈ ball 0 1
m : x ∈ closure (bottcher d '' multibrotExt d)
⊢ x ∈ bottcher d '' multibrotExt d
Tactic:
simp only [mem_ball, Complex.dist_eq, sub_zero] at x1
Proof state after:
case a.refine_3
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
⊢ x ∈ bottcher d '' multibrotExt d
Theorem: bottcher_surj
Proof state before:
case a.refine_3
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
⊢ x ∈ bottcher d '' multibrotExt d
Tactic:
rcases exists_between x1 with ⟨b, xb, b1⟩
Proof state after:
case a.refine_3.intro.intro
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
⊢ x ∈ bottcher d '' multibrotExt d
Theorem: bottcher_surj
Proof state before:
case a.refine_3.intro.intro
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
⊢ x ∈ bottcher d '' multibrotExt d
Tactic:
set t := {e | potential d e ≤ b}
Proof state after:
case a.refine_3.intro.intro
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
⊢ x ∈ bottcher d '' multibrotExt d
Theorem: bottcher_surj
Proof state before:
case a.refine_3.intro.intro
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
⊢ x ∈ bottcher d '' multibrotExt d
Tactic:
have ct : IsCompact t := (isClosed_le potential_continuous continuous_const).isCompact
Proof state after:
case a.refine_3.intro.intro
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
⊢ x ∈ bottcher d '' multibrotExt d
Theorem: bottcher_surj
Proof state before:
case a.refine_3.intro.intro
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
⊢ x ∈ bottcher d '' multibrotExt d
Tactic:
have ts : t ⊆ multibrotExt d := by
  intro c m; rw [← potential_lt_one]; exact lt_of_le_of_lt m b1
Proof state after:
case a.refine_3.intro.intro
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
⊢ x ∈ bottcher d '' multibrotExt d
Theorem: bottcher_surj
Proof state before:
case a.refine_3.intro.intro
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
⊢ x ∈ bottcher d '' multibrotExt d
Tactic:
have mt : x ∈ closure (bottcher d '' t) := by
  rw [mem_closure_iff_frequently] at m ⊢; apply m.mp
  have lt : ∀ᶠ y : ℂ in 𝓝 x, abs y < b :=
    Complex.continuous_abs.continuousAt.eventually_lt continuousAt_const xb
  refine lt.mp (eventually_of_forall fun y lt m ↦ ?_)
  rcases m with ⟨c, _, cy⟩; rw [← cy]; rw [← cy, abs_bottcher] at lt
  exact ⟨c, lt.le, rfl⟩
Proof state after:
case a.refine_3.intro.intro
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
mt : x ∈ closure (bottcher d '' t)
⊢ x ∈ bottcher d '' multibrotExt d
Theorem: bottcher_surj
Proof state before:
case a.refine_3.intro.intro
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
mt : x ∈ closure (bottcher d '' t)
⊢ x ∈ bottcher d '' multibrotExt d
Tactic:
apply image_subset _ ts
Proof state after:
case a.refine_3.intro.intro.a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
mt : x ∈ closure (bottcher d '' t)
⊢ x ∈ bottcher d '' t
Theorem: bottcher_surj
Proof state before:
case a.refine_3.intro.intro.a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
mt : x ∈ closure (bottcher d '' t)
⊢ x ∈ bottcher d '' t
Tactic:
rw [IsClosed.closure_eq] at mt
Proof state after:
case a.refine_3.intro.intro.a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
mt : x ∈ bottcher d '' t
⊢ x ∈ bottcher d '' t

case a.refine_3.intro.intro.a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
mt : x ∈ closure (bottcher d '' t)
⊢ IsClosed (bottcher d '' t)
Theorem: bottcher_surj
Proof state before:
case a.refine_3.intro.intro.a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
mt : x ∈ bottcher d '' t
⊢ x ∈ bottcher d '' t

case a.refine_3.intro.intro.a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
mt : x ∈ closure (bottcher d '' t)
⊢ IsClosed (bottcher d '' t)
Tactic:
exact mt
Proof state after:
case a.refine_3.intro.intro.a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
mt : x ∈ closure (bottcher d '' t)
⊢ IsClosed (bottcher d '' t)
Theorem: bottcher_surj
Proof state before:
case a.refine_3.intro.intro.a
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
mt : x ∈ closure (bottcher d '' t)
⊢ IsClosed (bottcher d '' t)
Tactic:
apply IsCompact.isClosed
Proof state after:
case a.refine_3.intro.intro.a.hs
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
mt : x ∈ closure (bottcher d '' t)
⊢ IsCompact (bottcher d '' t)
Theorem: bottcher_surj
Proof state before:
case a.refine_3.intro.intro.a.hs
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
mt : x ∈ closure (bottcher d '' t)
⊢ IsCompact (bottcher d '' t)
Tactic:
apply IsCompact.image_of_continuousOn ct
Proof state after:
case a.refine_3.intro.intro.a.hs
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
mt : x ∈ closure (bottcher d '' t)
⊢ ContinuousOn (bottcher d) t
Theorem: bottcher_surj
Proof state before:
case a.refine_3.intro.intro.a.hs
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
mt : x ∈ closure (bottcher d '' t)
⊢ ContinuousOn (bottcher d) t
Tactic:
refine ContinuousOn.mono ?_ ts
Proof state after:
case a.refine_3.intro.intro.a.hs
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
mt : x ∈ closure (bottcher d '' t)
⊢ ContinuousOn (bottcher d) (multibrotExt d)