-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_prod (f : ι → PowerSeries R) (d : ℕ) (s : Finset ι) :
    coeff R d (∏ j ∈ s, f j) = ∑ l ∈ finsuppAntidiag s d, ∏ i ∈ s, coeff R (l i) (f i)

Proof state:
R : Type u_2
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
x : ι →₀ ℕ
a✝¹ : x ∈ s.finsuppAntidiag d
i : ι
a✝ : i ∈ s
⊢ (MvPowerSeries.coeff R (((Finsupp.mapRange.addEquiv AddEquiv.finsuppUnique.symm).toEmbedding x) i)) (f i) =
    (MvPowerSeries.coeff R (single () (x i))) (f i)

Tactic:
congr 2

Result:
case e_a.e_n
R : Type u_2
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
x : ι →₀ ℕ
a✝¹ : x ∈ s.finsuppAntidiag d
i : ι
a✝ : i ∈ s
⊢ ((Finsupp.mapRange.addEquiv AddEquiv.finsuppUnique.symm).toEmbedding x) i = single () (x i)

Proof state:
R : Type u_2
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
⊢ ∀ x ∈ s.finsuppAntidiag d,
    ∏ i ∈ s, (MvPowerSeries.coeff R (((Finsupp.mapRange.addEquiv AddEquiv.finsuppUnique.symm).toEmbedding x) i)) (f i) =
      ∏ x_1 ∈ s, (MvPowerSeries.coeff R (single () (x x_1))) (f x_1)

Tactic:
intro x _

Result:
R : Type u_2
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
x : ι →₀ ℕ
a✝ : x ∈ s.finsuppAntidiag d
⊢ ∏ i ∈ s, (MvPowerSeries.coeff R (((Finsupp.mapRange.addEquiv AddEquiv.finsuppUnique.symm).toEmbedding x) i)) (f i) =
    ∏ x_1 ∈ s, (MvPowerSeries.coeff R (single () (x x_1))) (f x_1)

Proof state:
R : Type u_2
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
x : ι →₀ ℕ
a✝ : x ∈ s.finsuppAntidiag d
⊢ ∀ x_1 ∈ s,
    (MvPowerSeries.coeff R (((Finsupp.mapRange.addEquiv AddEquiv.finsuppUnique.symm).toEmbedding x) x_1)) (f x_1) =
      (MvPowerSeries.coeff R (single () (x x_1))) (f x_1)

Tactic:
intro i _

Result:
R : Type u_2
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
x : ι →₀ ℕ
a✝¹ : x ∈ s.finsuppAntidiag d
i : ι
a✝ : i ∈ s
⊢ (MvPowerSeries.coeff R (((Finsupp.mapRange.addEquiv AddEquiv.finsuppUnique.symm).toEmbedding x) i)) (f i) =
    (MvPowerSeries.coeff R (single () (x i))) (f i)

Proof state:
R : Type u_2
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
⊢ (MvPowerSeries.coeff R (single () d)) (∏ j ∈ s, f j) =
    ∑ x ∈ s.finsuppAntidiag d, ∏ x_1 ∈ s, (MvPowerSeries.coeff R (single () (x x_1))) (f x_1)

Tactic:
rw [MvPowerSeries.coeff_prod, ← AddEquiv.finsuppUnique_symm d, ← mapRange_finsuppAntidiag_eq,
  sum_map, sum_congr rfl]

Result:
R : Type u_2
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
⊢ ∀ x ∈ s.finsuppAntidiag d,
    ∏ i ∈ s, (MvPowerSeries.coeff R (((Finsupp.mapRange.addEquiv AddEquiv.finsuppUnique.symm).toEmbedding x) i)) (f i) =
      ∏ x_1 ∈ s, (MvPowerSeries.coeff R (single () (x x_1))) (f x_1)

Proof state:
R : Type u_2
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
⊢ (coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff R (l i)) (f i)

Tactic:
simp only [coeff]

Result:
R : Type u_2
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
⊢ (MvPowerSeries.coeff R (single () d)) (∏ j ∈ s, f j) =
    ∑ x ∈ s.finsuppAntidiag d, ∏ x_1 ∈ s, (MvPowerSeries.coeff R (single () (x x_1))) (f x_1)

Proof state:
R : Type u_2
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
x : ι →₀ ℕ
a✝ : x ∈ s.finsuppAntidiag d
⊢ ∏ i ∈ s, (MvPowerSeries.coeff R (((Finsupp.mapRange.addEquiv AddEquiv.finsuppUnique.symm).toEmbedding x) i)) (f i) =
    ∏ x_1 ∈ s, (MvPowerSeries.coeff R (single () (x x_1))) (f x_1)

Tactic:
apply prod_congr rfl

Result:
R : Type u_2
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
x : ι →₀ ℕ
a✝ : x ∈ s.finsuppAntidiag d
⊢ ∀ x_1 ∈ s,
    (MvPowerSeries.coeff R (((Finsupp.mapRange.addEquiv AddEquiv.finsuppUnique.symm).toEmbedding x) x_1)) (f x_1) =
      (MvPowerSeries.coeff R (single () (x x_1))) (f x_1)

Proof state:
case e_a.e_n
R : Type u_2
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
x : ι →₀ ℕ
a✝¹ : x ∈ s.finsuppAntidiag d
i : ι
a✝ : i ∈ s
⊢ ((Finsupp.mapRange.addEquiv AddEquiv.finsuppUnique.symm).toEmbedding x) i = single () (x i)

Tactic:
simp only [AddEquiv.toEquiv_eq_coe, Finsupp.mapRange.addEquiv_toEquiv, AddEquiv.toEquiv_symm,
  Equiv.coe_toEmbedding, Finsupp.mapRange.equiv_apply, AddEquiv.coe_toEquiv_symm,
  Finsupp.mapRange_apply, AddEquiv.finsuppUnique_symm]

Result:
no goals