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

State before:
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
⊢ CompletelyMultiplicative (f.pmul g)
Tactic:
constructor
State after:
case left
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
⊢ (f.pmul g) 1 = 1

case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
⊢ ∀ (a b : ℕ), (f.pmul g) (a * b) = (f.pmul g) a * (f.pmul g) b

State before:
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
⊢ ∀ (a b : ℕ), (f.pmul g) (a * b) = (f.pmul g) a * (f.pmul g) b
Tactic:
intro a b
State after:
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
a b : ℕ
⊢ (f.pmul g) (a * b) = (f.pmul g) a * (f.pmul g) b

State before:
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
a b : ℕ
⊢ (f.pmul g) (a * b) = (f.pmul g) a * (f.pmul g) b
Tactic:
simp_rw [pmul_apply, hf.2, hg.2]
State after:
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
a b : ℕ
⊢ f a * f b * (g a * g b) = f a * g a * (f b * g b)

State before:
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
a b : ℕ
⊢ f a * f b * (g a * g b) = f a * g a * (f b * g b)
Tactic:
ring
State after:
no goals

State before:
case left
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
⊢ (f.pmul g) 1 = 1
Tactic:
rw [pmul_apply, hf.1, hg.1, mul_one]
State after:
no goals