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

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
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

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
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

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
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

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]
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

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⟩
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

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]
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

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
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

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
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

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]
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

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
State after:
no goals

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
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

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]
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

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)
State after:
no goals

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
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)

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 ?_ ?_ ?_
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

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, ∞
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

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]
State after:
no goals

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]
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)

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 _ _
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)

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]
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

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⟩
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

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]
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

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)
State after:
no goals

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
State after:
no goals

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⟩
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

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
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

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⟩
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

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}
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

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
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

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
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

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⟩
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

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
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

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
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)

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
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)

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
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)

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
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

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
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)

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) (multibrotExt d)
Tactic:
exact (bottcherHolomorphic d).continuousOn
State after:
no goals

State before:
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
⊢ t ⊆ multibrotExt d
Tactic:
intro c m
State after:
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
c : 𝕊
m : c ∈ t
⊢ c ∈ multibrotExt d

State before:
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
c : 𝕊
m : c ∈ t
⊢ c ∈ multibrotExt d
Tactic:
rw [← potential_lt_one]
State after:
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
c : 𝕊
m : c ∈ t
⊢ potential d c < 1

State before:
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
c : 𝕊
m : c ∈ t
⊢ potential d c < 1
Tactic:
exact lt_of_le_of_lt m b1
State after:
no goals

State before:
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 ∈ closure (bottcher d '' t)
Tactic:
rw [mem_closure_iff_frequently] at m ⊢
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ 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 : ℂ) in 𝓝 x, x ∈ bottcher d '' t

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ 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 : ℂ) in 𝓝 x, x ∈ bottcher d '' t
Tactic:
apply m.mp
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ 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 : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d → x ∈ bottcher d '' t

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ 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 : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d → x ∈ bottcher d '' t
Tactic:
have lt : ∀ᶠ y : ℂ in 𝓝 x, abs y < b :=
  Complex.continuous_abs.continuousAt.eventually_lt continuousAt_const xb
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ 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
lt : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
⊢ ∀ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d → x ∈ bottcher d '' t

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ 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
lt : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
⊢ ∀ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d → x ∈ bottcher d '' t
Tactic:
refine lt.mp (eventually_of_forall fun y lt m ↦ ?_)
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m✝ : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ 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
lt✝ : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
y : ℂ
lt : Complex.abs y < b
m : y ∈ bottcher d '' multibrotExt d
⊢ y ∈ bottcher d '' t

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m✝ : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ 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
lt✝ : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
y : ℂ
lt : Complex.abs y < b
m : y ∈ bottcher d '' multibrotExt d
⊢ y ∈ bottcher d '' t
Tactic:
rcases m with ⟨c, _, cy⟩
State after:
case intro.intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ 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
lt✝ : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
y : ℂ
lt : Complex.abs y < b
c : 𝕊
left✝ : c ∈ multibrotExt d
cy : bottcher d c = y
⊢ y ∈ bottcher d '' t

State before:
case intro.intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ 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
lt✝ : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
y : ℂ
lt : Complex.abs y < b
c : 𝕊
left✝ : c ∈ multibrotExt d
cy : bottcher d c = y
⊢ y ∈ bottcher d '' t
Tactic:
rw [← cy]
State after:
case intro.intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ 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
lt✝ : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
y : ℂ
lt : Complex.abs y < b
c : 𝕊
left✝ : c ∈ multibrotExt d
cy : bottcher d c = y
⊢ bottcher d c ∈ bottcher d '' t

State before:
case intro.intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ 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
lt✝ : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
y : ℂ
lt : Complex.abs y < b
c : 𝕊
left✝ : c ∈ multibrotExt d
cy : bottcher d c = y
⊢ bottcher d c ∈ bottcher d '' t
Tactic:
rw [← cy, abs_bottcher] at lt
State after:
case intro.intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ 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
lt✝ : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
y : ℂ
c : 𝕊
lt : potential d c < b
left✝ : c ∈ multibrotExt d
cy : bottcher d c = y
⊢ bottcher d c ∈ bottcher d '' t

State before:
case intro.intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ 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
lt✝ : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
y : ℂ
c : 𝕊
lt : potential d c < b
left✝ : c ∈ multibrotExt d
cy : bottcher d c = y
⊢ bottcher d c ∈ bottcher d '' t
Tactic:
exact ⟨c, lt.le, rfl⟩
State after:
no goals