internlm/Lean-Github huggingface dataset:
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 y), Complex.abs (id x) < Complex.abs (bottcher d y)
Tactic:
apply frequently_smaller
Proof 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
Theorem: bottcher_inj
Proof 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]
Proof 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
Theorem: bottcher_inj
Proof 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
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
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]
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 : 𝕊
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
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 : 𝕊
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
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 : 𝕊
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]
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 : 𝕊
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
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 : 𝕊
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 ?_)
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 : 𝕊
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
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 : 𝕊
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, _⟩
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✝ : 𝕊
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
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✝ : 𝕊
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
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✝ : 𝕊
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
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✝ : 𝕊
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)
Proof state after:
no goals
Theorem: bottcher_inj
Proof 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⟩
Proof 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
Theorem: bottcher_inj
Proof 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
Proof 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
Theorem: bottcher_inj
Proof 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
Proof 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
Theorem: bottcher_inj
Proof 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
Proof 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
Theorem: bottcher_inj
Proof 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
Proof 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