internlm/Lean-Github huggingface dataset:
Theorem: isConnected_compl_multibrot
Proof state before:
case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
w : 𝕊
m : w ∈ multibrotExt d
wi : w ∉ {∞}
wz : w.toComplex = z
⊢ z ∉ multibrot d
Tactic:
induction w using OnePoint.rec
Proof state after:
case h.mpr.h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
m : ∞ ∈ multibrotExt d
wi : ∞ ∉ {∞}
wz : ∞.toComplex = z
⊢ z ∉ multibrot d

case h.mpr.h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
wi : ↑x✝ ∉ {∞}
wz : (↑x✝).toComplex = z
⊢ z ∉ multibrot d
Theorem: isConnected_compl_multibrot
Proof state before:
case h.mpr.h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
m : ∞ ∈ multibrotExt d
wi : ∞ ∉ {∞}
wz : ∞.toComplex = z
⊢ z ∉ multibrot d
Tactic:
contrapose wi
Proof state after:
case h.mpr.h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
m : ∞ ∈ multibrotExt d
wz : ∞.toComplex = z
wi : ¬z ∉ multibrot d
⊢ ¬∞ ∉ {∞}
Theorem: isConnected_compl_multibrot
Proof state before:
case h.mpr.h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
m : ∞ ∈ multibrotExt d
wz : ∞.toComplex = z
wi : ¬z ∉ multibrot d
⊢ ¬∞ ∉ {∞}
Tactic:
clear wi
Proof state after:
case h.mpr.h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
m : ∞ ∈ multibrotExt d
wz : ∞.toComplex = z
⊢ ¬∞ ∉ {∞}
Theorem: isConnected_compl_multibrot
Proof state before:
case h.mpr.h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z : ℂ
m : ∞ ∈ multibrotExt d
wz : ∞.toComplex = z
⊢ ¬∞ ∉ {∞}
Tactic:
simp only [mem_singleton_iff, not_not]
Proof state after:
no goals
Theorem: isConnected_compl_multibrot
Proof state before:
case h.mpr.h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
wi : ↑x✝ ∉ {∞}
wz : (↑x✝).toComplex = z
⊢ z ∉ multibrot d
Tactic:
simp only [multibrotExt_coe, toComplex_coe, mem_diff] at m wz
Proof state after:
case h.mpr.h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z x✝ : ℂ
wi : ↑x✝ ∉ {∞}
wz : x✝ = z
m : x✝ ∉ multibrot d
⊢ z ∉ multibrot d
Theorem: isConnected_compl_multibrot
Proof state before:
case h.mpr.h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
dc : IsConnected (multibrotExt d \ {∞})
z x✝ : ℂ
wi : ↑x✝ ∉ {∞}
wz : x✝ = z
m : x✝ ∉ multibrot d
⊢ z ∉ multibrot d
Tactic:
rwa [← wz]
Proof state after:
no goals
Theorem: late_iff_disjoint_range
Proof state before:
m : ℕ
A : Finset ℕ
⊢ Late A m ↔ Disjoint A (Finset.range m)
Tactic:
simp only [Late, ge_iff_le, Finset.disjoint_iff_ne, Finset.mem_range, ne_eq]
Proof state after:
m : ℕ
A : Finset ℕ
⊢ (∀ n ∈ A, m ≤ n) ↔ ∀ a ∈ A, ∀ b < m, ¬a = b
Theorem: late_iff_disjoint_range
Proof state before:
m : ℕ
A : Finset ℕ
⊢ (∀ n ∈ A, m ≤ n) ↔ ∀ a ∈ A, ∀ b < m, ¬a = b
Tactic:
constructor
Proof state after:
case mp
m : ℕ
A : Finset ℕ
⊢ (∀ n ∈ A, m ≤ n) → ∀ a ∈ A, ∀ b < m, ¬a = b

