internlm/Lean-Github huggingface dataset:
Theorem: bottcherNontrivial
Proof 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}
Proof 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
Theorem: bottcherNontrivial
Proof 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
Proof 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
Theorem: bottcherNontrivial
Proof 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
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
⊢ Complex.abs b < 1
Tactic:
simp only [abs_bottcher, potential_lt_one, m, b]
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}
⊢ t = univ
Tactic:
refine IsClopen.eq_univ ?_ ⟨c, m, h⟩
Proof 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
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}
⊢ IsClopen t
Tactic:
constructor
Proof 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
Theorem: bottcherNontrivial
Proof 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]
Proof 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
Theorem: bottcherNontrivial
Proof 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
Proof 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
Theorem: bottcherNontrivial
Proof 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
Proof 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
Theorem: bottcherNontrivial
Proof 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]
Proof 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
Theorem: bottcherNontrivial
Proof 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
Proof 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
Theorem: bottcherNontrivial
Proof 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]
Proof 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
Theorem: bottcherNontrivial
Proof 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
Proof 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
Theorem: bottcherNontrivial
Proof 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
Proof 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
Theorem: bottcherNontrivial
Proof 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]
Proof 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
Theorem: bottcherNontrivial
Proof 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
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
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
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
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
Proof 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
Theorem: bottcherNontrivial
Proof 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
Proof 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
Theorem: bottcherNontrivial
Proof 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
Proof 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
Theorem: bottcherNontrivial
Proof 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 ⊢
Proof 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
Theorem: bottcherNontrivial
Proof 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)
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}
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
Proof 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
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}
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 ?_)
Proof 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
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}
x : 𝕊
e : ∃ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
xt : x ∉ t
⊢ ∀ x ∈ t, potential d x = Complex.abs b
Tactic:
intro z ⟨_, h⟩
Proof 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
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}
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]
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
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]
Proof 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
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
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, ?_⟩)
Proof 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
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
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
Proof 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
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
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 ⊢
Proof 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
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
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]
Proof state after:
no goals
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}
⊢ IsOpen t
Tactic:
rw [isOpen_iff_eventually]
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}
⊢ ∀ x ∈ t, ∀ᶠ (y : 𝕊) in 𝓝 x, y ∈ 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}
⊢ ∀ x ∈ t, ∀ᶠ (y : 𝕊) in 𝓝 x, y ∈ t
Tactic:
intro e ⟨m, h⟩
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
⊢ ∀ᶠ (y : 𝕊) in 𝓝 e, y ∈ t