Theorem: riemannZeta0_zero_aux (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
N : ℕ
Npos : 0 < N
⊢ ∑ x ∈ Finset.Ico 0 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹
Tactic:
have : Finset.Ico 1 N ⊆ Finset.Ico 0 N := by
  intro x hx
  simp only [Finset.mem_Ico, Nat.Ico_zero_eq_range, Finset.mem_range] at hx ⊢
  exact hx.2
State after:
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
⊢ ∑ x ∈ Finset.Ico 0 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹

State before:
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
⊢ ∑ x ∈ Finset.Ico 0 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹
Tactic:
rw [← Finset.sum_sdiff (s₁ := Finset.Ico 1 N) (s₂ := Finset.Ico 0 N) this]
State after:
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
⊢ ∑ x ∈ Finset.Ico 0 N \ Finset.Ico 1 N, (↑x)⁻¹ + ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹

State before:
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
⊢ ∑ x ∈ Finset.Ico 0 N \ Finset.Ico 1 N, (↑x)⁻¹ + ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹
Tactic:
have : Finset.Ico 0 N \ Finset.Ico 1 N = Finset.range 1 := by
  ext a
  simp only [Nat.Ico_zero_eq_range, Finset.mem_sdiff, Finset.mem_range, Finset.mem_Ico, not_and,
    not_lt, Finset.range_one, Finset.mem_singleton]
  exact ⟨fun _ ↦ by omega, fun ha ↦ ⟨by simp [ha, Npos], by omega⟩⟩
State after:
N : ℕ
Npos : 0 < N
this✝ : Finset.Ico 1 N ⊆ Finset.Ico 0 N
this : Finset.Ico 0 N \ Finset.Ico 1 N = Finset.range 1
⊢ ∑ x ∈ Finset.Ico 0 N \ Finset.Ico 1 N, (↑x)⁻¹ + ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹

State before:
N : ℕ
Npos : 0 < N
this✝ : Finset.Ico 1 N ⊆ Finset.Ico 0 N
this : Finset.Ico 0 N \ Finset.Ico 1 N = Finset.range 1
⊢ ∑ x ∈ Finset.Ico 0 N \ Finset.Ico 1 N, (↑x)⁻¹ + ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹
Tactic:
rw [this]
State after:
N : ℕ
Npos : 0 < N
this✝ : Finset.Ico 1 N ⊆ Finset.Ico 0 N
this : Finset.Ico 0 N \ Finset.Ico 1 N = Finset.range 1
⊢ ∑ x ∈ Finset.range 1, (↑x)⁻¹ + ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹

State before:
N : ℕ
Npos : 0 < N
this✝ : Finset.Ico 1 N ⊆ Finset.Ico 0 N
this : Finset.Ico 0 N \ Finset.Ico 1 N = Finset.range 1
⊢ ∑ x ∈ Finset.range 1, (↑x)⁻¹ + ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹
Tactic:
simp
State after:
no goals

State before:
N : ℕ
Npos : 0 < N
⊢ Finset.Ico 1 N ⊆ Finset.Ico 0 N
Tactic:
intro x hx
State after:
N : ℕ
Npos : 0 < N
x : ℕ
hx : x ∈ Finset.Ico 1 N
⊢ x ∈ Finset.Ico 0 N

State before:
N : ℕ
Npos : 0 < N
x : ℕ
hx : x ∈ Finset.Ico 1 N
⊢ x ∈ Finset.Ico 0 N
Tactic:
simp only [Finset.mem_Ico, Nat.Ico_zero_eq_range, Finset.mem_range] at hx ⊢
State after:
N : ℕ
Npos : 0 < N
x : ℕ
hx : 1 ≤ x ∧ x < N
⊢ x < N

State before:
N : ℕ
Npos : 0 < N
x : ℕ
hx : 1 ≤ x ∧ x < N
⊢ x < N
Tactic:
exact hx.2
State after:
no goals

State before:
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
⊢ Finset.Ico 0 N \ Finset.Ico 1 N = Finset.range 1
Tactic:
ext a
State after:
case a
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
a : ℕ
⊢ a ∈ Finset.Ico 0 N \ Finset.Ico 1 N ↔ a ∈ Finset.range 1

State before:
case a
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
a : ℕ
⊢ a ∈ Finset.Ico 0 N \ Finset.Ico 1 N ↔ a ∈ Finset.range 1
Tactic:
simp only [Nat.Ico_zero_eq_range, Finset.mem_sdiff, Finset.mem_range, Finset.mem_Ico, not_and,
  not_lt, Finset.range_one, Finset.mem_singleton]
State after:
case a
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
a : ℕ
⊢ a < N ∧ (1 ≤ a → N ≤ a) ↔ a = 0

State before:
case a
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
a : ℕ
⊢ a < N ∧ (1 ≤ a → N ≤ a) ↔ a = 0
Tactic:
exact ⟨fun _ ↦ by omega, fun ha ↦ ⟨by simp [ha, Npos], by omega⟩⟩
State after:
no goals

State before:
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
a : ℕ
x✝ : a < N ∧ (1 ≤ a → N ≤ a)
⊢ a = 0
Tactic:
omega
State after:
no goals

State before:
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
a : ℕ
ha : a = 0
⊢ a < N
Tactic:
simp [ha, Npos]
State after:
no goals

State before:
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
a : ℕ
ha : a = 0
⊢ 1 ≤ a → N ≤ a
Tactic:
omega
State after:
no goals