case mpr
m : ℕ
A : Finset ℕ
⊢ (∀ a ∈ A, ∀ b < m, ¬a = b) → ∀ n ∈ A, m ≤ n
Theorem: late_iff_disjoint_range
Proof state before:
case mp
m : ℕ
A : Finset ℕ
⊢ (∀ n ∈ A, m ≤ n) → ∀ a ∈ A, ∀ b < m, ¬a = b
Tactic:
intro h n na b bm
Proof state after:
case mp
m : ℕ
A : Finset ℕ
h : ∀ n ∈ A, m ≤ n
n : ℕ
na : n ∈ A
b : ℕ
bm : b < m
⊢ ¬n = b
Theorem: late_iff_disjoint_range
Proof state before:
case mp
m : ℕ
A : Finset ℕ
h : ∀ n ∈ A, m ≤ n
n : ℕ
na : n ∈ A
b : ℕ
bm : b < m
⊢ ¬n = b
Tactic:
linarith [h _ na]
Proof state after:
no goals
Theorem: late_iff_disjoint_range
Proof state before:
case mpr
m : ℕ
A : Finset ℕ
⊢ (∀ a ∈ A, ∀ b < m, ¬a = b) → ∀ n ∈ A, m ≤ n
Tactic:
intro h n na
Proof state after:
case mpr
m : ℕ
A : Finset ℕ
h : ∀ a ∈ A, ∀ b < m, ¬a = b
n : ℕ
na : n ∈ A
⊢ m ≤ n
Theorem: late_iff_disjoint_range
Proof state before:
case mpr
m : ℕ
A : Finset ℕ
h : ∀ a ∈ A, ∀ b < m, ¬a = b
n : ℕ
na : n ∈ A
⊢ m ≤ n
Tactic:
specialize h n na n
Proof state after:
case mpr
m : ℕ
A : Finset ℕ
n : ℕ
na : n ∈ A
h : n < m → ¬n = n
⊢ m ≤ n
Theorem: late_iff_disjoint_range
Proof state before:
case mpr
m : ℕ
A : Finset ℕ
n : ℕ
na : n ∈ A
h : n < m → ¬n = n
⊢ m ≤ n
Tactic:
simpa [not_true, imp_false, not_lt] using h
Proof state after:
no goals
Theorem: sdiff_late
Proof state before:
m : ℕ
B A : Finset ℕ
⊢ B ≥ Finset.range m → Late (A \ B) m
Tactic:
intro Bm n nAB
Proof state after:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A \ B
⊢ n ≥ m
Theorem: sdiff_late
Proof state before:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A \ B
⊢ n ≥ m
Tactic:
rw [Finset.mem_sdiff] at nAB
Proof state after:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
⊢ n ≥ m
Theorem: sdiff_late
Proof state before:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
⊢ n ≥ m
Tactic:
by_contra h
Proof state after:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
h : ¬n ≥ m
⊢ False
Theorem: sdiff_late
Proof state before:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
h : ¬n ≥ m
⊢ False
Tactic:
simp only [not_le] at h
Proof state after:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
h : n < m
⊢ False
Theorem: sdiff_late
Proof state before:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
h : n < m
⊢ False
Tactic:
have nr := Finset.mem_range.mpr h
Proof state after:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
h : n < m
nr : n ∈ Finset.range m
⊢ False
Theorem: sdiff_late
Proof state before:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
h : n < m
nr : n ∈ Finset.range m
⊢ False
Tactic:
have nB := Finset.mem_of_subset Bm nr
Proof state after:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
h : n < m
nr : n ∈ Finset.range m
nB : n ∈ B
⊢ False
Theorem: sdiff_late
Proof state before:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
h : n < m
nr : n ∈ Finset.range m
nB : n ∈ B
⊢ False
Tactic:
exact nAB.2 nB
Proof state after:
no goals
Theorem: partial_geometric_bound
Proof state before:
a : ℝ
N : Finset ℕ
a0 : 0 ≤ a
a1 : a < 1
⊢ ∀ n ∉ N, 0 ≤ a ^ n
Tactic:
intro n _
Proof state after:
a : ℝ
N : Finset ℕ
a0 : 0 ≤ a
a1 : a < 1
n : ℕ
a✝ : n ∉ N
⊢ 0 ≤ a ^ n
Theorem: partial_geometric_bound
Proof state before:
a : ℝ
N : Finset ℕ
a0 : 0 ≤ a
a1 : a < 1
n : ℕ
a✝ : n ∉ N
⊢ 0 ≤ a ^ n
Tactic:
bound
Proof state after:
no goals
Theorem: partial_scaled_geometric_bound
Proof state before:
a : ℝ
c : ℝ≥0
N : Finset ℕ
a0 : 0 ≤ a
a1 : a < 1
⊢ (N.sum fun n => ↑c * a ^ n) ≤ ↑c * (1 - a)⁻¹
Tactic:
rw [←Finset.mul_sum]
Proof state after:
a : ℝ
c : ℝ≥0
N : Finset ℕ
a0 : 0 ≤ a
a1 : a < 1
⊢ (↑c * N.sum fun i => a ^ i) ≤ ↑c * (1 - a)⁻¹
Theorem: partial_scaled_geometric_bound
Proof state before:
a : ℝ
c : ℝ≥0
N : Finset ℕ
a0 : 0 ≤ a
a1 : a < 1
⊢ (↑c * N.sum fun i => a ^ i) ≤ ↑c * (1 - a)⁻¹
Tactic:
bound [partial_geometric_bound N a0 a1]
Proof state after:
no goals
Theorem: late_series_sum
Proof state before:
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
⊢ N.sum f = (Finset.image (fun n => n - m) N).sum fun n => f (n + m)
Tactic:
set Ns := Finset.image (fun n ↦ n - m) N
Proof state after:
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
⊢ N.sum f = Ns.sum fun n => f (n + m)
Theorem: late_series_sum
Proof state before:
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
NNs : N = Finset.image (fun n => n + m) Ns
⊢ N.sum f = Ns.sum fun n => f (n + m)
Tactic:
rw [NNs]
Proof state after:
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
NNs : N = Finset.image (fun n => n + m) Ns
⊢ (Finset.image (fun n => n + m) Ns).sum f = Ns.sum fun n => f (n + m)
Theorem: late_series_sum
Proof state before:
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
NNs : N = Finset.image (fun n => n + m) Ns
⊢ (Finset.image (fun n => n + m) Ns).sum f = Ns.sum fun n => f (n + m)
Tactic:
apply Finset.sum_image
Proof state after:
case a
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
NNs : N = Finset.image (fun n => n + m) Ns
⊢ ∀ x ∈ Ns, ∀ y ∈ Ns, x + m = y + m → x = y
Theorem: late_series_sum
Proof state before:
case a
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
NNs : N = Finset.image (fun n => n + m) Ns
⊢ ∀ x ∈ Ns, ∀ y ∈ Ns, x + m = y + m → x = y
Tactic:
intro a _ b _
Proof state after:
case a
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
NNs : N = Finset.image (fun n => n + m) Ns
a : ℕ
a✝¹ : a ∈ Ns
b : ℕ
a✝ : b ∈ Ns
⊢ a + m = b + m → a = b
Theorem: late_series_sum
Proof state before:
case a
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
NNs : N = Finset.image (fun n => n + m) Ns
a : ℕ
a✝¹ : a ∈ Ns
b : ℕ
a✝ : b ∈ Ns
⊢ a + m = b + m → a = b
Tactic:
exact Nat.add_right_cancel
Proof state after:
no goals
Theorem: late_series_sum
Proof state before:
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
⊢ N = Finset.image (fun n => n + m) Ns
Tactic:
apply Finset.ext
Proof state after:
case a
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
⊢ ∀ (a : ℕ), a ∈ N ↔ a ∈ Finset.image (fun n => n + m) Ns
Theorem: late_series_sum
Proof state before:
case a
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
⊢ ∀ (a : ℕ), a ∈ N ↔ a ∈ Finset.image (fun n => n + m) Ns
Tactic:
intro k
Proof state after:
case a
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
⊢ k ∈ N ↔ k ∈ Finset.image (fun n => n + m) Ns
Theorem: late_series_sum
Proof state before:
case a
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
⊢ k ∈ N ↔ k ∈ Finset.image (fun n => n + m) Ns
Tactic:
rw [Finset.image_image, Finset.mem_image]
Proof state after:
case a
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
⊢ k ∈ N ↔ ∃ a ∈ N, ((fun n => n + m) ∘ fun n => n - m) a = k
Theorem: late_series_sum
Proof state before:
case a
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
⊢ k ∈ N ↔ ∃ a ∈ N, ((fun n => n + m) ∘ fun n => n - m) a = k
Tactic:
simp
Proof state after:
case a
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
⊢ k ∈ N ↔ ∃ a ∈ N, a - m + m = k
Theorem: late_series_sum
Proof state before:
case a
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
⊢ k ∈ N ↔ ∃ a ∈ N, a - m + m = k
Tactic:
apply Iff.intro
Proof state after:
case a.mp
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
⊢ k ∈ N → ∃ a ∈ N, a - m + m = k

