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

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
⊢ NontrivialHolomorphicAt (bottcher d) c
Tactic:
by_cases h : ∃ᶠ e in 𝓝 c, bottcher d e ≠ bottcher d c
State after:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ∃ᶠ (e : 𝕊) in 𝓝 c, bottcher d e ≠ bottcher d c
⊢ NontrivialHolomorphicAt (bottcher d) c

case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ¬∃ᶠ (e : 𝕊) in 𝓝 c, bottcher d e ≠ bottcher d c
⊢ NontrivialHolomorphicAt (bottcher d) c

State before:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ∃ᶠ (e : 𝕊) in 𝓝 c, bottcher d e ≠ bottcher d c
⊢ NontrivialHolomorphicAt (bottcher d) c

case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ¬∃ᶠ (e : 𝕊) in 𝓝 c, bottcher d e ≠ bottcher d c
⊢ NontrivialHolomorphicAt (bottcher d) c
Tactic:
exact
  { holomorphicAt := bottcherHolomorphic d _ m
    nonconst := h }
State after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ¬∃ᶠ (e : 𝕊) in 𝓝 c, bottcher d e ≠ bottcher d c
⊢ NontrivialHolomorphicAt (bottcher d) c

State before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ¬∃ᶠ (e : 𝕊) in 𝓝 c, bottcher d e ≠ bottcher d c
⊢ NontrivialHolomorphicAt (bottcher d) c
Tactic:
exfalso
State after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ¬∃ᶠ (e : 𝕊) in 𝓝 c, bottcher d e ≠ bottcher d c
⊢ False

State before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ¬∃ᶠ (e : 𝕊) in 𝓝 c, bottcher d e ≠ bottcher d c
⊢ False
Tactic:
simp only [Filter.not_frequently, not_not] at h
State after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = bottcher d c
⊢ False

State before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = bottcher d c
⊢ False
Tactic:
set b := bottcher d c
State after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
⊢ False

State before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
⊢ False
Tactic:
have b1 : abs b < 1 := by simp only [abs_bottcher, potential_lt_one, m, b]
State after:
case neg
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
⊢ False

State before:
case neg
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
⊢ False
Tactic:
set t := {c | c ∈ multibrotExt d ∧ ∀ᶠ e in 𝓝 c, bottcher d e = b}
State after:
case neg
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}
⊢ False

State before:
case neg
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
⊢ False
Tactic:
have m0 : (0 : 𝕊) ∈ multibrotExt d :=
  haveI m : (0 : 𝕊) ∈ t := by simp only [tu, mem_univ]
  m.1
State after:
case neg
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
m0 : 0 ∈ multibrotExt d
⊢ False

State before:
case neg
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
m0 : 0 ∈ multibrotExt d
⊢ False
Tactic:
simp only [← coe_zero, multibrotExt_coe, multibrot_zero, not_true] at m0
State after:
no goals

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
⊢ Complex.abs b < 1
Tactic:
simp only [abs_bottcher, potential_lt_one, m, b]
State after:
no goals

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}
⊢ t = univ
Tactic:
refine IsClopen.eq_univ ?_ ⟨c, m, h⟩
State after:
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}
⊢ IsClopen t

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}
⊢ IsClopen t
Tactic:
constructor
State after:
case left
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}
⊢ IsClosed t

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}
⊢ IsOpen t

State before:
case left
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}
⊢ IsClosed t
Tactic:
rw [isClosed_iff_frequently]
State after:
case left
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}
⊢ ∀ (x : 𝕊), (∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t) → x ∈ t

State before:
case left
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}
⊢ ∀ (x : 𝕊), (∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t) → x ∈ t
Tactic:
intro x e
State after:
case left
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}
x : 𝕊
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
⊢ x ∈ t

State before:
case left
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}
x : 𝕊
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
⊢ x ∈ t
Tactic:
by_contra xt
State after:
case left
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}
x : 𝕊
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
⊢ False

State before:
case left
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}
x : 𝕊
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
⊢ False
Tactic:
have pb : potential d x = abs b := by
  apply tendsto_nhds_unique_of_frequently_eq potential_continuous.continuousAt
    continuousAt_const
  refine e.mp (eventually_of_forall ?_); intro z ⟨_, h⟩; rw [← h.self_of_nhds, abs_bottcher]
