Theorem: UpperBnd_aux5 (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
σ t : ℝ
t_ge : 3 < |t|
σ_le : σ ≤ 2
⊢ (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
Tactic:
obtain ⟨h₁, h₂⟩ := Nat.self_div_floor_bound (by linarith)
State after:
case intro
σ t : ℝ
t_ge : 3 < |t|
σ_le : σ ≤ 2
h₁ : 1 ≤ |t| / ↑⌊|t|⌋₊
h₂ : |t| / ↑⌊|t|⌋₊ ≤ 2
⊢ (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4

State before:
case intro
σ t : ℝ
t_ge : 3 < |t|
σ_le : σ ≤ 2
h₁ : 1 ≤ |t| / ↑⌊|t|⌋₊
h₂ : |t| / ↑⌊|t|⌋₊ ≤ 2
⊢ (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
Tactic:
calc _ ≤ ((|t| / ↑⌊|t|⌋₊) ^ (2 : ℝ)) := by gcongr; exact h₁
     _ ≤ (2 : ℝ) ^ (2 : ℝ) := by gcongr
     _ = 4 := by norm_num
State after:
no goals

State before:
σ t : ℝ
t_ge : 3 < |t|
σ_le : σ ≤ 2
⊢ 1 ≤ |?m.763672|
Tactic:
linarith
State after:
no goals

State before:
σ t : ℝ
t_ge : 3 < |t|
σ_le : σ ≤ 2
h₁ : 1 ≤ |t| / ↑⌊|t|⌋₊
h₂ : |t| / ↑⌊|t|⌋₊ ≤ 2
⊢ (|t| / ↑⌊|t|⌋₊) ^ σ ≤ (|t| / ↑⌊|t|⌋₊) ^ 2
Tactic:
gcongr
State after:
case hx
σ t : ℝ
t_ge : 3 < |t|
σ_le : σ ≤ 2
h₁ : 1 ≤ |t| / ↑⌊|t|⌋₊
h₂ : |t| / ↑⌊|t|⌋₊ ≤ 2
⊢ 1 ≤ |t| / ↑⌊|t|⌋₊

State before:
case hx
σ t : ℝ
t_ge : 3 < |t|
σ_le : σ ≤ 2
h₁ : 1 ≤ |t| / ↑⌊|t|⌋₊
h₂ : |t| / ↑⌊|t|⌋₊ ≤ 2
⊢ 1 ≤ |t| / ↑⌊|t|⌋₊
Tactic:
exact h₁
State after:
no goals

State before:
σ t : ℝ
t_ge : 3 < |t|
σ_le : σ ≤ 2
h₁ : 1 ≤ |t| / ↑⌊|t|⌋₊
h₂ : |t| / ↑⌊|t|⌋₊ ≤ 2
⊢ (|t| / ↑⌊|t|⌋₊) ^ 2 ≤ 2 ^ 2
Tactic:
gcongr
State after:
no goals

State before:
σ t : ℝ
t_ge : 3 < |t|
σ_le : σ ≤ 2
h₁ : 1 ≤ |t| / ↑⌊|t|⌋₊
h₂ : |t| / ↑⌊|t|⌋₊ ≤ 2
⊢ 2 ^ 2 = 4
Tactic:
norm_num
State after:
no goals