-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem map_prod {ι : Type*} [CommMonoidWithZero R] (g : ι → ℕ) {f : ArithmeticFunction R}
    (hf : f.IsMultiplicative) (s : Finset ι) (hs : (s : Set ι).Pairwise (Coprime on g)) :
    f (∏ i ∈ s, g i) = ∏ i ∈ s, f (g i)

Proof state:
case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (↑s✝).Pairwise (Coprime on g) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Coprime on g) a✝ b
⊢ f (∏ i ∈ insert a✝ s✝, g i) = ∏ i ∈ insert a✝ s✝, f (g i)

Tactic:
rw [prod_insert has, prod_insert has, hf.map_mul_of_coprime, ih hs.1]

Result:
case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (↑s✝).Pairwise (Coprime on g) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Coprime on g) a✝ b
⊢ (g a✝).Coprime (∏ x ∈ s✝, g x)

Proof state:
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
s : Finset ι
hs : (↑s).Pairwise (Coprime on g)
⊢ f (∏ i ∈ s, g i) = ∏ i ∈ s, f (g i)

Tactic:
induction s using Finset.induction_on with
| empty => simp [hf]
| insert has ih =>
  rw [coe_insert, Set.pairwise_insert_of_symmetric (Coprime.symmetric.comap g)] at hs
  rw [prod_insert has, prod_insert has, hf.map_mul_of_coprime, ih hs.1]
  exact .prod_right fun i hi => hs.2 _ hi (hi.ne_of_not_mem has).symm

Result:
no goals

Proof state:
case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (↑(insert a✝ s✝)).Pairwise (Coprime on g)
⊢ f (∏ i ∈ insert a✝ s✝, g i) = ∏ i ∈ insert a✝ s✝, f (g i)

Tactic:
rw [coe_insert, Set.pairwise_insert_of_symmetric (Coprime.symmetric.comap g)] at hs

Result:
case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (↑s✝).Pairwise (Coprime on g) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Coprime on g) a✝ b
⊢ f (∏ i ∈ insert a✝ s✝, g i) = ∏ i ∈ insert a✝ s✝, f (g i)

Proof state:
case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (↑s✝).Pairwise (Coprime on g) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Coprime on g) a✝ b
⊢ (g a✝).Coprime (∏ x ∈ s✝, g x)

Tactic:
exact .prod_right fun i hi => hs.2 _ hi (hi.ne_of_not_mem has).symm

Result:
no goals

Proof state:
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
s : Finset ι
hs : (↑s).Pairwise (Coprime on g)
⊢ f (∏ i ∈ s, g i) = ∏ i ∈ s, f (g i)

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp [hf]
  | insert has ih =>
    rw [coe_insert, Set.pairwise_insert_of_symmetric (Coprime.symmetric.comap g)] at hs
    rw [prod_insert has, prod_insert has, hf.map_mul_of_coprime, ih hs.1]
    exact .prod_right fun i hi => hs.2 _ hi (hi.ne_of_not_mem has).symm

Result:
no goals

Proof state:
case empty
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
hs : (↑∅).Pairwise (Coprime on g)
⊢ f (∏ i ∈ ∅, g i) = ∏ i ∈ ∅, f (g i)

Tactic:
simp [hf]

Result:
no goals