internlm/Lean-Github huggingface dataset:
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 : ∃ᶠ (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
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)
m : ∃ᶠ (z : 𝕊) in 𝓝 x, potential d z < p ∧ (z, r z) ∈ t2
⊢ 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 : ∃ᶠ (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⟩
Proof 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
Theorem: bottcher_inj
Proof 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)]
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 = ∞
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 ↦ ?_))
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 : 𝕊
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
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 = ∞
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]
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 : 𝕊
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
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 = ∞
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
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 : 𝕊
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
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 = ∞
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⟩
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 : 𝕊
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
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 : 𝕊
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, ?_⟩
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 : 𝕊
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
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 : 𝕊
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
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 : 𝕊
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
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 : 𝕊
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
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 = ∞
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
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 : 𝕊
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)