case a.mpr
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
⊢ (∃ a ∈ N, a - m + m = k) → k ∈ N
Theorem: late_series_sum
Proof state before:
case a.mp
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
⊢ k ∈ N → ∃ a ∈ N, a - m + m = k
Tactic:
intro kN
Proof state after:
case a.mp
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
kN : k ∈ N
⊢ ∃ a ∈ N, a - m + m = k
Theorem: late_series_sum
Proof state before:
case a.mp
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
kN : k ∈ N
⊢ ∃ a ∈ N, a - m + m = k
Tactic:
exists k
Proof state after:
case a.mp
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
kN : k ∈ N
⊢ k ∈ N ∧ k - m + m = k
Theorem: late_series_sum
Proof state before:
case a.mp
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
kN : k ∈ N
⊢ k ∈ N ∧ k - m + m = k
Tactic:
apply And.intro
Proof state after:
case a.mp.left
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
kN : k ∈ N
⊢ k ∈ N

case a.mp.right
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
kN : k ∈ N
⊢ k - m + m = k
Theorem: late_series_sum
Proof state before:
case a.mp.left
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
kN : k ∈ N
⊢ k ∈ N

case a.mp.right
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
kN : k ∈ N
⊢ k - m + m = k
Tactic:
assumption
Proof state after:
case a.mp.right
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
kN : k ∈ N
⊢ k - m + m = k
Theorem: late_series_sum
Proof state before:
case a.mp.right
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
kN : k ∈ N
⊢ k - m + m = k
Tactic:
exact Nat.sub_add_cancel (h k kN)
Proof state after:
no goals
Theorem: late_series_sum
Proof state before:
case a.mpr
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
⊢ (∃ a ∈ N, a - m + m = k) → k ∈ N
Tactic:
intro ha
Proof state after:
case a.mpr
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
ha : ∃ a ∈ N, a - m + m = k
⊢ k ∈ N
Theorem: late_series_sum
Proof state before:
case a.mpr
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k : ℕ
ha : ∃ a ∈ N, a - m + m = k
⊢ k ∈ N
Tactic:
rcases ha with ⟨a, aN, ak⟩
Proof state after:
case a.mpr.intro.intro
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k a : ℕ
aN : a ∈ N
ak : a - m + m = k
⊢ k ∈ N
Theorem: late_series_sum
Proof state before:
case a.mpr.intro.intro
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k a : ℕ
aN : a ∈ N
ak : a - m + m = k
⊢ k ∈ N
Tactic:
rw [Nat.sub_add_cancel (h a aN)] at ak
Proof state after:
case a.mpr.intro.intro
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k a : ℕ
aN : a ∈ N
ak : a = k
⊢ k ∈ N
Theorem: late_series_sum
Proof state before:
case a.mpr.intro.intro
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k a : ℕ
aN : a ∈ N
ak : a = k
⊢ k ∈ N
Tactic:
rw [← ak]
Proof state after:
case a.mpr.intro.intro
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k a : ℕ
aN : a ∈ N
ak : a = k
⊢ a ∈ N
Theorem: late_series_sum
Proof state before:
case a.mpr.intro.intro
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
Ns : Finset ℕ := Finset.image (fun n => n - m) N
k a : ℕ
aN : a ∈ N
ak : a = k
⊢ a ∈ N
Tactic:
assumption
Proof state after:
no goals
Theorem: late_series_sum'
Proof state before:
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
⊢ ∃ M, N.sum f = M.sum fun n => f (n + m)
Tactic:
exists Finset.image (fun n ↦ n - m) N
Proof state after:
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
⊢ N.sum f = (Finset.image (fun n => n - m) N).sum fun n => f (n + m)
Theorem: late_series_sum'
Proof state before:
m : ℕ
N : Finset ℕ
h : Late N m
f : ℕ → ℝ
⊢ N.sum f = (Finset.image (fun n => n - m) N).sum fun n => f (n + m)
Tactic:
exact late_series_sum h f
Proof state after:
no goals
Theorem: late_geometric_bound
Proof state before:
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
⊢ (N.sum fun n => a ^ n) ≤ a ^ m * (1 - a)⁻¹
Tactic:
rcases late_series_sum' h (fun n ↦ a^n) with ⟨M,L⟩
Proof state after:
case intro
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
L : (N.sum fun n => a ^ n) = M.sum fun n => a ^ (n + m)
⊢ (N.sum fun n => a ^ n) ≤ a ^ m * (1 - a)⁻¹
Theorem: late_geometric_bound
Proof state before:
case intro
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
L : (N.sum fun n => a ^ n) = M.sum fun n => a ^ (n + m)
⊢ (N.sum fun n => a ^ n) ≤ a ^ m * (1 - a)⁻¹
Tactic:
rw [L]
Proof state after:
case intro
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
L : (N.sum fun n => a ^ n) = M.sum fun n => a ^ (n + m)
⊢ (M.sum fun n => a ^ (n + m)) ≤ a ^ m * (1 - a)⁻¹
Theorem: late_geometric_bound
Proof state before:
case intro
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
L : (N.sum fun n => a ^ n) = M.sum fun n => a ^ (n + m)
⊢ (M.sum fun n => a ^ (n + m)) ≤ a ^ m * (1 - a)⁻¹
Tactic:
clear L
Proof state after:
case intro
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
⊢ (M.sum fun n => a ^ (n + m)) ≤ a ^ m * (1 - a)⁻¹
Theorem: late_geometric_bound
Proof state before:
case intro
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
⊢ (M.sum fun n => a ^ (n + m)) ≤ a ^ m * (1 - a)⁻¹
Tactic:
have pa : (fun n ↦ a^(n + m)) = (fun n ↦ a^n * a^m) := by apply funext; intro n; rw [pow_add]
Proof state after:
case intro
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
pa : (fun n => a ^ (n + m)) = fun n => a ^ n * a ^ m
⊢ (M.sum fun n => a ^ (n + m)) ≤ a ^ m * (1 - a)⁻¹
Theorem: late_geometric_bound
Proof state before:
case intro
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
pa : (fun n => a ^ (n + m)) = fun n => a ^ n * a ^ m
⊢ (M.sum fun n => a ^ (n + m)) ≤ a ^ m * (1 - a)⁻¹
Tactic:
calc
  M.sum (fun n ↦ a^(n + m)) = M.sum (fun n ↦ a^n * a^m) := by rw [ pa ]
  _ = M.sum (fun n ↦ a^n) * a^m := (Finset.sum_mul _ _ _).symm
  _ ≤ (1 - a)⁻¹ * a^m := by bound [partial_geometric_bound M a0 a1]
  _ = a^m * (1 - a)⁻¹ := by ring
