-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coeff_prod [DecidableEq σ]
    (f : ι → MvPowerSeries σ 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:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff R (l i)) (f i)
d : σ →₀ ℕ
⊢ ∑ p ∈ antidiagonal d, (coeff R p.1) (f a) * (coeff R p.2) (∏ x ∈ s, f x) =
    ∑ x ∈ antidiagonal d,
      ∑ i ∈ Finset.map { toFun := fun f => (↑f).update a x.1, inj' := ⋯ } (s.finsuppAntidiag x.2).attach,
        ∏ i_1 ∈ insert a s, (coeff R (i i_1)) (f i_1)

Tactic:
apply Finset.sum_congr rfl

Result:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff R (l i)) (f i)
d : σ →₀ ℕ
⊢ ∀ x ∈ antidiagonal d,
    (coeff R x.1) (f a) * (coeff R x.2) (∏ x ∈ s, f x) =
      ∑ i ∈ Finset.map { toFun := fun f => (↑f).update a x.1, inj' := ⋯ } (s.finsuppAntidiag x.2).attach,
        ∏ i_1 ∈ insert a s, (coeff R (i i_1)) (f i_1)

Proof state:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff R (l i)) (f i)
d : σ →₀ ℕ
⊢ ∀ (a_1 b : σ →₀ ℕ),
    a_1 + b = d →
      (coeff R a_1) (f a) * (coeff R b) (∏ x ∈ s, f x) =
        ∑ x ∈ (s.finsuppAntidiag b).attach, ∏ x_1 ∈ insert a s, (coeff R (Function.update (⇑↑x) a a_1 x_1)) (f x_1)

Tactic:
rintro u v rfl

Result:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff R (l i)) (f i)
u v : σ →₀ ℕ
⊢ (coeff R u) (f a) * (coeff R v) (∏ x ∈ s, f x) =
    ∑ x ∈ (s.finsuppAntidiag v).attach, ∏ x_1 ∈ insert a s, (coeff R (Function.update (⇑↑x) a u x_1)) (f x_1)

Proof state:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff R (l i)) (f i)
u v : σ →₀ ℕ
⊢ ∀ a_1 ∈ s.finsuppAntidiag v,
    (coeff R u) (f a) * ∏ x ∈ s, (coeff R (a_1 x)) (f x) =
      (coeff R u) (f a) * ∏ x ∈ s, (coeff R (Function.update (⇑a_1) a u x)) (f x)

Tactic:
rintro x -

Result:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff R (l i)) (f i)
u v : σ →₀ ℕ
x : ι →₀ σ →₀ ℕ
⊢ (coeff R u) (f a) * ∏ x_1 ∈ s, (coeff R (x x_1)) (f x_1) =
    (coeff R u) (f a) * ∏ x_1 ∈ s, (coeff R (Function.update (⇑x) a u x_1)) (f x_1)

Proof state:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff R (l i)) (f i)
v u' v' : σ →₀ ℕ
k l : ι →₀ σ →₀ ℕ
huv : u' + v' = u' + v
h : u' = u' → ¬v = v'
hkl : l.update a u' = k.update a u'
⊢ False

Tactic:
simp only [add_right_inj] at huv

Result:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff R (l i)) (f i)
v u' v' : σ →₀ ℕ
k l : ι →₀ σ →₀ ℕ
h : u' = u' → ¬v = v'
hkl : l.update a u' = k.update a u'
huv : v' = v
⊢ False

Proof state:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff R (l i)) (f i)
u v : σ →₀ ℕ
x : ι →₀ σ →₀ ℕ
i : ι
hi : i ∈ s
⊢ (coeff R (x i)) (f i) = (coeff R (Function.update (⇑x) a u i)) (f i)

Tactic:
rw [Function.update_of_ne]

Result:
case insert.h
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff R (l i)) (f i)
u v : σ →₀ ℕ
x : ι →₀ σ →₀ ℕ
i : ι
hi : i ∈ s
⊢ i ≠ a

Proof state:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff R (l i)) (f i)
u v : σ →₀ ℕ
⊢ ∑ x ∈ (s.finsuppAntidiag v).attach, (coeff R u) (f a) * ∏ i ∈ s, (coeff R (↑x i)) (f i) =
    ∑ x ∈ (s.finsuppAntidiag v).attach, ∏ x_1 ∈ insert a s, (coeff R (Function.update (⇑↑x) a u x_1)) (f x_1)

Tactic:
apply Finset.sum_congr rfl

Result:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff R (l i)) (f i)
u v : σ →₀ ℕ
⊢ ∀ x ∈ (s.finsuppAntidiag v).attach,
    (coeff R u) (f a) * ∏ i ∈ s, (coeff R (↑x i)) (f i) =
      ∏ x_1 ∈ insert a s, (coeff R (Function.update (⇑↑x) a u x_1)) (f x_1)

Proof state:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff R (l i)) (f i)
u v : σ →₀ ℕ
x : ι →₀ σ →₀ ℕ
⊢ ∀ x_1 ∈ s, (coeff R (x x_1)) (f x_1) = (coeff R (Function.update (⇑x) a u x_1)) (f x_1)

Tactic:
intro i hi

Result:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff R (l i)) (f i)
u v : σ →₀ ℕ
x : ι →₀ σ →₀ ℕ
i : ι
hi : i ∈ s
⊢ (coeff R (x i)) (f i) = (coeff R (Function.update (⇑x) a u i)) (f i)

Proof state:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff R (l i)) (f i)
u v : σ →₀ ℕ
x : ι →₀ σ →₀ ℕ
⊢ (coeff R u) (f a) * ∏ x_1 ∈ s, (coeff R (x x_1)) (f x_1) =
    (coeff R u) (f a) * ∏ x_1 ∈ s, (coeff R (Function.update (⇑x) a u x_1)) (f x_1)

Tactic:
rw [Finset.prod_congr rfl]

Result:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff R (l i)) (f i)
u v : σ →₀ ℕ
x : ι →₀ σ →₀ ℕ
⊢ ∀ x_1 ∈ s, (coeff R (x x_1)) (f x_1) = (coeff R (Function.update (⇑x) a u x_1)) (f x_1)