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

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

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

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

State before:
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
a b : ℕ
⊢ (f.pdiv g) (a * b) = (f.pdiv g) a * (f.pdiv g) b
Tactic:
simp_rw [pdiv_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.pdiv g) 1 = 1
Tactic:
rw [pdiv_apply, hf.1, hg.1, div_one]
State after:
no goals