Theorem: late_series_sum (Ray/Misc/Bounds.lean)

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
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)

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]
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)

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
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

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 _
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

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
State after:
no goals

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
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

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
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

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]
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

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
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

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
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

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
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

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
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

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
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

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
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

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)
State after:
no goals

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
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

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⟩
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

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
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

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]
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

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
State after:
no goals