Proof state after:
no goals
Theorem: late_geometric_bound
Proof state before:
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
⊢ (fun n => a ^ (n + m)) = fun n => a ^ n * a ^ m
Tactic:
apply funext
Proof state after:
case h
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
⊢ ∀ (x : ℕ), a ^ (x + m) = a ^ x * a ^ m
Theorem: late_geometric_bound
Proof state before:
case h
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
⊢ ∀ (x : ℕ), a ^ (x + m) = a ^ x * a ^ m
Tactic:
intro n
Proof state after:
case h
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
n : ℕ
⊢ a ^ (n + m) = a ^ n * a ^ m
Theorem: late_geometric_bound
Proof state before:
case h
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
n : ℕ
⊢ a ^ (n + m) = a ^ n * a ^ m
Tactic:
rw [pow_add]
Proof state after:
no goals
Theorem: late_geometric_bound
Proof state before:
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
pa : (fun n => a ^ (n + m)) = fun n => a ^ n * a ^ m
⊢ (M.sum fun n => a ^ (n + m)) = M.sum fun n => a ^ n * a ^ m
Tactic:
rw [ pa ]
Proof state after:
no goals
Theorem: late_geometric_bound
Proof state before:
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
pa : (fun n => a ^ (n + m)) = fun n => a ^ n * a ^ m
⊢ (M.sum fun n => a ^ n) * a ^ m ≤ (1 - a)⁻¹ * a ^ m
Tactic:
bound [partial_geometric_bound M a0 a1]
Proof state after:
no goals
Theorem: late_geometric_bound
Proof state before:
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
pa : (fun n => a ^ (n + m)) = fun n => a ^ n * a ^ m
⊢ (1 - a)⁻¹ * a ^ m = a ^ m * (1 - a)⁻¹
Tactic:
ring
Proof state after:
no goals
Theorem: finset_partition
Proof state before:
A B : Finset ℕ
⊢ A = A \ B ∪ A ∩ B
Tactic:
apply Finset.ext
Proof state after:
case a
A B : Finset ℕ
⊢ ∀ (a : ℕ), a ∈ A ↔ a ∈ A \ B ∪ A ∩ B
Theorem: finset_partition
Proof state before:
case a
A B : Finset ℕ
⊢ ∀ (a : ℕ), a ∈ A ↔ a ∈ A \ B ∪ A ∩ B
Tactic:
simp only [Finset.mem_union, Finset.mem_sdiff, Finset.mem_inter]
Proof state after:
case a
A B : Finset ℕ
⊢ ∀ (a : ℕ), a ∈ A ↔ a ∈ A ∧ a ∉ B ∨ a ∈ A ∧ a ∈ B
Theorem: finset_partition
Proof state before:
case a
A B : Finset ℕ
⊢ ∀ (a : ℕ), a ∈ A ↔ a ∈ A ∧ a ∉ B ∨ a ∈ A ∧ a ∈ B
Tactic:
intro x
Proof state after:
case a
A B : Finset ℕ
x : ℕ
⊢ x ∈ A ↔ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B
Theorem: finset_partition
Proof state before:
case a
A B : Finset ℕ
x : ℕ
⊢ x ∈ A ↔ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B
Tactic:
constructor
Proof state after:
case a.mp
A B : Finset ℕ
x : ℕ
⊢ x ∈ A → x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B

