Theorem: UpperBnd_aux3 (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
⊢ let N := ⌊|t|⌋₊;
  ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log
Tactic:
intro N
State after:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log

State before:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log
Tactic:
obtain ⟨Npos, N_le_t, _, _, σPos, _⟩ := UpperBnd_aux hA t_gt σ_ge
State after:
case intro.intro.intro.intro.intro
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log

State before:
case intro.intro.intro.intro.intro
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log
Tactic:
have logt_gt := logt_gt_one t_gt
State after:
case intro.intro.intro.intro.intro
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log

State before:
case intro.intro.intro.intro.intro
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log
Tactic:
have (n : ℕ) (hn : n ∈ Finset.range (N + 1)) := ZetaBnd_aux2 (n := n) hA.1 σPos ?_ σ_ge
State after:
case intro.intro.intro.intro.intro.refine_2
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ∀ n ∈ Finset.range (N + 1), ‖↑n ^ (-(↑σ + ↑t * I))‖ ≤ (↑n)⁻¹ * A.exp
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log

case intro.intro.intro.intro.intro.refine_1
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
n : ℕ
hn : n ∈ Finset.range (N + 1)
⊢ ↑n ≤ |t|

State before:
case intro.intro.intro.intro.intro.refine_2
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ∀ n ∈ Finset.range (N + 1), ‖↑n ^ (-(↑σ + ↑t * I))‖ ≤ (↑n)⁻¹ * A.exp
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log
Tactic:
replace := norm_sum_le_of_le (Finset.range (N + 1)) this
State after:
case intro.intro.intro.intro.intro.refine_2
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ ∑ b ∈ Finset.range (N + 1), (↑b)⁻¹ * A.exp
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log

State before:
case intro.intro.intro.intro.intro.refine_2
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ ∑ b ∈ Finset.range (N + 1), (↑b)⁻¹ * A.exp
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log
Tactic:
rw [← Finset.sum_mul, mul_comm _ (Real.exp A)] at this
State after:
case intro.intro.intro.intro.intro.refine_2
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log

State before:
case intro.intro.intro.intro.intro.refine_2
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log
Tactic:
rw [mul_assoc]
State after:
case intro.intro.intro.intro.intro.refine_2
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * (C * |t|.log)

State before:
case intro.intro.intro.intro.intro.refine_2
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * (C * |t|.log)
Tactic:
apply le_trans this <| (mul_le_mul_left A.exp_pos).mpr ?_
State after:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
⊢ ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹ ≤ C * |t|.log

State before:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this✝ : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹ ≤ C * |t|.log
Tactic:
refine le_trans ?_ this
State after:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this✝ : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹ ≤ 1 + (↑N).log

State before:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this✝ : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹ ≤ 1 + (↑N).log
Tactic:
convert harmonic_eq_sum_Icc ▸ harmonic_le_one_add_log N
State after:
case h.e'_3
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this✝ : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹ = ↑(∑ i ∈ Finset.Icc 1 N, (↑i)⁻¹)

State before:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
⊢ 1 + (↑N).log ≤ C * |t|.log
Tactic:
by_cases hN : N = 1
State after:
case pos
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : N = 1
⊢ 1 + (↑N).log ≤ C * |t|.log

case neg
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : ¬N = 1
⊢ 1 + (↑N).log ≤ C * |t|.log

State before:
case pos
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : N = 1
⊢ 1 + (↑N).log ≤ C * |t|.log
Tactic:
simp only [hN, Nat.cast_one, Real.log_one, add_zero]
State after:
case pos
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : N = 1
⊢ 1 ≤ C * |t|.log

State before:
case pos
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : N = 1
⊢ 1 ≤ C * |t|.log
Tactic:
have : 2 * 1 ≤ C * Real.log |t| := mul_le_mul hC logt_gt.le (by linarith) (by linarith)
State after:
case pos
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this✝ : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : N = 1
this : 2 * 1 ≤ C * |t|.log
⊢ 1 ≤ C * |t|.log

State before:
case pos
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this✝ : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : N = 1
this : 2 * 1 ≤ C * |t|.log
⊢ 1 ≤ C * |t|.log
Tactic:
linarith
State after:
no goals

State before:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : N = 1
⊢ 0 ≤ 1
Tactic:
linarith
State after:
no goals

State before:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : N = 1
⊢ 0 ≤ C
Tactic:
linarith
State after:
no goals

State before:
case neg
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : ¬N = 1
⊢ 1 + (↑N).log ≤ C * |t|.log
Tactic:
rw [(by ring : C * Real.log |t| = Real.log |t| + (C - 1) * Real.log |t|),
  ← one_mul <| Real.log (N: ℝ)]
State after:
case neg
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : ¬N = 1
⊢ 1 + 1 * (↑N).log ≤ |t|.log + (C - 1) * |t|.log

State before:
case neg
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : ¬N = 1
⊢ 1 + 1 * (↑N).log ≤ |t|.log + (C - 1) * |t|.log
Tactic:
apply add_le_add logt_gt.le
State after:
case neg
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : ¬N = 1
⊢ 1 * (↑N).log ≤ (C - 1) * |t|.log

State before:
case neg
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : ¬N = 1
⊢ 1 * (↑N).log ≤ (C - 1) * |t|.log
Tactic:
refine mul_le_mul (by linarith) ?_ (by positivity) (by linarith)
State after:
case neg
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : ¬N = 1
⊢ (↑N).log ≤ |t|.log

State before:
case neg
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : ¬N = 1
⊢ (↑N).log ≤ |t|.log
Tactic:
exact Real.log_le_log (by positivity) N_le_t
State after:
no goals

State before:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : ¬N = 1
⊢ C * |t|.log = |t|.log + (C - 1) * |t|.log
Tactic:
ring
State after:
no goals

State before:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : ¬N = 1
⊢ 1 ≤ C - 1
Tactic:
linarith
State after:
no goals

State before:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : ¬N = 1
⊢ 0 ≤ (↑N).log
Tactic:
positivity
State after:
no goals

State before:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : ¬N = 1
⊢ 0 ≤ C - 1
Tactic:
linarith
State after:
no goals

State before:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : ¬N = 1
⊢ 0 < ↑N
Tactic:
positivity
State after:
no goals

State before:
case h.e'_3
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this✝ : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹ = ↑(∑ i ∈ Finset.Icc 1 N, (↑i)⁻¹)
Tactic:
simp only [Rat.cast_sum, Rat.cast_inv, Rat.cast_natCast, Finset.range_eq_Ico]
State after:
case h.e'_3
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this✝ : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ ∑ x ∈ Finset.Ico 0 (N + 1), (↑x)⁻¹ = ∑ x ∈ Finset.Icc 1 N, (↑x)⁻¹

State before:
case h.e'_3
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this✝ : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ ∑ x ∈ Finset.Ico 0 (N + 1), (↑x)⁻¹ = ∑ x ∈ Finset.Icc 1 N, (↑x)⁻¹
Tactic:
rw [riemannZeta0_zero_aux (N + 1) (by linarith)]
State after:
case h.e'_3
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this✝ : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ ∑ x ∈ Finset.Ico 1 (N + 1), (↑x)⁻¹ = ∑ x ∈ Finset.Icc 1 N, (↑x)⁻¹

State before:
case h.e'_3
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this✝ : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ ∑ x ∈ Finset.Ico 1 (N + 1), (↑x)⁻¹ = ∑ x ∈ Finset.Icc 1 N, (↑x)⁻¹
Tactic:
congr! 1
State after:
no goals

State before:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this✝ : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ 0 < N + 1
Tactic:
linarith
State after:
no goals

State before:
case intro.intro.intro.intro.intro.refine_1
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
n : ℕ
hn : n ∈ Finset.range (N + 1)
⊢ ↑n ≤ |t|
Tactic:
simp only [Finset.mem_range] at hn
State after:
case intro.intro.intro.intro.intro.refine_1
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
n : ℕ
hn : n < N + 1
⊢ ↑n ≤ |t|

State before:
case intro.intro.intro.intro.intro.refine_1
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
n : ℕ
hn : n < N + 1
⊢ ↑n ≤ |t|
Tactic:
linarith [(by exact_mod_cast (by omega : n ≤ N) : (n : ℝ) ≤ N)]
State after:
no goals

State before:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
n : ℕ
hn : n < N + 1
⊢ ↑n ≤ ↑N
Tactic:
exact_mod_cast (by omega : n ≤ N)
State after:
no goals

State before:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
n : ℕ
hn : n < N + 1
⊢ n ≤ N
Tactic:
omega
State after:
no goals