Theorem: ZetaSum_aux2a (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
⊢ ∃ C, ∀ (x : ℝ), |↑⌊x⌋ + 1 / 2 - x| ≤ C
Tactic:
use 1 / 2
State after:
case h

⊢ ∀ (x : ℝ), |↑⌊x⌋ + 1 / 2 - x| ≤ 1 / 2

State before:
case h

⊢ ∀ (x : ℝ), |↑⌊x⌋ + 1 / 2 - x| ≤ 1 / 2
Tactic:
exact ZetaSum_aux1_3
State after:
no goals