case a.mpr
A B : Finset ℕ
x : ℕ
⊢ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B → x ∈ A
Theorem: finset_partition
Proof state before:
case a.mp
A B : Finset ℕ
x : ℕ
⊢ x ∈ A → x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B
Tactic:
intro a
Proof state after:
case a.mp
A B : Finset ℕ
x : ℕ
a : x ∈ A
⊢ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B
Theorem: finset_partition
Proof state before:
case a.mp
A B : Finset ℕ
x : ℕ
a : x ∈ A
⊢ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B
Tactic:
by_cases b : x ∈ B
Proof state after:
case pos
A B : Finset ℕ
x : ℕ
a : x ∈ A
b : x ∈ B
⊢ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B

case neg
A B : Finset ℕ
x : ℕ
a : x ∈ A
b : x ∉ B
⊢ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B
Theorem: finset_partition
Proof state before:
case pos
A B : Finset ℕ
x : ℕ
a : x ∈ A
b : x ∈ B
⊢ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B
Tactic:
right
Proof state after:
case pos.h
A B : Finset ℕ
x : ℕ
a : x ∈ A
b : x ∈ B
⊢ x ∈ A ∧ x ∈ B
Theorem: finset_partition
Proof state before:
case pos.h
A B : Finset ℕ
x : ℕ
a : x ∈ A
b : x ∈ B
⊢ x ∈ A ∧ x ∈ B
Tactic:
use a,b
Proof state after:
no goals
Theorem: finset_partition
Proof state before:
case neg
A B : Finset ℕ
x : ℕ
a : x ∈ A
b : x ∉ B
⊢ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B
Tactic:
left
Proof state after:
case neg.h
A B : Finset ℕ
x : ℕ
a : x ∈ A
b : x ∉ B
⊢ x ∈ A ∧ x ∉ B
Theorem: finset_partition
Proof state before:
case neg.h
A B : Finset ℕ
x : ℕ
a : x ∈ A
b : x ∉ B
⊢ x ∈ A ∧ x ∉ B
Tactic:
use a,b
Proof state after:
no goals
Theorem: finset_partition
Proof state before:
case a.mpr
A B : Finset ℕ
x : ℕ
⊢ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B → x ∈ A
Tactic:
intro h
Proof state after:
case a.mpr
A B : Finset ℕ
x : ℕ
h : x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B
⊢ x ∈ A
Theorem: finset_partition
Proof state before:
case a.mpr
A B : Finset ℕ
x : ℕ
h : x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B
⊢ x ∈ A
Tactic:
cases' h with m m
Proof state after:
case a.mpr.inl
A B : Finset ℕ
x : ℕ
m : x ∈ A ∧ x ∉ B
⊢ x ∈ A

