awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
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)
⊢ 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)
have 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
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
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
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
⊢ 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)
have 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
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
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) ≠ n
⊢ coeff s
      (HPow.hPow (α := MvPolynomial σ R)
        ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) a : MvPolynomial σ R) n) =
    0
have simp : Eq.{u_1 + 1} (α := R)
  (∑ 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)
  0
Tactic: simp only [sum, linearCombination_apply, Finset.sum_pow_eq_sum_piAntidiag, coeff_sum, ← map_pow,
    ← C_eq_coe_nat, coeff_C_mul, smul_eq_C_mul, mul_pow, Finset.prod_mul_distrib, ← map_prod,
    coeff_prod_X_pow, mul_ite, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) ≠ n
⊢ Eq.{u_1 + 1} (α := R)
    (∑ 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)
    0
have apply : ∀ (x : σ → ℕ) (hx : 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) =
    0
Tactic: apply Finset.sum_eq_zero (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) ≠ n
x : σ → ℕ
hx : 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) =
    0
have hnc : ¬s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i
Tactic: rw [if_neg]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
n : ℕ
x : σ → ℕ
hx : x ∈ a.support.piAntidiag n
hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n
⊢ False
have hnc : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) = n
Tactic: apply hs
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (hypothesis)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
n : ℕ
x : σ → ℕ
hx : x ∈ a.support.piAntidiag n
hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n
⊢ (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) = n
have hx₁ : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support
Tactic: simp only [Finset.mem_piAntidiag] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
n : ℕ
x : σ → ℕ
hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n
hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support
⊢ (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) = n
have hnc : ∑ x_1 ∈ a.support, (indicator a.support fun (i : σ) (x_2 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) x_1 = a.support.sum x
Tactic: rw [sum_of_support_subset _ (support_indicator_subset a.support _) _ (by simp), ← hx.1]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
n : ℕ
x : σ → ℕ
hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n
hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support
⊢ ∑ x_1 ∈ a.support, (indicator a.support fun (i : σ) (x_2 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) x_1 = a.support.sum x
have hnc : (fun (x_1 : σ) ↦ (indicator a.support fun (i : σ) (x_2 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) x_1) = x
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
n : ℕ
x : σ → ℕ
hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n
hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support
⊢ (fun (x_1 : σ) ↦ (indicator a.support fun (i : σ) (x_2 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) x_1) = x
have hnc : ∀ (i : σ), (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) i = x i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
n : ℕ
x : σ → ℕ
hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n
hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support
i : σ
⊢ (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) i = x i
have pos : ∀ (hi : i ∈ a.support), (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) i = x i
Tactic: by_cases hi : i ∈ a.support
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
a : σ →₀ R
n : ℕ
x : σ → ℕ
hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n
hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support
i : σ
pos : ∀ (hi : i ∈ a.support), (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) i = x i
⊢ (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) i = x i
have neg : ∀ (hi : i ∉ a.support), (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i : (a : σ) → ℕ) i = x i
Tactic: by_cases hi : i ∈ a.support
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) ≠ n
⊢ coeff s
      (HPow.hPow (α := MvPolynomial σ R)
        ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) a : MvPolynomial σ R) n) =
    0
have simp : Eq.{u_1 + 1} (α := R)
  (∑ 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)
  0
Tactic: classical
  simp only [sum, linearCombination_apply, Finset.sum_pow_eq_sum_piAntidiag, coeff_sum, ← map_pow,
    ← C_eq_coe_nat, coeff_C_mul, smul_eq_C_mul, mul_pow, Finset.prod_mul_distrib, ← map_prod,
    coeff_prod_X_pow, mul_ite, mul_one, mul_zero]
  apply Finset.sum_eq_zero (fun x hx ↦ ?_)
  rw [if_neg]
  rintro ⟨rfl⟩
  apply hs
  simp only [Finset.mem_piAntidiag] at hx
  rw [sum_of_support_subset _ (support_indicator_subset a.support _) _ (by simp), ← hx.1]
  congr
  ext i
  by_cases hi : i ∈ a.support
  · simp [Finsupp.indicator_of_mem hi]
  · grind [Finsupp.indicator_of_notMem hi]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) ≠ n
simp :
  Eq.{u_1 + 1} (α := R)
    (∑ 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)
    0
⊢ coeff s
      (HPow.hPow (α := MvPolynomial σ R)
        ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) a : MvPolynomial σ R) n) =
    0
have simp₁ : ∀ (x : σ → ℕ) (hx : 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) =
    0
Tactic: classical
  simp only [sum, linearCombination_apply, Finset.sum_pow_eq_sum_piAntidiag, coeff_sum, ← map_pow,
    ← C_eq_coe_nat, coeff_C_mul, smul_eq_C_mul, mul_pow, Finset.prod_mul_distrib, ← map_prod,
    coeff_prod_X_pow, mul_ite, mul_one, mul_zero]
  apply Finset.sum_eq_zero (fun x hx ↦ ?_)
  rw [if_neg]
  rintro ⟨rfl⟩
  apply hs
  simp only [Finset.mem_piAntidiag] at hx
  rw [sum_of_support_subset _ (support_indicator_subset a.support _) _ (by simp), ← hx.1]
  congr
  ext i
  by_cases hi : i ∈ a.support
  · simp [Finsupp.indicator_of_mem hi]
  · grind [Finsupp.indicator_of_notMem hi]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) ≠ n
simp :
  Eq.{u_1 + 1} (α := R)
    (∑ 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)
    0
