-- Module: Mathlib.Algebra.MvPolynomial.Coeff
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) = n
simp :
  (∑ x ∈ a.support.piAntidiag n,
      if s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i then
        HMul.hMul (α := R) (↑(Nat.multinomial a.support x) : R)
          (∏ x_1 ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x_1 : R) (x x_1))
      else 0) =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
simp₁ :
  (if s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ (s : (a : σ) → ℕ) i then
      HMul.hMul (α := R) (↑(Nat.multinomial a.support (⇑s : (a : σ) → ℕ)) : R)
        (∏ x ∈ a.support, HPow.hPow (α := R) (β := ℕ) ((a : (a : σ) → R) x : R) ((s : (a : σ) → ℕ) x : ℕ))
    else 0) =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
h₀ :
  ∀ b ∈ a.support.piAntidiag n,
    b ≠ (⇑s : (a : σ) → ℕ) →
      (if s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ b i then
          HMul.hMul (α := R) (↑(Nat.multinomial a.support b) : R)
            (∏ x ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x : R) (b x))
        else 0) =
        0
h₁ :
  (⇑s : (a : σ) → ℕ) ∉ a.support.piAntidiag n →
    (if s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ (s : (a : σ) → ℕ) i then
        HMul.hMul (α := R) (↑(Nat.multinomial a.support (⇑s : (a : σ) → ℕ)) : R)
          (∏ x ∈ a.support, HPow.hPow (α := R) (β := ℕ) ((a : (a : σ) → R) x : R) ((s : (a : σ) → ℕ) x : ℕ))
      else 0) =
      0
h₂ :
  ∀ b ∈ a.support.piAntidiag n,
    b ≠ (⇑s : (a : σ) → ℕ) →
      (if s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ b i then
          HMul.hMul (α := R) (↑(Nat.multinomial a.support b) : R)
            (∏ x ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x : R) (b x))
        else 0) =
        0
h₃ h₄ :
  (⇑s : (a : σ) → ℕ) ∉ a.support.piAntidiag n →
    (if s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ (s : (a : σ) → ℕ) i then
        HMul.hMul (α := R) (↑(Nat.multinomial a.support (⇑s : (a : σ) → ℕ)) : R)
          (∏ x ∈ a.support, HPow.hPow (α := R) (β := ℕ) ((a : (a : σ) → R) x : R) ((s : (a : σ) → ℕ) x : ℕ))
      else 0) =
      0
⊢ coeff s
      (HPow.hPow (α := MvPolynomial σ R)
        ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) a : MvPolynomial σ R) n) =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)

Tactic:
classical
  simp only [sum, linearCombination_apply, Finset.sum_pow_eq_sum_piAntidiag, coeff_sum,
    ← C_eq_coe_nat, coeff_C_mul, smul_eq_C_mul, mul_pow, Finset.prod_mul_distrib, ← map_pow,
    ← map_prod, coeff_prod_X_pow, mul_ite, mul_one, mul_zero]
  rw [Finset.sum_eq_single (s : σ → ℕ)]
  · simp_rw [eq_indicator_self_iff]
    split_ifs with hs'
    · rw [prod_of_support_subset _ hs' _ (by simp), Finsupp.multinomial_of_support_subset hs']
    · rw [Finset.subset_iff] at hs'
      simp only [Finsupp.mem_support_iff, ne_eq, not_forall, Decidable.not_not] at hs'
      obtain ⟨i, hsi, hai⟩ := hs'
      rw [← mul_prod_erase _ i _ (by simpa), hai, zero_pow hsi, zero_mul, mul_zero]
  · simp only [Finset.mem_piAntidiag, ne_eq, Finsupp.mem_support_iff, ite_eq_right_iff, and_imp]
    intro _ _ _ _ hed
    simp [Finsupp.ext_iff] at hed
    grind
  · simp_rw [ite_eq_right_iff]
    intro hs' hs''
    rw [eq_indicator_self_iff] at hs''
    exfalso
    rw [Finset.mem_piAntidiag, not_and_or] at hs'
    rcases hs' with hs' | hs'
    · apply hs'
      rw [← hs, sum_of_support_subset _ hs'' _ (by simp)]
    · grind

Premises used: Finset.sum_pow_eq_sum_piAntidiag, Finsupp.mem_support_iff, Finset.prod_mul_distrib, and_imp, MulZeroClass.zero_mul, Finsupp.sum, MvPolynomial.coeff_C_mul, mul_ite, map_pow, Finset.mem_piAntidiag, MvPolynomial.coeff_prod_X_pow, Finsupp.linearCombination_apply, ne_eq, map_prod, Finset.sum_eq_single, MulZeroClass.mul_zero, ite_eq_right_iff, Finset.subset_iff, Finsupp.eq_indicator_self_iff, MvPolynomial.C_eq_coe_nat, not_and_or, Decidable.not_not, MvPolynomial.smul_eq_C_mul, mul_one, mul_pow, Classical.not_forall, Finsupp.ext_iff, DFunLike.coe, MvPolynomial.coeff_sum