Theorem: S_sub_S (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ S f 0 N - S f ε N = cumsum f ⌈ε * ↑N⌉₊ / ↑N
Tactic:
have r1 : Finset.range N = Finset.range ⌈ε * N⌉₊ ∪ Finset.Ico ⌈ε * N⌉₊ N := by
  rw [Finset.range_eq_Ico] ; symm ; apply Finset.Ico_union_Ico_eq_Ico (by simp)
  simp ; convert_to ε * ↑N ≤ 1 * ↑N ; ring ; gcongr
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
r1 : Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
⊢ S f 0 N - S f ε N = cumsum f ⌈ε * ↑N⌉₊ / ↑N

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
r1 : Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
⊢ S f 0 N - S f ε N = cumsum f ⌈ε * ↑N⌉₊ / ↑N
Tactic:
have r2 : Disjoint (Finset.range ⌈ε * N⌉₊) (Finset.Ico ⌈ε * N⌉₊ N) := by
  rw [Finset.range_eq_Ico] ; apply Finset.Ico_disjoint_Ico_consecutive
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
r1 : Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
r2 : Disjoint (Finset.range ⌈ε * ↑N⌉₊) (Finset.Ico ⌈ε * ↑N⌉₊ N)
⊢ S f 0 N - S f ε N = cumsum f ⌈ε * ↑N⌉₊ / ↑N

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
r1 : Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
r2 : Disjoint (Finset.range ⌈ε * ↑N⌉₊) (Finset.Ico ⌈ε * ↑N⌉₊ N)
⊢ S f 0 N - S f ε N = cumsum f ⌈ε * ↑N⌉₊ / ↑N
Tactic:
simp [S, r1, Finset.sum_union r2, cumsum, add_div, abs_div]
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
Tactic:
rw [Finset.range_eq_Ico]
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ Finset.Ico 0 N = Finset.Ico 0 ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ Finset.Ico 0 N = Finset.Ico 0 ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
Tactic:
symm
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ Finset.Ico 0 ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N = Finset.Ico 0 N

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ Finset.Ico 0 ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N = Finset.Ico 0 N
Tactic:
apply Finset.Ico_union_Ico_eq_Ico (by simp)
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ⌈ε * ↑N⌉₊ ≤ N

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ⌈ε * ↑N⌉₊ ≤ N
Tactic:
simp
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ε * ↑N ≤ ↑N

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ε * ↑N ≤ ↑N
Tactic:
convert_to ε * ↑N ≤ 1 * ↑N
State after:
case h.e'_4
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ↑N = 1 * ↑N

n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ε * ↑N ≤ 1 * ↑N

State before:
case h.e'_4
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ↑N = 1 * ↑N

n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ε * ↑N ≤ 1 * ↑N
Tactic:
ring
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ε * ↑N ≤ 1 * ↑N

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ε * ↑N ≤ 1 * ↑N
Tactic:
gcongr
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ 0 ≤ ⌈ε * ↑N⌉₊
Tactic:
simp
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
r1 : Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
⊢ Disjoint (Finset.range ⌈ε * ↑N⌉₊) (Finset.Ico ⌈ε * ↑N⌉₊ N)
Tactic:
rw [Finset.range_eq_Ico]
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
r1 : Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
⊢ Disjoint (Finset.Ico 0 ⌈ε * ↑N⌉₊) (Finset.Ico ⌈ε * ↑N⌉₊ N)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
r1 : Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
⊢ Disjoint (Finset.Ico 0 ⌈ε * ↑N⌉₊) (Finset.Ico ⌈ε * ↑N⌉₊ N)
Tactic:
apply Finset.Ico_disjoint_Ico_consecutive
State after:
no goals