-- 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 neg
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
h✝ : ¬d = 0
⊢ 0 = ↑(#∅)

Tactic:
simp only [card_empty, Nat.cast_zero]

Result:
no goals

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 : σ →₀ ℕ
⊢ ∀ 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)

Tactic:
simp only [mem_antidiagonal, sum_map, Function.Embedding.coeFn_mk, coe_update, Prod.forall]

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 : σ →₀ ℕ
⊢ ∀ (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)

Proof state:
case empty
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
⊢ (if d = 0 then 1 else 0) = ↑(#(if d = 0 then {0} else ∅))

Tactic:
split_ifs

Result:
case pos
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
h✝ : d = 0
⊢ 1 = ↑(#{0})

case neg
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
h✝ : ¬d = 0
⊢ 0 = ↑(#∅)

Proof state:
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

Tactic:
exact ne_of_mem_of_not_mem hi ha

Result:
no goals

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 : σ →₀ ℕ
⊢ (↑(antidiagonal d)).PairwiseDisjoint fun p =>
    Finset.map { toFun := fun f => (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach

Tactic:
simp only [Set.PairwiseDisjoint, Set.Pairwise, mem_coe, mem_antidiagonal, ne_eq,
  disjoint_left, mem_map, mem_attach, Function.Embedding.coeFn_mk, true_and, Subtype.exists,
  exists_prop, not_exists, not_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
  Prod.forall, Prod.mk.injEq]

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 : σ →₀ ℕ
⊢ ∀ (a_1 b : σ →₀ ℕ),
    a_1 + b = d →
      ∀ (a_3 b_1 : σ →₀ ℕ),
        a_3 + b_1 = d →
          (a_1 = a_3 → ¬b = b_1) →
            ∀ a_6 ∈ s.finsuppAntidiag b, ∀ x ∈ s.finsuppAntidiag b_1, ¬x.update a a_3 = a_6.update a a_1

Proof state:
case empty
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
⊢ (coeff R d) (∏ j ∈ ∅, f j) = ∑ l ∈ ∅.finsuppAntidiag d, ∏ i ∈ ∅, (coeff R (l i)) (f i)

Tactic:
simp only [prod_empty, sum_const, nsmul_eq_mul, mul_one, coeff_one, finsuppAntidiag_empty]

Result:
case empty
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
⊢ (if d = 0 then 1 else 0) = ↑(#(if d = 0 then {0} else ∅))

Proof state:
case pos
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
h✝ : d = 0
⊢ 1 = ↑(#{0})

Tactic:
simp only [card_singleton, Nat.cast_one]

Result:
no goals

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 : ι →₀ σ →₀ ℕ
h : u' = u' → ¬v = v'
hkl : l.update a u' = k.update a u'
huv : v' = v
⊢ False

Tactic:
exact h rfl huv.symm

Result:
no goals

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 u' v' : σ →₀ ℕ
huv : u' + v' = u + v
h : u = u' → ¬v = v'
k l : ι →₀ σ →₀ ℕ
hkl : l.update a u' = k.update a u
⊢ False

Tactic:
obtain rfl : u' = u := by
  simpa only [Finsupp.coe_update, Function.update_self] using DFunLike.congr_fun hkl a

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 : ι →₀ σ →₀ ℕ
huv : u' + v' = u' + v
h : u' = u' → ¬v = v'
hkl : l.update a u' = k.update a u'
⊢ 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)
d : σ →₀ ℕ
⊢ ∀ (a_1 b : σ →₀ ℕ),
    a_1 + b = d →
      ∀ (a_3 b_1 : σ →₀ ℕ),
        a_3 + b_1 = d →
          (a_1 = a_3 → ¬b = b_1) →
            ∀ a_6 ∈ s.finsuppAntidiag b, ∀ x ∈ s.finsuppAntidiag b_1, ¬x.update a a_3 = a_6.update a a_1

Tactic:
rintro u v rfl u' v' huv h k - l - hkl

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 u' v' : σ →₀ ℕ
huv : u' + v' = u + v
h : u = u' → ¬v = v'
k l : ι →₀ σ →₀ ℕ
hkl : l.update a u' = k.update a u
⊢ False