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

State before:
⊢ CompletelyMultiplicative ↑ArithmeticFunction.id
Tactic:
constructor <;> simp
State after:
no goals