Theorem: Sieve.zeta_pos_of_prime (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean)

State before:
⊢ ∀ (p : ℕ), p.Prime → 0 < ↑ζ p
Tactic:
intro p hp
State after:
p : ℕ
hp : p.Prime
⊢ 0 < ↑ζ p

State before:
p : ℕ
hp : p.Prime
⊢ 0 < ↑ζ p
Tactic:
rw [ArithmeticFunction.natCoe_apply, ArithmeticFunction.zeta_apply, if_neg (Nat.Prime.ne_zero hp)]
State after:
p : ℕ
hp : p.Prime
⊢ 0 < ↑1

State before:
p : ℕ
hp : p.Prime
⊢ 0 < ↑1
Tactic:
norm_num
State after:
no goals