internlm/Lean-Github huggingface dataset:
Theorem: sum_drop
Proof state before:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : HasSum (Stream'.cons (-f 0) f) (-f 0 + g)
⊢ HasSum (fun n => f (n + 1)) (g - f 0)
Tactic:
rw [HasSum]
Proof state after:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : HasSum (Stream'.cons (-f 0) f) (-f 0 + g)
⊢ Filter.Tendsto (fun s => s.sum fun b => f (b + 1)) atTop (𝓝 (g - f 0))
Theorem: sum_drop
Proof state before:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : HasSum (Stream'.cons (-f 0) f) (-f 0 + g)
⊢ Filter.Tendsto (fun s => s.sum fun b => f (b + 1)) atTop (𝓝 (g - f 0))
Tactic:
rw [neg_add_eq_sub, HasSum, ← tendsto_comp_push, ← tendsto_comp_push] at c
Proof state after:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : Filter.Tendsto (((fun s => s.sum fun b => Stream'.cons (-f 0) f b) ∘ push) ∘ push) atTop (𝓝 (g - f 0))
⊢ Filter.Tendsto (fun s => s.sum fun b => f (b + 1)) atTop (𝓝 (g - f 0))
Theorem: sum_drop
Proof state before:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : Filter.Tendsto (((fun s => s.sum fun b => Stream'.cons (-f 0) f b) ∘ push) ∘ push) atTop (𝓝 (g - f 0))
⊢ Filter.Tendsto (fun s => s.sum fun b => f (b + 1)) atTop (𝓝 (g - f 0))
Tactic:
have s : ((fun N : Finset ℕ ↦ N.sum fun n ↦ (Stream'.cons (-f 0) f) n) ∘ push) ∘ push =
    fun N : Finset ℕ ↦ N.sum fun n ↦ f (n + 1) := by
  clear c h g; apply funext; intro N; simp
  nth_rw 2 [← Stream'.eta f]
  simp only [←push_sum, Stream'.head, Stream'.tail, Stream'.get]
  abel
Proof state after:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : Filter.Tendsto (((fun s => s.sum fun b => Stream'.cons (-f 0) f b) ∘ push) ∘ push) atTop (𝓝 (g - f 0))
s : ((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push = fun N => N.sum fun n => f (n + 1)
⊢ Filter.Tendsto (fun s => s.sum fun b => f (b + 1)) atTop (𝓝 (g - f 0))
Theorem: sum_drop
Proof state before:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : Filter.Tendsto (((fun s => s.sum fun b => Stream'.cons (-f 0) f b) ∘ push) ∘ push) atTop (𝓝 (g - f 0))
s : ((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push = fun N => N.sum fun n => f (n + 1)
⊢ Filter.Tendsto (fun s => s.sum fun b => f (b + 1)) atTop (𝓝 (g - f 0))
Tactic:
rw [s] at c
Proof state after:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : Filter.Tendsto (fun N => N.sum fun n => f (n + 1)) atTop (𝓝 (g - f 0))
s : ((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push = fun N => N.sum fun n => f (n + 1)
⊢ Filter.Tendsto (fun s => s.sum fun b => f (b + 1)) atTop (𝓝 (g - f 0))
Theorem: sum_drop
Proof state before:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : Filter.Tendsto (fun N => N.sum fun n => f (n + 1)) atTop (𝓝 (g - f 0))
s : ((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push = fun N => N.sum fun n => f (n + 1)
⊢ Filter.Tendsto (fun s => s.sum fun b => f (b + 1)) atTop (𝓝 (g - f 0))
Tactic:
assumption
Proof state after:
no goals
Theorem: sum_drop
Proof state before:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
g : X
h : HasSum f g
c : Filter.Tendsto (((fun s => s.sum fun b => Stream'.cons (-f 0) f b) ∘ push) ∘ push) atTop (𝓝 (g - f 0))
⊢ ((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push = fun N => N.sum fun n => f (n + 1)
Tactic:
clear c h g
Proof state after:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
⊢ ((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push = fun N => N.sum fun n => f (n + 1)
Theorem: sum_drop
Proof state before:
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
⊢ ((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push = fun N => N.sum fun n => f (n + 1)
Tactic:
apply funext
Proof state after:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
⊢ ∀ (x : Finset ℕ), (((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push) x = x.sum fun n => f (n + 1)
Theorem: sum_drop
Proof state before:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
⊢ ∀ (x : Finset ℕ), (((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push) x = x.sum fun n => f (n + 1)
Tactic:
intro N
Proof state after:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
N : Finset ℕ
⊢ (((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push) N = N.sum fun n => f (n + 1)
Theorem: sum_drop
Proof state before:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
N : Finset ℕ
⊢ (((fun N => N.sum fun n => Stream'.cons (-f 0) f n) ∘ push) ∘ push) N = N.sum fun n => f (n + 1)
Tactic:
simp
Proof state after:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
N : Finset ℕ
⊢ ((push (push N)).sum fun n => Stream'.cons (-f 0) f n) = N.sum fun n => f (n + 1)
Theorem: sum_drop
Proof state before:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
N : Finset ℕ
⊢ ((push (push N)).sum fun n => Stream'.cons (-f 0) f n) = N.sum fun n => f (n + 1)
Tactic:
nth_rw 2 [← Stream'.eta f]
Proof state after:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
N : Finset ℕ
⊢ ((push (push N)).sum fun n => Stream'.cons (-f 0) (Stream'.cons (Stream'.head f) (Stream'.tail f)) n) =
    N.sum fun n => f (n + 1)
Theorem: sum_drop
Proof state before:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
N : Finset ℕ
⊢ ((push (push N)).sum fun n => Stream'.cons (-f 0) (Stream'.cons (Stream'.head f) (Stream'.tail f)) n) =
    N.sum fun n => f (n + 1)
Tactic:
simp only [←push_sum, Stream'.head, Stream'.tail, Stream'.get]
Proof state after:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
N : Finset ℕ
⊢ -f 0 + (f 0 + N.sum fun x => f (x + 1)) = N.sum fun x => f (x + 1)
Theorem: sum_drop
Proof state before:
case h
X : Type
inst✝ : NormedAddCommGroup X
f : ℕ → X
N : Finset ℕ
⊢ -f 0 + (f 0 + N.sum fun x => f (x + 1)) = N.sum fun x => f (x + 1)
Tactic:
abel
Proof state after:
no goals
Theorem: bottcher_inj
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ InjOn (bottcher d) (multibrotExt d)
Tactic:
by_contra bad
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
bad : ¬InjOn (bottcher d) (multibrotExt d)
⊢ False
Theorem: bottcher_inj
Proof 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
Proof 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
Theorem: bottcher_inj
Proof 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⟩
Proof 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
Theorem: bottcher_inj
Proof 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
Proof 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
Theorem: bottcher_inj
Proof 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]
Proof 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
Theorem: bottcher_inj
Proof 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}
Proof 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
Theorem: bottcher_inj
Proof 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
Proof 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
Theorem: bottcher_inj
Proof 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}
Proof 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
Theorem: bottcher_inj
Proof 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}
Proof 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
Theorem: bottcher_inj
Proof 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
Proof 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
Theorem: bottcher_inj
Proof 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
Proof 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
Theorem: bottcher_inj
Proof 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 _ _
Proof 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
Theorem: bottcher_inj
Proof 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 _ _
Proof 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
Theorem: bottcher_inj
Proof 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
Proof 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
Theorem: bottcher_inj
Proof 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
Proof 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
Theorem: bottcher_inj
Proof 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
Proof 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
Theorem: bottcher_inj
Proof 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
Proof 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
Theorem: bottcher_inj
Proof 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
Proof 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
Theorem: bottcher_inj
Proof 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
Proof 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
Theorem: bottcher_inj
Proof 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⟩
Proof 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
Theorem: bottcher_inj
Proof 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
Proof 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
Theorem: bottcher_inj
Proof 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
Proof 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