case empty
R : Type u_2
ι : Type u_1
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : IsMultiplicative f
s : Finset ι
hs✝ : Set.Pairwise (↑s) (coprime on g)
hs : Set.Pairwise (↑∅) (coprime on g)
⊢ ↑f (∏ i in ∅, g i) = ∏ i in ∅, ↑f (g i)

case insert
R : Type u_2
ι : Type u_1
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : IsMultiplicative f
s✝ : Finset ι
hs✝ : Set.Pairwise (↑s✝) (coprime on g)
a : ι
s : Finset ι
has : ¬a ∈ s
ih : Set.Pairwise (↑s) (coprime on g) → ↑f (∏ i in s, g i) = ∏ i in s, ↑f (g i)
hs : Set.Pairwise (↑(insert a s)) (coprime on g)
⊢ ↑f (∏ i in insert a s, g i) = ∏ i in insert a s, ↑f (g i)
R : Type u_2
ι : Type u_1
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : IsMultiplicative f
s : Finset ι
hs : Set.Pairwise (↑s) (coprime on g)
⊢ ↑f (∏ i in s, g i) = ∏ i in s, ↑f (g i)
induction' s using Finset.induction_on with a s has ih hs
case insert
R : Type u_2
ι : Type u_1
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : IsMultiplicative f
s✝ : Finset ι
hs✝ : Set.Pairwise (↑s✝) (coprime on g)
a : ι
s : Finset ι
has : ¬a ∈ s
ih : Set.Pairwise (↑s) (coprime on g) → ↑f (∏ i in s, g i) = ∏ i in s, ↑f (g i)
hs : Set.Pairwise (↑s) (coprime on g) ∧ ∀ (b : ι), b ∈ ↑s → a ≠ b → (coprime on g) a b
⊢ ↑f (∏ i in insert a s, g i) = ∏ i in insert a s, ↑f (g i)
case insert
R : Type u_2
ι : Type u_1
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : IsMultiplicative f
s✝ : Finset ι
hs✝ : Set.Pairwise (↑s✝) (coprime on g)
a : ι
s : Finset ι
has : ¬a ∈ s
ih : Set.Pairwise (↑s) (coprime on g) → ↑f (∏ i in s, g i) = ∏ i in s, ↑f (g i)
hs : Set.Pairwise (↑(insert a s)) (coprime on g)
⊢ ↑f (∏ i in insert a s, g i) = ∏ i in insert a s, ↑f (g i)
rw [coe_insert, Set.pairwise_insert_of_symmetric (coprime.symmetric.comap g)] at hs
case insert
R : Type u_2
ι : Type u_1
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : IsMultiplicative f
s✝ : Finset ι
hs✝ : Set.Pairwise (↑s✝) (coprime on g)
a : ι
s : Finset ι
has : ¬a ∈ s
ih : Set.Pairwise (↑s) (coprime on g) → ↑f (∏ i in s, g i) = ∏ i in s, ↑f (g i)
hs : Set.Pairwise (↑s) (coprime on g) ∧ ∀ (b : ι), b ∈ ↑s → a ≠ b → (coprime on g) a b
⊢ coprime (g a) (∏ x in s, g x)
case insert
R : Type u_2
ι : Type u_1
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : IsMultiplicative f
s✝ : Finset ι
hs✝ : Set.Pairwise (↑s✝) (coprime on g)
a : ι
s : Finset ι
has : ¬a ∈ s
ih : Set.Pairwise (↑s) (coprime on g) → ↑f (∏ i in s, g i) = ∏ i in s, ↑f (g i)
hs : Set.Pairwise (↑s) (coprime on g) ∧ ∀ (b : ι), b ∈ ↑s → a ≠ b → (coprime on g) a b
⊢ ↑f (∏ i in insert a s, g i) = ∏ i in insert a s, ↑f (g i)
rw [prod_insert has, prod_insert has, hf.map_mul_of_coprime, ih hs.1]
no goals
case insert
R : Type u_2
ι : Type u_1
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : IsMultiplicative f
s✝ : Finset ι
hs✝ : Set.Pairwise (↑s✝) (coprime on g)
a : ι
s : Finset ι
has : ¬a ∈ s
ih : Set.Pairwise (↑s) (coprime on g) → ↑f (∏ i in s, g i) = ∏ i in s, ↑f (g i)
hs : Set.Pairwise (↑s) (coprime on g) ∧ ∀ (b : ι), b ∈ ↑s → a ≠ b → (coprime on g) a b
⊢ coprime (g a) (∏ x in s, g x)
exact Nat.coprime_prod_right fun i hi => hs.2 _ hi (hi.ne_of_not_mem has).symm
no goals
case empty
R : Type u_2
ι : Type u_1
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : IsMultiplicative f
s : Finset ι
hs✝ : Set.Pairwise (↑s) (coprime on g)
hs : Set.Pairwise (↑∅) (coprime on g)
⊢ ↑f (∏ i in ∅, g i) = ∏ i in ∅, ↑f (g i)
simp [hf]