simp₁ :
  ∀ (x : σ → ℕ) (hx : 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) =
      0
⊢ coeff s
      (HPow.hPow (α := MvPolynomial σ R)
        ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) a : MvPolynomial σ R) n) =
    0
have hnc : ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n), ¬s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i
Tactic: classical
  simp only [sum, linearCombination_apply, Finset.sum_pow_eq_sum_piAntidiag, coeff_sum, ← map_pow,
    ← C_eq_coe_nat, coeff_C_mul, smul_eq_C_mul, mul_pow, Finset.prod_mul_distrib, ← map_prod,
    coeff_prod_X_pow, mul_ite, mul_one, mul_zero]
  apply Finset.sum_eq_zero (fun x hx ↦ ?_)
  rw [if_neg]
  rintro ⟨rfl⟩
  apply hs
  simp only [Finset.mem_piAntidiag] at hx
  rw [sum_of_support_subset _ (support_indicator_subset a.support _) _ (by simp), ← hx.1]
  congr
  ext i
  by_cases hi : i ∈ a.support
  · simp [Finsupp.indicator_of_mem hi]
  · grind [Finsupp.indicator_of_notMem hi]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) ≠ n
simp :
  Eq.{u_1 + 1} (α := R)
    (∑ 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)
    0
simp₁ :
  ∀ (x : σ → ℕ) (hx : 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) =
      0
hnc : ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n), ¬s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i
⊢ coeff s
      (HPow.hPow (α := MvPolynomial σ R)
        ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) a : MvPolynomial σ R) n) =
    0
have hnc₁ : ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n)
  (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n), False
Tactic: classical
  simp only [sum, linearCombination_apply, Finset.sum_pow_eq_sum_piAntidiag, coeff_sum, ← map_pow,
    ← C_eq_coe_nat, coeff_C_mul, smul_eq_C_mul, mul_pow, Finset.prod_mul_distrib, ← map_prod,
    coeff_prod_X_pow, mul_ite, mul_one, mul_zero]
  apply Finset.sum_eq_zero (fun x hx ↦ ?_)
  rw [if_neg]
  rintro ⟨rfl⟩
  apply hs
  simp only [Finset.mem_piAntidiag] at hx
  rw [sum_of_support_subset _ (support_indicator_subset a.support _) _ (by simp), ← hx.1]
  congr
  ext i
  by_cases hi : i ∈ a.support
  · simp [Finsupp.indicator_of_mem hi]
  · grind [Finsupp.indicator_of_notMem hi]
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) ≠ n
simp :
  Eq.{u_1 + 1} (α := R)
    (∑ 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)
    0
simp₁ :
  ∀ (x : σ → ℕ) (hx : 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) =
      0
hnc : ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n), ¬s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i
hnc₁ :
  ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n)
    (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n), False
⊢ coeff s
      (HPow.hPow (α := MvPolynomial σ R)
        ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) a : MvPolynomial σ R) n) =
    0
have hnc₂ : ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n)
  (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n),
  (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) = n
Tactic: classical
  simp only [sum, linearCombination_apply, Finset.sum_pow_eq_sum_piAntidiag, coeff_sum, ← map_pow,
    ← C_eq_coe_nat, coeff_C_mul, smul_eq_C_mul, mul_pow, Finset.prod_mul_distrib, ← map_prod,
    coeff_prod_X_pow, mul_ite, mul_one, mul_zero]
  apply Finset.sum_eq_zero (fun x hx ↦ ?_)
  rw [if_neg]
  rintro ⟨rfl⟩
  apply hs
  simp only [Finset.mem_piAntidiag] at hx
  rw [sum_of_support_subset _ (support_indicator_subset a.support _) _ (by simp), ← hx.1]
  congr
  ext i
  by_cases hi : i ∈ a.support
  · simp [Finsupp.indicator_of_mem hi]
  · grind [Finsupp.indicator_of_notMem hi]
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) ≠ n
simp :
  Eq.{u_1 + 1} (α := R)
    (∑ 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)
    0
simp₁ :
  ∀ (x : σ → ℕ) (hx : 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) =
      0
hnc : ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n), ¬s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i
hnc₁ :
  ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n)
    (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n), False
hnc₂ :
  ∀ (x : σ → ℕ) (hx : x ∈ a.support.piAntidiag n)
    (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n),
    (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) = n
⊢ coeff s
      (HPow.hPow (α := MvPolynomial σ R)
        ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) a : MvPolynomial σ R) n) =
    0
have hnc₃ : ∀ (x : σ → ℕ) (hs : (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) ≠ n)
  (hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support),
  (sum (indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i) fun (x : σ) (m : ℕ) ↦ m) = n
Tactic: classical
  simp only [sum, linearCombination_apply, Finset.sum_pow_eq_sum_piAntidiag, coeff_sum, ← map_pow,
    ← C_eq_coe_nat, coeff_C_mul, smul_eq_C_mul, mul_pow, Finset.prod_mul_distrib, ← map_prod,
    coeff_prod_X_pow, mul_ite, mul_one, mul_zero]
  apply Finset.sum_eq_zero (fun x hx ↦ ?_)
  rw [if_neg]
  rintro ⟨rfl⟩
  apply hs
  simp only [Finset.mem_piAntidiag] at hx
  rw [sum_of_support_subset _ (support_indicator_subset a.support _) _ (by simp), ← hx.1]
  congr
  ext i
  by_cases hi : i ∈ a.support
  · simp [Finsupp.indicator_of_mem hi]
  · grind [Finsupp.indicator_of_notMem hi]
Cleared hypotheses: s, hs