Theorem: bottcher_inj (Ray/Dynamics/Multibrot/Isomorphism.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ InjOn (bottcher d) (multibrotExt d)
Tactic:
by_contra bad
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
bad : ¬InjOn (bottcher d) (multibrotExt d)
⊢ False

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
bad : ¬InjOn (bottcher d) (multibrotExt d)
⊢ False
Tactic:
simp only [InjOn, not_forall, ← ne_eq] at bad
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
bad : ∃ x, ∃ (_ : x ∈ multibrotExt d), ∃ x_1, ∃ (_ : x_1 ∈ multibrotExt d) (_ : bottcher d x = bottcher d x_1), x ≠ x_1
⊢ False

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
bad : ∃ x, ∃ (_ : x ∈ multibrotExt d), ∃ x_1, ∃ (_ : x_1 ∈ multibrotExt d) (_ : bottcher d x = bottcher d x_1), x ≠ x_1
⊢ False
Tactic:
rcases bad with ⟨x, xm, y, ym, bxy, xy⟩
State after:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
⊢ False

State before:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
⊢ False
Tactic:
generalize hb : potential d x = b
State after:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
b : ℝ
hb : potential d x = b
⊢ False

State before:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
b : ℝ
hb : potential d x = b
⊢ False
Tactic:
have b1 : b < 1 := by rwa [← hb, potential_lt_one]
State after:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
b : ℝ
hb : potential d x = b
b1 : b < 1
⊢ False

State before:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
b : ℝ
hb : potential d x = b
b1 : b < 1
⊢ False
Tactic:
set u := {c | potential d c ≤ b}
State after:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
b : ℝ
hb : potential d x = b
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
⊢ False

State before:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
b : ℝ
hb : potential d x = b
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
⊢ False
Tactic:
set t0 := u ×ˢ u
State after:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
b : ℝ
hb : potential d x = b
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
⊢ False

State before:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
b : ℝ
hb : potential d x = b
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
⊢ False
Tactic:
set t1 := {q : 𝕊 × 𝕊 | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
State after:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
b : ℝ
hb : potential d x = b
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
⊢ False

State before:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
b : ℝ
hb : potential d x = b
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
⊢ False
Tactic:
set t2 := {q : 𝕊 × 𝕊 | q.1 ≠ q.2 ∧ q ∈ t1}
State after:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
b : ℝ
hb : potential d x = b
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
⊢ False

State before:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
b : ℝ
hb : potential d x = b
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
⊢ False
Tactic:
clear x xm y ym bxy xy hb
State after:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
⊢ False

State before:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
⊢ False
Tactic:
have ue : u ⊆ multibrotExt d := by intro c m; rw [← potential_lt_one]; exact lt_of_le_of_lt m b1
State after:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
⊢ False

State before:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
⊢ False
Tactic:
have t01 : t1 ⊆ t0 := inter_subset_right _ _
State after:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
⊢ False

State before:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
⊢ False
Tactic:
have t12 : t2 ⊆ t1 := inter_subset_right _ _
State after:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
⊢ False

State before:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
⊢ False
Tactic:
have uc : IsClosed u := isClosed_le potential_continuous continuous_const
State after:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
⊢ False

State before:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
⊢ False
Tactic:
have t0c : IsClosed t0 := uc.prod uc
State after:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
⊢ False

State before:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
⊢ False
Tactic:
have t12' : closure t2 ⊆ t1 := by rw [← t1c.closure_eq]; exact closure_mono t12
State after:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
⊢ False

State before:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
⊢ False
Tactic:
have t2c' : IsCompact (closure t2) := isClosed_closure.isCompact
State after:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
⊢ False

State before:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
⊢ False
Tactic:
have t2ne' : (closure t2).Nonempty := t2ne.closure
State after:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
⊢ False

State before:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
⊢ False
Tactic:
have pc : Continuous fun q : 𝕊 × 𝕊 ↦ potential d q.1 := potential_continuous.comp continuous_fst
State after:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
⊢ False

State before:
case intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
⊢ False
Tactic:
rcases t2c'.exists_isMinOn t2ne' pc.continuousOn with ⟨⟨x, y⟩, m2, min⟩
State after:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
min : IsMinOn (fun q => potential d q.1) (closure t2) (x, y)
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
min : IsMinOn (fun q => potential d q.1) (closure t2) (x, y)
⊢ False
Tactic:
simp only [isMinOn_iff] at min
State after:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
min : ∀ x_1 ∈ closure t2, potential d x ≤ potential d x_1.1
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
min : ∀ x_1 ∈ closure t2, potential d x ≤ potential d x_1.1
⊢ False
Tactic:
generalize xp : potential d x = p
State after:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
min : ∀ x_1 ∈ closure t2, potential d x ≤ potential d x_1.1
p : ℝ
xp : potential d x = p
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
min : ∀ x_1 ∈ closure t2, potential d x ≤ potential d x_1.1
p : ℝ
xp : potential d x = p
⊢ False
Tactic:
rw [xp] at min
State after:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
⊢ False
Tactic:
have m1 := t12' m2
State after:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
⊢ False
Tactic:
have pb : p ≤ b := by rw [← xp]; exact m1.2.1
State after:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
⊢ False
Tactic:
have xm : x ∈ multibrotExt d := ue m1.2.1
State after:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
⊢ False
Tactic:
have ym : y ∈ multibrotExt d := ue m1.2.2
State after:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
⊢ False
Tactic:
have yp : potential d y = p := by rw [← abs_bottcher, ← m1.1, abs_bottcher, xp]
State after:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
⊢ False
Tactic:
have p0i : p = 0 → x = ∞ ∧ y = ∞ := by intro p0; rw [p0, potential_eq_zero] at xp yp; use xp, yp
State after:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.mk.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
⊢ False
Tactic:
by_cases xy : x ≠ y
State after:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
⊢ False

case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : ¬x ≠ y
⊢ False

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : ¬x ≠ y
⊢ False
Tactic:
simp only [not_not] at xy
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x = y
⊢ False

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x = y
⊢ False
Tactic:
rw [← xy] at m1 m2 p0i
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ x = ∞
xy : x = y
⊢ False

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ x = ∞
xy : x = y
⊢ False
Tactic:
clear xy ym yp y
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
⊢ False

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
⊢ False
Tactic:
have db : mfderiv I I (bottcher d) x = 0 := by
  contrapose m2; simp only [mem_closure_iff_frequently, Filter.not_frequently]
  refine ((bottcherHolomorphic d _ xm).local_inj m2).mp (eventually_of_forall ?_)
  intro ⟨x, y⟩ inj ⟨xy, e, _⟩; simp only at xy e inj; exact xy (inj e)
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
⊢ False

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
⊢ False
Tactic:
by_cases p0 : p ≠ 0
State after:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : p ≠ 0
⊢ False

case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : ¬p ≠ 0
⊢ False

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
b : ℝ
hb : potential d x = b
⊢ b < 1
Tactic:
rwa [← hb, potential_lt_one]
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
b : ℝ
hb : potential d x = b
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
⊢ t2.Nonempty
Tactic:
refine ⟨⟨x, y⟩, xy, bxy, ?_, ?_⟩
State after:
case refine_1
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
b : ℝ
hb : potential d x = b
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
⊢ (x, y).1 ∈ u

case refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
b : ℝ
hb : potential d x = b
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
⊢ (x, y).2 ∈ u

State before:
case refine_1
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
b : ℝ
hb : potential d x = b
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
⊢ (x, y).1 ∈ u
Tactic:
simp only [mem_setOf, ← hb, le_refl, u]
State after:
no goals

State before:
case refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : 𝕊
xm : x ∈ multibrotExt d
y : 𝕊
ym : y ∈ multibrotExt d
bxy : bottcher d x = bottcher d y
xy : x ≠ y
b : ℝ
hb : potential d x = b
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
⊢ (x, y).2 ∈ u
Tactic:
simp only [mem_setOf, ← hb, ← abs_bottcher, bxy, le_refl, u]
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
⊢ u ⊆ multibrotExt d
Tactic:
intro c m
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
c : 𝕊
m : c ∈ u
⊢ c ∈ multibrotExt d

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
c : 𝕊
m : c ∈ u
⊢ c ∈ multibrotExt d
Tactic:
rw [← potential_lt_one]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
c : 𝕊
m : c ∈ u
⊢ potential d c < 1

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
c : 𝕊
m : c ∈ u
⊢ 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)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
⊢ IsClosed t1
Tactic:
rw [isClosed_iff_frequently]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
⊢ ∀ (x : 𝕊 × 𝕊), (∃ᶠ (y : 𝕊 × 𝕊) in 𝓝 x, y ∈ t1) → x ∈ t1

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
⊢ ∀ (x : 𝕊 × 𝕊), (∃ᶠ (y : 𝕊 × 𝕊) in 𝓝 x, y ∈ t1) → x ∈ t1
Tactic:
intro ⟨x, y⟩ f
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
x y : 𝕊
f : ∃ᶠ (y : 𝕊 × 𝕊) in 𝓝 (x, y), y ∈ t1
⊢ (x, y) ∈ t1

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
x y : 𝕊
f : ∃ᶠ (y : 𝕊 × 𝕊) in 𝓝 (x, y), y ∈ t1
⊢ (x, y) ∈ t1
Tactic:
have m0 : (x, y) ∈ t0 :=
  Filter.Frequently.mem_of_closed (f.mp (eventually_of_forall fun _ m ↦ t01 m)) t0c
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
x y : 𝕊
f : ∃ᶠ (y : 𝕊 × 𝕊) in 𝓝 (x, y), y ∈ t1
m0 : (x, y) ∈ t0
⊢ (x, y) ∈ t1

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
x y : 𝕊
f : ∃ᶠ (y : 𝕊 × 𝕊) in 𝓝 (x, y), y ∈ t1
m0 : (x, y) ∈ t0
⊢ (x, y) ∈ t1
Tactic:
refine ⟨tendsto_nhds_unique_of_frequently_eq ?_ ?_
  (f.mp (eventually_of_forall fun _ m ↦ m.1)), m0⟩
State after:
case refine_1
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
x y : 𝕊
f : ∃ᶠ (y : 𝕊 × 𝕊) in 𝓝 (x, y), y ∈ t1
m0 : (x, y) ∈ t0
⊢ Tendsto (fun x => bottcher d x.1) (𝓝 (x, y)) (𝓝 (bottcher d (x, y).1))

case refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
x y : 𝕊
f : ∃ᶠ (y : 𝕊 × 𝕊) in 𝓝 (x, y), y ∈ t1
m0 : (x, y) ∈ t0
⊢ Tendsto (fun x => bottcher d x.2) (𝓝 (x, y)) (𝓝 (bottcher d (x, y).2))

State before:
case refine_1
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
x y : 𝕊
f : ∃ᶠ (y : 𝕊 × 𝕊) in 𝓝 (x, y), y ∈ t1
m0 : (x, y) ∈ t0
⊢ Tendsto (fun x => bottcher d x.1) (𝓝 (x, y)) (𝓝 (bottcher d (x, y).1))
Tactic:
exact (bottcherHolomorphic d _ (ue m0.1)).continuousAt.comp continuousAt_fst
State after:
no goals

State before:
case refine_2
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
x y : 𝕊
f : ∃ᶠ (y : 𝕊 × 𝕊) in 𝓝 (x, y), y ∈ t1
m0 : (x, y) ∈ t0
⊢ Tendsto (fun x => bottcher d x.2) (𝓝 (x, y)) (𝓝 (bottcher d (x, y).2))
Tactic:
exact (bottcherHolomorphic d _ (ue m0.2)).continuousAt.comp continuousAt_snd
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
⊢ closure t2 ⊆ t1
Tactic:
rw [← t1c.closure_eq]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
⊢ closure t2 ⊆ closure t1

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
⊢ closure t2 ⊆ closure t1
Tactic:
exact closure_mono t12
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
⊢ p ≤ b
Tactic:
rw [← xp]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
⊢ potential d x ≤ b

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
⊢ potential d x ≤ b
Tactic:
exact m1.2.1
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
⊢ potential d y = p
Tactic:
rw [← abs_bottcher, ← m1.1, abs_bottcher, xp]
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
⊢ p = 0 → x = ∞ ∧ y = ∞
Tactic:
intro p0
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0 : p = 0
⊢ x = ∞ ∧ y = ∞

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0 : p = 0
⊢ x = ∞ ∧ y = ∞
Tactic:
rw [p0, potential_eq_zero] at xp yp
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : x = ∞
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : y = ∞
p0 : p = 0
⊢ x = ∞ ∧ y = ∞

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : x = ∞
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : y = ∞
p0 : p = 0
⊢ x = ∞ ∧ y = ∞
Tactic:
use xp, yp
State after:
no goals

State before:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
⊢ False
Tactic:
have p0 : p ≠ 0 := by
  contrapose xy; simp only [not_not] at xy ⊢; rcases p0i xy with ⟨xi, yi⟩; rw [xi, yi]
State after:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
⊢ False

State before:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
⊢ False
Tactic:
have f : ∃ᶠ q : ℂ × ℂ in Filter.map
    (fun q : 𝕊 × 𝕊 ↦ (bottcher d q.1, bottcher d q.2)) (𝓝 (x, y)),
    q.1 = q.2 ∧ abs q.1 < p := by
  rw [nhds_prod_eq, ← Filter.prod_map_map_eq, ← (bottcherNontrivial xm).nhds_eq_map_nhds, ←
    (bottcherNontrivial ym).nhds_eq_map_nhds, m1.1, ← nhds_prod_eq]
  apply (continuous_id.prod_mk continuous_id).continuousAt.frequently
  simp only [eq_self_iff_true, true_and_iff, ← yp, ← abs_bottcher]; apply frequently_smaller
  rw [← Complex.abs.ne_zero_iff, abs_bottcher, yp]; exact p0
State after:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
f : ∃ᶠ (q : ℂ × ℂ) in Filter.map (fun q => (bottcher d q.1, bottcher d q.2)) (𝓝 (x, y)), q.1 = q.2 ∧ Complex.abs q.1 < p
⊢ False

State before:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
f : ∃ᶠ (q : ℂ × ℂ) in Filter.map (fun q => (bottcher d q.1, bottcher d q.2)) (𝓝 (x, y)), q.1 = q.2 ∧ Complex.abs q.1 < p
⊢ False
Tactic:
simp only [Filter.frequently_map] at f
State after:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
f : ∃ᶠ (a : 𝕊 × 𝕊) in 𝓝 (x, y), bottcher d a.1 = bottcher d a.2 ∧ Complex.abs (bottcher d a.1) < p
⊢ False

State before:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
f : ∃ᶠ (a : 𝕊 × 𝕊) in 𝓝 (x, y), bottcher d a.1 = bottcher d a.2 ∧ Complex.abs (bottcher d a.1) < p
⊢ False
Tactic:
rcases(f.and_eventually (Ne.eventually_ne xy)).exists with ⟨⟨v, w⟩, ⟨bvw, pv⟩, vw⟩
State after:
case pos.intro.mk.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
f : ∃ᶠ (a : 𝕊 × 𝕊) in 𝓝 (x, y), bottcher d a.1 = bottcher d a.2 ∧ Complex.abs (bottcher d a.1) < p
v w : 𝕊
vw : (v, w).1 ≠ (v, w).2
bvw : bottcher d (v, w).1 = bottcher d (v, w).2
pv : Complex.abs (bottcher d (v, w).1) < p
⊢ False

State before:
case pos.intro.mk.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
f : ∃ᶠ (a : 𝕊 × 𝕊) in 𝓝 (x, y), bottcher d a.1 = bottcher d a.2 ∧ Complex.abs (bottcher d a.1) < p
v w : 𝕊
vw : (v, w).1 ≠ (v, w).2
bvw : bottcher d (v, w).1 = bottcher d (v, w).2
pv : Complex.abs (bottcher d (v, w).1) < p
⊢ False
Tactic:
simp only [not_lt, abs_bottcher] at vw bvw pv ⊢
State after:
case pos.intro.mk.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
f : ∃ᶠ (a : 𝕊 × 𝕊) in 𝓝 (x, y), bottcher d a.1 = bottcher d a.2 ∧ Complex.abs (bottcher d a.1) < p
v w : 𝕊
vw : v ≠ w
bvw : bottcher d v = bottcher d w
pv : potential d v < p
⊢ False

State before:
case pos.intro.mk.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
f : ∃ᶠ (a : 𝕊 × 𝕊) in 𝓝 (x, y), bottcher d a.1 = bottcher d a.2 ∧ Complex.abs (bottcher d a.1) < p
v w : 𝕊
vw : v ≠ w
bvw : bottcher d v = bottcher d w
pv : potential d v < p
⊢ False
Tactic:
have pw : potential d w < p := by rwa [← abs_bottcher, ← bvw, abs_bottcher]
State after:
case pos.intro.mk.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
f : ∃ᶠ (a : 𝕊 × 𝕊) in 𝓝 (x, y), bottcher d a.1 = bottcher d a.2 ∧ Complex.abs (bottcher d a.1) < p
v w : 𝕊
vw : v ≠ w
bvw : bottcher d v = bottcher d w
pv : potential d v < p
pw : potential d w < p
⊢ False

State before:
case pos.intro.mk.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
f : ∃ᶠ (a : 𝕊 × 𝕊) in 𝓝 (x, y), bottcher d a.1 = bottcher d a.2 ∧ Complex.abs (bottcher d a.1) < p
v w : 𝕊
vw : v ≠ w
bvw : bottcher d v = bottcher d w
pv : potential d v < p
pw : potential d w < p
⊢ False
Tactic:
have m : (v, w) ∈ t2 := ⟨vw, bvw, le_trans pv.le pb, le_trans pw.le pb⟩
State after:
case pos.intro.mk.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
f : ∃ᶠ (a : 𝕊 × 𝕊) in 𝓝 (x, y), bottcher d a.1 = bottcher d a.2 ∧ Complex.abs (bottcher d a.1) < p
v w : 𝕊
vw : v ≠ w
bvw : bottcher d v = bottcher d w
pv : potential d v < p
pw : potential d w < p
m : (v, w) ∈ t2
⊢ False

State before:
case pos.intro.mk.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
f : ∃ᶠ (a : 𝕊 × 𝕊) in 𝓝 (x, y), bottcher d a.1 = bottcher d a.2 ∧ Complex.abs (bottcher d a.1) < p
v w : 𝕊
vw : v ≠ w
bvw : bottcher d v = bottcher d w
pv : potential d v < p
pw : potential d w < p
m : (v, w) ∈ t2
⊢ False
Tactic:
contrapose pv
State after:
case pos.intro.mk.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
f : ∃ᶠ (a : 𝕊 × 𝕊) in 𝓝 (x, y), bottcher d a.1 = bottcher d a.2 ∧ Complex.abs (bottcher d a.1) < p
v w : 𝕊
vw : v ≠ w
bvw : bottcher d v = bottcher d w
pw : potential d w < p
m : (v, w) ∈ t2
pv : ¬False
⊢ ¬potential d v < p

State before:
case pos.intro.mk.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
f : ∃ᶠ (a : 𝕊 × 𝕊) in 𝓝 (x, y), bottcher d a.1 = bottcher d a.2 ∧ Complex.abs (bottcher d a.1) < p
v w : 𝕊
vw : v ≠ w
bvw : bottcher d v = bottcher d w
pw : potential d w < p
m : (v, w) ∈ t2
pv : ¬False
⊢ ¬potential d v < p
Tactic:
clear pv
State after:
case pos.intro.mk.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
f : ∃ᶠ (a : 𝕊 × 𝕊) in 𝓝 (x, y), bottcher d a.1 = bottcher d a.2 ∧ Complex.abs (bottcher d a.1) < p
v w : 𝕊
vw : v ≠ w
bvw : bottcher d v = bottcher d w
pw : potential d w < p
m : (v, w) ∈ t2
⊢ ¬potential d v < p

State before:
case pos.intro.mk.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
f : ∃ᶠ (a : 𝕊 × 𝕊) in 𝓝 (x, y), bottcher d a.1 = bottcher d a.2 ∧ Complex.abs (bottcher d a.1) < p
v w : 𝕊
vw : v ≠ w
bvw : bottcher d v = bottcher d w
pw : potential d w < p
m : (v, w) ∈ t2
⊢ ¬potential d v < p
Tactic:
simp only [not_lt]
State after:
case pos.intro.mk.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
f : ∃ᶠ (a : 𝕊 × 𝕊) in 𝓝 (x, y), bottcher d a.1 = bottcher d a.2 ∧ Complex.abs (bottcher d a.1) < p
v w : 𝕊
vw : v ≠ w
bvw : bottcher d v = bottcher d w
pw : potential d w < p
m : (v, w) ∈ t2
⊢ p ≤ potential d v

State before:
case pos.intro.mk.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
f : ∃ᶠ (a : 𝕊 × 𝕊) in 𝓝 (x, y), bottcher d a.1 = bottcher d a.2 ∧ Complex.abs (bottcher d a.1) < p
v w : 𝕊
vw : v ≠ w
bvw : bottcher d v = bottcher d w
pw : potential d w < p
m : (v, w) ∈ t2
⊢ p ≤ potential d v
Tactic:
exact min ⟨v, w⟩ (subset_closure m)
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
⊢ p ≠ 0
Tactic:
contrapose xy
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : ¬p ≠ 0
⊢ ¬x ≠ y

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : ¬p ≠ 0
⊢ ¬x ≠ y
Tactic:
simp only [not_not] at xy ⊢
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : p = 0
⊢ x = y

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : p = 0
⊢ x = y
Tactic:
rcases p0i xy with ⟨xi, yi⟩
State after:
case intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : p = 0
xi : x = ∞
yi : y = ∞
⊢ x = y

State before:
case intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : p = 0
xi : x = ∞
yi : y = ∞
⊢ x = y
Tactic:
rw [xi, yi]
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
⊢ ∃ᶠ (q : ℂ × ℂ) in Filter.map (fun q => (bottcher d q.1, bottcher d q.2)) (𝓝 (x, y)), q.1 = q.2 ∧ Complex.abs q.1 < p
Tactic:
rw [nhds_prod_eq, ← Filter.prod_map_map_eq, ← (bottcherNontrivial xm).nhds_eq_map_nhds, ←
  (bottcherNontrivial ym).nhds_eq_map_nhds, m1.1, ← nhds_prod_eq]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
⊢ ∃ᶠ (q : ℂ × ℂ) in 𝓝 (bottcher d (x, y).2, bottcher d y), q.1 = q.2 ∧ Complex.abs q.1 < p

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
⊢ ∃ᶠ (q : ℂ × ℂ) in 𝓝 (bottcher d (x, y).2, bottcher d y), q.1 = q.2 ∧ Complex.abs q.1 < p
Tactic:
apply (continuous_id.prod_mk continuous_id).continuousAt.frequently
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
⊢ ∃ᶠ (x : ℂ) in 𝓝 (fill (bottcher' d) 0 (x, y).2), (id x, id x).1 = (id x, id x).2 ∧ Complex.abs (id x, id x).1 < p

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
⊢ ∃ᶠ (x : ℂ) in 𝓝 (fill (bottcher' d) 0 (x, y).2), (id x, id x).1 = (id x, id x).2 ∧ Complex.abs (id x, id x).1 < p
Tactic:
simp only [eq_self_iff_true, true_and_iff, ← yp, ← abs_bottcher]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
⊢ ∃ᶠ (x : ℂ) in 𝓝 (fill (bottcher' d) 0 y), Complex.abs (id x) < Complex.abs (bottcher d y)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
⊢ ∃ᶠ (x : ℂ) in 𝓝 (fill (bottcher' d) 0 y), Complex.abs (id x) < Complex.abs (bottcher d y)
Tactic:
apply frequently_smaller
State after:
case z0
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
⊢ bottcher d y ≠ 0

State before:
case z0
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
⊢ bottcher d y ≠ 0
Tactic:
rw [← Complex.abs.ne_zero_iff, abs_bottcher, yp]
State after:
case z0
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
⊢ p ≠ 0

State before:
case z0
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
⊢ p ≠ 0
Tactic:
exact p0
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x y : 𝕊
m2 : (x, y) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, y) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
ym : y ∈ multibrotExt d
yp : potential d y = p
p0i : p = 0 → x = ∞ ∧ y = ∞
xy : x ≠ y
p0 : p ≠ 0
f : ∃ᶠ (a : 𝕊 × 𝕊) in 𝓝 (x, y), bottcher d a.1 = bottcher d a.2 ∧ Complex.abs (bottcher d a.1) < p
v w : 𝕊
vw : v ≠ w
bvw : bottcher d v = bottcher d w
pv : potential d v < p
⊢ potential d w < p
Tactic:
rwa [← abs_bottcher, ← bvw, abs_bottcher]
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
⊢ mfderiv I I (bottcher d) x = 0
Tactic:
contrapose m2
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
m2 : ¬mfderiv I I (bottcher d) x = 0
⊢ (x, x) ∉ closure t2

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
m2 : ¬mfderiv I I (bottcher d) x = 0
⊢ (x, x) ∉ closure t2
Tactic:
simp only [mem_closure_iff_frequently, Filter.not_frequently]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
m2 : ¬mfderiv I I (bottcher d) x = 0
⊢ ∀ᶠ (x : 𝕊 × 𝕊) in 𝓝 (x, x), x ∉ t2

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
m2 : ¬mfderiv I I (bottcher d) x = 0
⊢ ∀ᶠ (x : 𝕊 × 𝕊) in 𝓝 (x, x), x ∉ t2
Tactic:
refine ((bottcherHolomorphic d _ xm).local_inj m2).mp (eventually_of_forall ?_)
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
m2 : ¬mfderiv I I (bottcher d) x = 0
⊢ ∀ (x : 𝕊 × 𝕊), (bottcher d x.1 = bottcher d x.2 → x.1 = x.2) → x ∉ t2

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
m2 : ¬mfderiv I I (bottcher d) x = 0
⊢ ∀ (x : 𝕊 × 𝕊), (bottcher d x.1 = bottcher d x.2 → x.1 = x.2) → x ∉ t2
Tactic:
intro ⟨x, y⟩ inj ⟨xy, e, _⟩
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x✝ : 𝕊
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x✝ = p
m1 : (x✝, x✝) ∈ t1
pb : p ≤ b
xm : x✝ ∈ multibrotExt d
p0i : p = 0 → x✝ = ∞ ∧ x✝ = ∞
m2 : ¬mfderiv I I (bottcher d) x✝ = 0
x y : 𝕊
inj : bottcher d (x, y).1 = bottcher d (x, y).2 → (x, y).1 = (x, y).2
xy : (x, y).1 ≠ (x, y).2
e : bottcher d (x, y).1 = bottcher d (x, y).2
right✝ : (x, y) ∈ t0
⊢ False

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x✝ : 𝕊
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x✝ = p
m1 : (x✝, x✝) ∈ t1
pb : p ≤ b
xm : x✝ ∈ multibrotExt d
p0i : p = 0 → x✝ = ∞ ∧ x✝ = ∞
m2 : ¬mfderiv I I (bottcher d) x✝ = 0
x y : 𝕊
inj : bottcher d (x, y).1 = bottcher d (x, y).2 → (x, y).1 = (x, y).2
xy : (x, y).1 ≠ (x, y).2
e : bottcher d (x, y).1 = bottcher d (x, y).2
right✝ : (x, y) ∈ t0
⊢ False
Tactic:
simp only at xy e inj
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x✝ : 𝕊
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x✝ = p
m1 : (x✝, x✝) ∈ t1
pb : p ≤ b
xm : x✝ ∈ multibrotExt d
p0i : p = 0 → x✝ = ∞ ∧ x✝ = ∞
m2 : ¬mfderiv I I (bottcher d) x✝ = 0
x y : 𝕊
inj : bottcher d x = bottcher d y → x = y
xy : x ≠ y
e : bottcher d x = bottcher d y
right✝ : (x, y) ∈ t0
⊢ False

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x✝ : 𝕊
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x✝ = p
m1 : (x✝, x✝) ∈ t1
pb : p ≤ b
xm : x✝ ∈ multibrotExt d
p0i : p = 0 → x✝ = ∞ ∧ x✝ = ∞
m2 : ¬mfderiv I I (bottcher d) x✝ = 0
x y : 𝕊
inj : bottcher d x = bottcher d y → x = y
xy : x ≠ y
e : bottcher d x = bottcher d y
right✝ : (x, y) ∈ t0
⊢ False
Tactic:
exact xy (inj e)
State after:
no goals

State before:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : p ≠ 0
⊢ False
Tactic:
rcases not_local_inj_of_mfderiv_zero (bottcherHolomorphic d _ xm) db with ⟨r, ra, rx, e⟩
State after:
case pos.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : p ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e : ∀ᶠ (z : 𝕊) in 𝓝[≠] x, r z ≠ z ∧ bottcher d (r z) = bottcher d z
⊢ False

State before:
case pos.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : p ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e : ∀ᶠ (z : 𝕊) in 𝓝[≠] x, r z ≠ z ∧ bottcher d (r z) = bottcher d z
⊢ False
Tactic:
simp only [eventually_nhdsWithin_iff, mem_compl_singleton_iff] at e
State after:
case pos.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : p ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
⊢ False

State before:
case pos.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : p ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
⊢ False
Tactic:
rw [← xp, ← abs_bottcher, Complex.abs.ne_zero_iff] at p0
State after:
case pos.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
⊢ False

State before:
case pos.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
⊢ False
Tactic:
have h := frequently_smaller p0
State after:
case pos.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (w : ℂ) in 𝓝 (bottcher d x), Complex.abs w < Complex.abs (bottcher d x)
⊢ False

State before:
case pos.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (w : ℂ) in 𝓝 (bottcher d x), Complex.abs w < Complex.abs (bottcher d x)
⊢ False
Tactic:
rw [(bottcherNontrivial xm).nhds_eq_map_nhds, Filter.frequently_map] at h
State after:
case pos.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
⊢ False

State before:
case pos.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
⊢ False
Tactic:
have m : ∃ᶠ z in 𝓝 x, potential d z < p ∧ (z, r z) ∈ t2 := by
  refine h.mp (e.mp (eventually_of_forall fun z e lt ↦ ?_))
  have zx : z ≠ x := by
    contrapose lt; simp only [not_not, not_lt] at lt ⊢; simp only [lt, le_refl]
  rw [abs_bottcher, abs_bottcher, xp] at lt
  rcases e zx with ⟨rz, e⟩
  refine ⟨lt, rz.symm, e.symm, le_trans lt.le pb, ?_⟩
  rw [← abs_bottcher, ← e, abs_bottcher] at lt; exact le_trans lt.le pb
State after:
case pos.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
m : ∃ᶠ (z : 𝕊) in 𝓝 x, potential d z < p ∧ (z, r z) ∈ t2
⊢ False

State before:
case pos.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
m : ∃ᶠ (z : 𝕊) in 𝓝 x, potential d z < p ∧ (z, r z) ∈ t2
⊢ False
Tactic:
rcases m.exists with ⟨y, yp, m⟩
State after:
case pos.intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
m✝ : ∃ᶠ (z : 𝕊) in 𝓝 x, potential d z < p ∧ (z, r z) ∈ t2
y : 𝕊
yp : potential d y < p
m : (y, r y) ∈ t2
⊢ False

State before:
case pos.intro.intro.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
m✝ : ∃ᶠ (z : 𝕊) in 𝓝 x, potential d z < p ∧ (z, r z) ∈ t2
y : 𝕊
yp : potential d y < p
m : (y, r y) ∈ t2
⊢ False
Tactic:
linarith [min _ (subset_closure m)]
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
⊢ ∃ᶠ (z : 𝕊) in 𝓝 x, potential d z < p ∧ (z, r z) ∈ t2
Tactic:
refine h.mp (e.mp (eventually_of_forall fun z e lt ↦ ?_))
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : Complex.abs (bottcher d z) < Complex.abs (bottcher d x)
⊢ potential d z < p ∧ (z, r z) ∈ t2

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : Complex.abs (bottcher d z) < Complex.abs (bottcher d x)
⊢ potential d z < p ∧ (z, r z) ∈ t2
Tactic:
have zx : z ≠ x := by
  contrapose lt; simp only [not_not, not_lt] at lt ⊢; simp only [lt, le_refl]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : Complex.abs (bottcher d z) < Complex.abs (bottcher d x)
zx : z ≠ x
⊢ potential d z < p ∧ (z, r z) ∈ t2

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : Complex.abs (bottcher d z) < Complex.abs (bottcher d x)
zx : z ≠ x
⊢ potential d z < p ∧ (z, r z) ∈ t2
Tactic:
rw [abs_bottcher, abs_bottcher, xp] at lt
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : potential d z < p
zx : z ≠ x
⊢ potential d z < p ∧ (z, r z) ∈ t2

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : potential d z < p
zx : z ≠ x
⊢ potential d z < p ∧ (z, r z) ∈ t2
Tactic:
rcases e zx with ⟨rz, e⟩
State after:
case intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝¹ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e✝ : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : potential d z < p
zx : z ≠ x
rz : r z ≠ z
e : bottcher d (r z) = bottcher d z
⊢ potential d z < p ∧ (z, r z) ∈ t2

State before:
case intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝¹ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e✝ : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : potential d z < p
zx : z ≠ x
rz : r z ≠ z
e : bottcher d (r z) = bottcher d z
⊢ potential d z < p ∧ (z, r z) ∈ t2
Tactic:
refine ⟨lt, rz.symm, e.symm, le_trans lt.le pb, ?_⟩
State after:
case intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝¹ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e✝ : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : potential d z < p
zx : z ≠ x
rz : r z ≠ z
e : bottcher d (r z) = bottcher d z
⊢ (z, r z).2 ∈ u

State before:
case intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝¹ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e✝ : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : potential d z < p
zx : z ≠ x
rz : r z ≠ z
e : bottcher d (r z) = bottcher d z
⊢ (z, r z).2 ∈ u
Tactic:
rw [← abs_bottcher, ← e, abs_bottcher] at lt
State after:
case intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝¹ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e✝ : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : potential d (r z) < p
zx : z ≠ x
rz : r z ≠ z
e : bottcher d (r z) = bottcher d z
⊢ (z, r z).2 ∈ u

State before:
case intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝¹ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e✝ : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : potential d (r z) < p
zx : z ≠ x
rz : r z ≠ z
e : bottcher d (r z) = bottcher d z
⊢ (z, r z).2 ∈ u
Tactic:
exact le_trans lt.le pb
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : Complex.abs (bottcher d z) < Complex.abs (bottcher d x)
⊢ z ≠ x
Tactic:
contrapose lt
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : ¬z ≠ x
⊢ ¬Complex.abs (bottcher d z) < Complex.abs (bottcher d x)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : ¬z ≠ x
⊢ ¬Complex.abs (bottcher d z) < Complex.abs (bottcher d x)
Tactic:
simp only [not_not, not_lt] at lt ⊢
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : z = x
⊢ Complex.abs (bottcher d x) ≤ Complex.abs (bottcher d z)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : z = x
⊢ Complex.abs (bottcher d x) ≤ Complex.abs (bottcher d z)
Tactic:
simp only [lt, le_refl]
State after:
no goals

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : ¬p ≠ 0
⊢ False
Tactic:
simp only [not_not] at p0
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : p = 0
⊢ False

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : p = 0
⊢ False
Tactic:
rw [(p0i p0).1] at db
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) ∞ = 0
p0 : p = 0
⊢ False

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) ∞ = 0
p0 : p = 0
⊢ False
Tactic:
exact bottcher_mfderiv_inf_ne_zero db
State after:
no goals