State after:
case left
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}
x : 𝕊
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
pb : potential d x = Complex.abs b
⊢ False

State before:
case left
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}
x : 𝕊
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
pb : potential d x = Complex.abs b
⊢ False
Tactic:
rw [← pb, potential_lt_one] at b1
State after:
case left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
pb : potential d x = Complex.abs b
⊢ False

State before:
case left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
pb : potential d x = Complex.abs b
⊢ False
Tactic:
have e' : ∃ᶠ y in 𝓝[{x}ᶜ] x, y ∈ t := by
  simp only [frequently_nhdsWithin_iff, mem_compl_singleton_iff]
  refine e.mp (eventually_of_forall fun z zt ↦ ⟨zt, ?_⟩)
  contrapose xt; simp only [not_not] at xt ⊢; rwa [← xt]
State after:
case left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
⊢ False

State before:
case left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
⊢ False
Tactic:
contrapose xt
State after:
case left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
xt : ¬False
⊢ ¬x ∉ t

State before:
case left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
xt : ¬False
⊢ ¬x ∉ t
Tactic:
clear xt
State after:
case left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
⊢ ¬x ∉ t

State before:
case left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
⊢ ¬x ∉ t
Tactic:
simp only [not_not]
State after:
case left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
⊢ x ∈ t

State before:
case left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
⊢ x ∈ t
Tactic:
use b1
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
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
⊢ ∀ᶠ (e : 𝕊) in 𝓝 x, bottcher d e = b

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
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
⊢ ∀ᶠ (e : 𝕊) in 𝓝 x, bottcher d e = b
Tactic:
cases' HolomorphicAt.eventually_eq_or_eventually_ne (bottcherHolomorphic d _ b1)
  holomorphicAt_const with h h
State after:
case right.inl
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h✝ : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
h : ∀ᶠ (w : 𝕊) in 𝓝 x, bottcher d w = ?m.320207
⊢ ∀ᶠ (e : 𝕊) in 𝓝 x, bottcher d e = b

case right.inr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h✝ : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
h : ∀ᶠ (w : 𝕊) in 𝓝[≠] x, bottcher d w ≠ ?m.320207
⊢ ∀ᶠ (e : 𝕊) in 𝓝 x, bottcher d e = b

State before:
case right.inl
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h✝ : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
h : ∀ᶠ (w : 𝕊) in 𝓝 x, bottcher d w = ?m.320207
⊢ ∀ᶠ (e : 𝕊) in 𝓝 x, bottcher d e = b

case right.inr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h✝ : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
h : ∀ᶠ (w : 𝕊) in 𝓝[≠] x, bottcher d w ≠ ?m.320207
⊢ ∀ᶠ (e : 𝕊) in 𝓝 x, bottcher d e = b
Tactic:
use h
State after:
case right.inr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h✝ : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
h : ∀ᶠ (w : 𝕊) in 𝓝[≠] x, bottcher d w ≠ b
⊢ ∀ᶠ (e : 𝕊) in 𝓝 x, bottcher d e = b

State before:
case right.inr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h✝ : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
h : ∀ᶠ (w : 𝕊) in 𝓝[≠] x, bottcher d w ≠ b
⊢ ∀ᶠ (e : 𝕊) in 𝓝 x, bottcher d e = b
Tactic:
contrapose h
State after:
case right.inr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h✝ : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
h : ¬∀ᶠ (e : 𝕊) in 𝓝 x, bottcher d e = b
⊢ ¬∀ᶠ (w : 𝕊) in 𝓝[≠] x, bottcher d w ≠ b

State before:
case right.inr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h✝ : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
h : ¬∀ᶠ (e : 𝕊) in 𝓝 x, bottcher d e = b
⊢ ¬∀ᶠ (w : 𝕊) in 𝓝[≠] x, bottcher d w ≠ b
Tactic:
simp only [Filter.not_eventually, not_not] at h ⊢
State after:
case right.inr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h✝ : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
h : ∃ᶠ (x : 𝕊) in 𝓝 x, ¬bottcher d x = b
⊢ ∃ᶠ (x : 𝕊) in 𝓝[≠] x, bottcher d x = b

