case mp
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
⊢ f = g → ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)

case mpr
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
⊢ (∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)) → f = g
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
⊢ f = g ↔ ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
constructor
case mpr
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
⊢ f = g
case mpr
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
⊢ (∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)) → f = g
intro h
case mpr.h
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
⊢ ↑f n = ↑g n
case mpr
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
⊢ f = g
ext n
case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
hn : n = 0
⊢ ↑f n = ↑g n

case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
hn : ¬n = 0
⊢ ↑f n = ↑g n
case mpr.h
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
⊢ ↑f n = ↑g n
by_cases hn : n = 0
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
hn : ¬n = 0
⊢ (Finsupp.prod (factorization n) fun p k => ↑f (p ^ k)) = Finsupp.prod (factorization n) fun p k => ↑g (p ^ k)
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
hn : ¬n = 0
⊢ ↑f n = ↑g n
rw [multiplicative_factorization f hf hn, multiplicative_factorization g hg hn]
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
hn : ¬n = 0
⊢ ∀ (x : ℕ),
    x ∈ (factorization n).support →
      (fun p k => ↑f (p ^ k)) x (↑(factorization n) x) = (fun p k => ↑g (p ^ k)) x (↑(factorization n) x)
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
hn : ¬n = 0
⊢ (Finsupp.prod (factorization n) fun p k => ↑f (p ^ k)) = Finsupp.prod (factorization n) fun p k => ↑g (p ^ k)
refine' Finset.prod_congr rfl _
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
hn : ¬n = 0
⊢ ∀ (x : ℕ), x ∈ factors n → ↑f (x ^ ↑(factorization n) x) = ↑g (x ^ ↑(factorization n) x)
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
hn : ¬n = 0
⊢ ∀ (x : ℕ),
    x ∈ (factorization n).support →
      (fun p k => ↑f (p ^ k)) x (↑(factorization n) x) = (fun p k => ↑g (p ^ k)) x (↑(factorization n) x)
simp only [support_factorization, List.mem_toFinset]
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
hn : ¬n = 0
p : ℕ
hp : p ∈ factors n
⊢ ↑f (p ^ ↑(factorization n) p) = ↑g (p ^ ↑(factorization n) p)
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
hn : ¬n = 0
⊢ ∀ (x : ℕ), x ∈ factors n → ↑f (x ^ ↑(factorization n) x) = ↑g (x ^ ↑(factorization n) x)
intro p hp
no goals
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
hn : ¬n = 0
p : ℕ
hp : p ∈ factors n
⊢ ↑f (p ^ ↑(factorization n) p) = ↑g (p ^ ↑(factorization n) p)
exact h p _ (Nat.prime_of_mem_factors hp)
case mp
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : f = g
p i : ℕ
a✝ : Prime p
⊢ ↑f (p ^ i) = ↑g (p ^ i)
case mp
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
⊢ f = g → ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
intro h p i _
no goals
case mp
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : f = g
p i : ℕ
a✝ : Prime p
⊢ ↑f (p ^ i) = ↑g (p ^ i)
rw [h]
no goals
case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
hn : n = 0
⊢ ↑f n = ↑g n
rw [hn, ArithmeticFunction.map_zero, ArithmeticFunction.map_zero]