internlm/Lean-Github huggingface dataset:
Theorem: bottcher_inj
Proof 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 ⊢
Proof 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
Theorem: bottcher_inj
Proof 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]
Proof 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
Theorem: bottcher_inj
Proof 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⟩
Proof 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
Theorem: bottcher_inj
Proof 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
Proof 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
Theorem: bottcher_inj
Proof 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
Proof 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
Theorem: bottcher_inj
Proof 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]
Proof 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
Theorem: bottcher_inj
Proof 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)
Proof state after:
no goals
Theorem: bottcher_inj
Proof 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
Proof 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
Theorem: bottcher_inj
Proof 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 ⊢
Proof 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
Theorem: bottcher_inj
Proof 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⟩
Proof 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
Theorem: bottcher_inj
Proof 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]
Proof state after:
no goals
Theorem: bottcher_inj
Proof 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]
Proof 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
Theorem: bottcher_inj
Proof 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
Proof 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
Theorem: bottcher_inj
Proof 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]
Proof 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)