-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
s : Finset ι
empty :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ ∅, f j) : R)
      (∑ l ∈ finsuppAntidiag ∅ d, ∏ i ∈ ∅, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R)
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (ih :
      ∀ (d : σ →₀ ℕ),
        Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ s, f j) : R)
          (∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) :
            R))
    (d : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ Insert.insert a s, f j) : R)
      (∑ l ∈ (Insert.insert a s).finsuppAntidiag d,
          ∏ i ∈ Insert.insert a s, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) :
        R)
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ s, f j) : R)
    (∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R)

Tactic:
induction s using Finset.induction_on generalizing d with
  | empty =>
    simp only [prod_empty, sum_const, nsmul_eq_mul, mul_one, coeff_one, finsuppAntidiag_empty]
    split_ifs
    · simp only [card_singleton, Nat.cast_one]
    · simp only [card_empty, Nat.cast_zero]
  | insert a s ha ih =>
    rw [finsuppAntidiag_insert ha, prod_insert ha, coeff_mul, sum_biUnion]
    · apply Finset.sum_congr rfl
      simp only [mem_antidiagonal, sum_map, Function.Embedding.coeFn_mk, coe_update, Prod.forall]
      rintro u v rfl
      rw [ih, Finset.mul_sum, ← Finset.sum_attach]
      apply Finset.sum_congr rfl
      simp only [mem_attach, Finset.prod_insert ha, Function.update_self, forall_true_left,
        Subtype.forall]
      rintro x -
      rw [Finset.prod_congr rfl]
      intro i hi
      rw [Function.update_of_ne]
      exact ne_of_mem_of_not_mem hi ha
    · 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]
      rintro u v rfl u' v' huv h k - l - hkl
      obtain rfl : u' = u := by
        simpa only [Finsupp.coe_update, Function.update_self] using DFunLike.congr_fun hkl a
      simp only [add_right_inj] at huv
      exact h rfl huv.symm

Premises used: Finset.mul_sum, forall_true_left, Finset.prod_empty, and_imp, Set.PairwiseDisjoint, Finset.sum_map, Finset.mem_attach, Subtype.exists, forall_exists_index, not_exists, Finset.sum_attach, Subtype.forall, Insert.insert, MvPowerSeries.coeff_one, Finset.prod_congr, exists_prop, Set.Pairwise, Finsupp.coe_update, ne_eq, Finset.HasAntidiagonal.mem_antidiagonal, Finset.card_empty, Prod.mk.injEq, Finset.finsuppAntidiag_empty, Function.Embedding.coeFn_mk, nsmul_eq_mul, Prod.forall, Finset.sum_biUnion, Nat.cast_zero, Finset.disjoint_left, Function.update_self, Finset.mem_map, mul_one, not_and, Nat.cast_one, add_right_inj, Finset.mem_coe, Finset.sum_congr, forall_apply_eq_imp_iff₂, rfl, true_and, MvPowerSeries.coeff_mul, Finset.sum_const, Finset.card_singleton, Function.update_of_ne