case a.mpr.inr
A B : Finset ℕ
x : ℕ
m : x ∈ A ∧ x ∈ B
⊢ x ∈ A
Theorem: finset_partition
Proof state before:
case a.mpr.inl
A B : Finset ℕ
x : ℕ
m : x ∈ A ∧ x ∉ B
⊢ x ∈ A

case a.mpr.inr
A B : Finset ℕ
x : ℕ
m : x ∈ A ∧ x ∈ B
⊢ x ∈ A
Tactic:
repeat exact m.1
Proof state after:
no goals
Theorem: finset_partition
Proof state before:
case a.mpr.inr
A B : Finset ℕ
x : ℕ
m : x ∈ A ∧ x ∈ B
⊢ x ∈ A
Tactic:
exact m.1
Proof state after:
no goals
Theorem: finset_sum_partition
Proof state before:
A B : Finset ℕ
f : ℕ → ℂ
⊢ A.sum f = (A \ B).sum f + (A ∩ B).sum f
Tactic:
have ha : A = A \ B ∪ A ∩ B := finset_partition A B
Proof state after:
A B : Finset ℕ
f : ℕ → ℂ
ha : A = A \ B ∪ A ∩ B
⊢ A.sum f = (A \ B).sum f + (A ∩ B).sum f
Theorem: finset_sum_partition
Proof state before:
A B : Finset ℕ
f : ℕ → ℂ
ha : A = A \ B ∪ A ∩ B
⊢ A.sum f = (A \ B).sum f + (A ∩ B).sum f
Tactic:
nth_rw 1 [ha]
Proof state after:
A B : Finset ℕ
f : ℕ → ℂ
ha : A = A \ B ∪ A ∩ B
⊢ (A \ B ∪ A ∩ B).sum f = (A \ B).sum f + (A ∩ B).sum f
Theorem: finset_sum_partition
Proof state before:
A B : Finset ℕ
f : ℕ → ℂ
ha : A = A \ B ∪ A ∩ B
⊢ (A \ B ∪ A ∩ B).sum f = (A \ B).sum f + (A ∩ B).sum f
Tactic:
exact Finset.sum_union (Finset.disjoint_sdiff_inter A B)
Proof state after:
no goals
Theorem: symmDiff_union
Proof state before:
A B : Finset ℕ
⊢ A ∆ B = A \ B ∪ B \ A
Tactic:
rw [symmDiff_def, Finset.sup_eq_union]
Proof state after:
no goals
Theorem: symmDiff_bound
Proof state before:
A B : Finset ℕ
f : ℕ → ℂ
⊢ dist (A.sum f) (B.sum f) ≤ (A ∆ B).sum fun n => Complex.abs (f n)
Tactic:
rw [finset_sum_partition A B f, finset_sum_partition B A f, Finset.inter_comm B A]
Proof state after:
A B : Finset ℕ
f : ℕ → ℂ
⊢ dist ((A \ B).sum f + (A ∩ B).sum f) ((B \ A).sum f + (A ∩ B).sum f) ≤ (A ∆ B).sum fun n => Complex.abs (f n)