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

State before:
⊢ CompletelyMultiplicative ↑ζ
Tactic:
unfold CompletelyMultiplicative
State after:
⊢ ↑ζ 1 = 1 ∧ ∀ (a b : ℕ), ↑ζ (a * b) = ↑ζ a * ↑ζ b

State before:
⊢ ↑ζ 1 = 1 ∧ ∀ (a b : ℕ), ↑ζ (a * b) = ↑ζ a * ↑ζ b
Tactic:
simp_rw [ArithmeticFunction.natCoe_apply, ArithmeticFunction.zeta_apply, ite_false, Nat.cast_one,
  mul_eq_zero, Nat.cast_ite, CharP.cast_eq_zero, mul_ite, mul_zero, true_and]
State after:
⊢ ∀ (a b : ℕ), (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1

State before:
⊢ ∀ (a b : ℕ), (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1
Tactic:
intro a b
State after:
a b : ℕ
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1

State before:
a b : ℕ
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1
Tactic:
by_cases ha : a = 0
State after:
case pos
a b : ℕ
ha : a = 0
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1

case neg
a b : ℕ
ha : ¬a = 0
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1

State before:
case neg
a b : ℕ
ha : ¬a = 0
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1
Tactic:
by_cases hb : b = 0
State after:
case pos
a b : ℕ
ha : ¬a = 0
hb : b = 0
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1

case neg
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1

State before:
case neg
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1
Tactic:
rw [if_neg, if_neg hb, if_neg ha]
State after:
case neg
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ ↑1 = ↑1 * ↑1

case neg.hnc
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ ¬(a = 0 ∨ b = 0)

State before:
case neg
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ ↑1 = ↑1 * ↑1

case neg.hnc
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ ¬(a = 0 ∨ b = 0)
Tactic:
ring
State after:
case neg.hnc
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ ¬(a = 0 ∨ b = 0)

State before:
case neg.hnc
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ ¬(a = 0 ∨ b = 0)
Tactic:
push_neg
State after:
case neg.hnc
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ a ≠ 0 ∧ b ≠ 0

State before:
case neg.hnc
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ a ≠ 0 ∧ b ≠ 0
Tactic:
exact ⟨ha, hb⟩
State after:
no goals

State before:
case pos
a b : ℕ
ha : a = 0
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1
Tactic:
simp [ha]
State after:
no goals

State before:
case pos
a b : ℕ
ha : ¬a = 0
hb : b = 0
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1
Tactic:
simp [hb]
State after:
no goals