State before:
case right.inr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h✝ : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
e' : ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
h : ∃ᶠ (x : 𝕊) in 𝓝 x, ¬bottcher d x = b
⊢ ∃ᶠ (x : 𝕊) in 𝓝[≠] x, bottcher d x = b
Tactic:
exact e'.mp (eventually_of_forall fun y yt ↦ yt.2.self_of_nhds)
State after:
no goals

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}
x : 𝕊
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
⊢ potential d x = Complex.abs b
Tactic:
apply tendsto_nhds_unique_of_frequently_eq potential_continuous.continuousAt
  continuousAt_const
State after:
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}
x : 𝕊
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
⊢ ∃ᶠ (x : 𝕊) in 𝓝 x, potential d x = Complex.abs b

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}
x : 𝕊
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
⊢ ∃ᶠ (x : 𝕊) in 𝓝 x, potential d x = Complex.abs b
Tactic:
refine e.mp (eventually_of_forall ?_)
State after:
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}
x : 𝕊
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
⊢ ∀ x ∈ t, potential d x = Complex.abs b

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}
x : 𝕊
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
⊢ ∀ x ∈ t, potential d x = Complex.abs b
Tactic:
intro z ⟨_, h⟩
State after:
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}
x : 𝕊
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
z : 𝕊
left✝ : z ∈ multibrotExt d
h : ∀ᶠ (e : 𝕊) in 𝓝 z, bottcher d e = b
⊢ potential d z = Complex.abs b

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}
x : 𝕊
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
z : 𝕊
left✝ : z ∈ multibrotExt d
h : ∀ᶠ (e : 𝕊) in 𝓝 z, bottcher d e = b
⊢ potential d z = Complex.abs b
Tactic:
rw [← h.self_of_nhds, abs_bottcher]
State after:
no goals

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
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
pb : potential d x = Complex.abs b
⊢ ∃ᶠ (y : 𝕊) in 𝓝[≠] x, y ∈ t
Tactic:
simp only [frequently_nhdsWithin_iff, mem_compl_singleton_iff]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
pb : potential d x = Complex.abs b
⊢ ∃ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ∈ t ∧ x_1 ≠ x

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
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
pb : potential d x = Complex.abs b
⊢ ∃ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ∈ t ∧ x_1 ≠ x
Tactic:
refine e.mp (eventually_of_forall fun z zt ↦ ⟨zt, ?_⟩)
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
pb : potential d x = Complex.abs b
z : 𝕊
zt : z ∈ t
⊢ z ≠ x

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
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
pb : potential d x = Complex.abs b
z : 𝕊
zt : z ∈ t
⊢ z ≠ x
Tactic:
contrapose xt
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
z : 𝕊
zt : z ∈ t
xt : ¬z ≠ x
⊢ ¬x ∉ t

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
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
z : 𝕊
zt : z ∈ t
xt : ¬z ≠ x
⊢ ¬x ∉ t
Tactic:
simp only [not_not] at xt ⊢
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
z : 𝕊
zt : z ∈ t
xt : z = x
⊢ x ∈ t

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
t : Set 𝕊 := {c | c ∈ multibrotExt d ∧ ∀ᶠ (e : 𝕊) in 𝓝 c, bottcher d e = b}
x : 𝕊
b1 : x ∈ multibrotExt d
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
pb : potential d x = Complex.abs b
z : 𝕊
zt : z ∈ t
xt : z = x
⊢ x ∈ t
Tactic:
rwa [← xt]
State after:
no goals

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}
⊢ IsOpen t
Tactic:
rw [isOpen_iff_eventually]
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}
⊢ ∀ x ∈ t, ∀ᶠ (y : 𝕊) in 𝓝 x, y ∈ t

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}
⊢ ∀ x ∈ t, ∀ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
Tactic:
intro e ⟨m, h⟩
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
⊢ ∀ᶠ (y : 𝕊) in 𝓝 e, y ∈ t

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

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

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

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