awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Cardinal
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
inst_1 : Nonempty σ
inst_2 : Nontrivial R
⊢ #(MvPolynomial σ R) = max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀

Tactic:
simp [sup_assoc]

Premises used: sup_assoc
-- Module: Mathlib.Algebra.MvPolynomial.Cardinal
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
inst_1 : IsEmpty σ
⊢ #(MvPolynomial σ R) = lift.{u, v} #R

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Cardinal
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
inst_1 : Subsingleton R
⊢ #(MvPolynomial σ R) = 1

Tactic:
mk_eq_one _

Premises used: Cardinal.mk_eq_one
-- Module: Mathlib.Algebra.MvPolynomial.Cardinal
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.MvPolynomial.Cardinal
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
h : Nontrivial R
inl : IsEmpty σ → #(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀
inr : Nonempty σ → #(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀
⊢ #(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀

Tactic:
cases isEmpty_or_nonempty σ

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Algebra.MvPolynomial.Cardinal
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
h : Nontrivial R
h_1 : IsEmpty σ
⊢ #(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Cardinal
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
h : Nontrivial R
h_1 : Nonempty σ
⊢ #(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Cardinal
Goal:
σ R : Type u
inst : CommSemiring R
inst_1 : Nonempty σ
inst_2 : Nontrivial R
⊢ #(MvPolynomial σ R) = max (max #R #σ) ℵ₀

Tactic:
simp [sup_assoc]

Premises used: sup_assoc
-- Module: Mathlib.Algebra.MvPolynomial.Cardinal
Goal:
σ R : Type u
inst : CommSemiring R
inst_1 : IsEmpty σ
⊢ #(MvPolynomial σ R) = #R

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Cardinal
Goal:
σ R : Type u
inst : CommSemiring R
rw : max (max (#R) (lift.{u, u} #σ)) ℵ₀ ≤ max (max #R #σ) ℵ₀
rw₁ rw₂ : max (max #R #σ) ℵ₀ ≤ max (max #R #σ) ℵ₀
⊢ max (max (lift.{u, u} #R) (lift.{u, u} #σ)) ℵ₀ ≤ max (max #R #σ) ℵ₀

Tactic:
rw [lift_id, lift_id]

Premises used: Cardinal.lift_id
-- 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)
⊢ 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:
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]

Premises used: Finset.sum_pow_eq_sum_piAntidiag, Finset.prod_mul_distrib, Finsupp.sum, MvPolynomial.coeff_C_mul, mul_ite, map_pow, MvPolynomial.coeff_prod_X_pow, Finsupp.linearCombination_apply, map_prod, MulZeroClass.mul_zero, MvPolynomial.C_eq_coe_nat, MvPolynomial.smul_eq_C_mul, mul_one, mul_pow, MvPolynomial.coeff_sum
-- 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
rw :
  (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
⊢ (∑ 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)

Tactic:
rw [Finset.sum_eq_single (s : σ → ℕ)]

Premises used: Finset.sum_eq_single, DFunLike.coe
-- 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_rw :
  (if s.support ⊆ a.support 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)
⊢ (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)

Tactic:
simp_rw [eq_indicator_self_iff]

Premises used: Finsupp.eq_indicator_self_iff
-- 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
pos :
  ∀ (hs' : s.support ⊆ a.support),
    HMul.hMul (α := R) (↑(Nat.multinomial a.support (⇑s : (a : σ) → ℕ)) : R)
        (∏ x ∈ a.support, HPow.hPow (α := R) (β := ℕ) ((a : (a : σ) → R) x : R) ((s : (a : σ) → ℕ) x : ℕ)) =
      HMul.hMul (α := R) (↑s.multinomial : R)
        (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
neg :
  ∀ (hs' : ¬s.support ⊆ a.support),
    0 =
      HMul.hMul (α := R) (↑s.multinomial : R)
        (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
⊢ (if s.support ⊆ a.support 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)

Tactic:
split_ifs with hs'
-- 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
hs' : s.support ⊆ a.support
⊢ ∀ i ∈ a.support, HPow.hPow (α := R) (β := ℕ) ((a : (a : σ) → R) i : R) 0 = 1

Tactic:
simp
-- 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
hs' : s.support ⊆ a.support
pos :
  HMul.hMul (α := R) (↑(Nat.multinomial a.support (⇑s : (a : σ) → ℕ)) : R)
      (∏ x ∈ a.support, HPow.hPow (α := R) (β := ℕ) ((a : (a : σ) → R) x : R) ((s : (a : σ) → ℕ) x : ℕ)) =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (∏ x ∈ a.support, HPow.hPow (α := R) (β := ℕ) ((a : (a : σ) → R) x : R) ((s : (a : σ) → ℕ) x : ℕ))
pos₁ pos₂ :
  HMul.hMul (α := R) (↑s.multinomial : R)
      (∏ x ∈ a.support, HPow.hPow (α := R) (β := ℕ) ((a : (a : σ) → R) x : R) ((s : (a : σ) → ℕ) x : ℕ)) =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (∏ x ∈ a.support, HPow.hPow (α := R) (β := ℕ) ((a : (a : σ) → R) x : R) ((s : (a : σ) → ℕ) x : ℕ))
⊢ HMul.hMul (α := R) (↑(Nat.multinomial a.support (⇑s : (a : σ) → ℕ)) : R)
      (∏ x ∈ a.support, HPow.hPow (α := R) (β := ℕ) ((a : (a : σ) → R) x : R) ((s : (a : σ) → ℕ) x : ℕ)) =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)

Tactic:
rw [prod_of_support_subset _ hs' _ (by simp), Finsupp.multinomial_of_support_subset hs']

Premises used: Finsupp.multinomial_of_support_subset, Finsupp.prod_of_support_subset
-- 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
hs' : ¬s.support ⊆ a.support
⊢ ¬∀ ⦃x : σ⦄, x ∈ s.support → x ∈ a.support

Tactic:
rw [Finset.subset_iff] at hs'

Premises used: Finset.subset_iff
-- 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
hs' : ¬∀ ⦃x : σ⦄, x ∈ s.support → x ∈ a.support
⊢ ∃ (x : σ) (_ : ¬Eq (α := ℕ) ((s : (a : σ) → ℕ) x : ℕ) (0 : ℕ)),
    Eq.{u_1 + 1} (α := R) ((a : (a : σ) → R) x : R) (0 : R)

Tactic:
simp only [Finsupp.mem_support_iff, ne_eq, not_forall, Decidable.not_not] at hs'

Premises used: Finsupp.mem_support_iff, ne_eq, Decidable.not_not, Classical.not_forall
-- 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
hs' :
  ∃ (x : σ) (_ : ¬Eq (α := ℕ) ((s : (a : σ) → ℕ) x : ℕ) (0 : ℕ)),
    Eq.{u_1 + 1} (α := R) ((a : (a : σ) → R) x : R) (0 : R)
neg :
  ∀ (i : σ) (hsi : ¬Eq (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) (0 : ℕ))
    (hai : Eq.{u_1 + 1} (α := R) ((a : (a : σ) → R) i : R) (0 : R)),
    0 =
      HMul.hMul (α := R) (↑s.multinomial : R)
        (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
⊢ 0 =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)

Tactic:
obtain ⟨i, hsi, hai⟩ := hs'
-- 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
i : σ
hsi : ¬Eq (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
hai : Eq.{u_1 + 1} (α := R) ((a : (a : σ) → R) i : R) (0 : R)
⊢ i ∈ s.support

Tactic:
simpa
-- 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
i : σ
hsi : ¬Eq (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
hai : Eq.{u_1 + 1} (α := R) ((a : (a : σ) → R) i : R) (0 : R)
neg :
  0 =
    (↑s.multinomial : R) *
      (HPow.hPow (α := R) (β := ℕ) ((a : (a : σ) → R) i : R) ((s : (a : σ) → ℕ) i : ℕ) *
        (erase i s).prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
neg₁ :
  0 =
    (↑s.multinomial : R) *
      (HPow.hPow (α := R) (β := ℕ) 0 ((s : (a : σ) → ℕ) i : ℕ) *
        (erase i s).prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
neg₂ :
  0 =
    (↑s.multinomial : R) *
      HMul.hMul (α := R) 0 ((erase i s).prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
neg₃ : 0 = HMul.hMul (α := R) (↑s.multinomial : R) 0
neg₄ neg₅ : Eq.{u_1 + 1} (α := R) 0 0
⊢ 0 =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)

Tactic:
rw [← mul_prod_erase _ i _ (by simpa), hai, zero_pow hsi, zero_mul, mul_zero]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, Finsupp.mul_prod_erase, zero_pow
-- 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
h₀ :
  ∀ (b : (a : σ) → ℕ),
    a.support.sum b = n →
      (∀ (i : σ), ¬b i = 0 → ¬Eq.{u_1 + 1} (α := R) ((a : (a : σ) → R) i : R) (0 : R)) →
        ¬b = (⇑s : (a : σ) → ℕ) →
          (s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ b i) →
            HMul.hMul (α := R) (↑(Nat.multinomial a.support b) : R)
                (∏ x ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x : R) (b x)) =
              0
⊢ ∀ 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:
simp only [Finset.mem_piAntidiag, ne_eq, Finsupp.mem_support_iff, ite_eq_right_iff, and_imp]

Premises used: Finsupp.mem_support_iff, and_imp, Finset.mem_piAntidiag, ne_eq, ite_eq_right_iff
-- 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
b : (a : σ) → ℕ
h₀ :
  a.support.sum b = n →
    (∀ (i : σ), ¬b i = 0 → ¬Eq.{u_1 + 1} (α := R) ((a : (a : σ) → R) i : R) (0 : R)) →
      ¬b = (⇑s : (a : σ) → ℕ) →
        (s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ b i) →
          HMul.hMul (α := R) (↑(Nat.multinomial a.support b) : R)
              (∏ x ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x : R) (b x)) =
            0
⊢ a.support.sum b = n →
    (∀ (i : σ), ¬b i = 0 → ¬Eq.{u_1 + 1} (α := R) ((a : (a : σ) → R) i : R) (0 : R)) →
      ¬b = (⇑s : (a : σ) → ℕ) →
        (s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ b i) →
          HMul.hMul (α := R) (↑(Nat.multinomial a.support b) : R)
              (∏ x ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x : R) (b x)) =
            0

Tactic:
_
-- 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
b : (a : σ) → ℕ
h : a.support.sum b = n
h₀ :
  (∀ (i : σ), ¬b i = 0 → ¬Eq.{u_1 + 1} (α := R) ((a : (a : σ) → R) i : R) (0 : R)) →
    ¬b = (⇑s : (a : σ) → ℕ) →
      (s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ b i) →
        HMul.hMul (α := R) (↑(Nat.multinomial a.support b) : R)
            (∏ x ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x : R) (b x)) =
          0
⊢ (∀ (i : σ), ¬b i = 0 → ¬Eq.{u_1 + 1} (α := R) ((a : (a : σ) → R) i : R) (0 : R)) →
    ¬b = (⇑s : (a : σ) → ℕ) →
      (s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ b i) →
        HMul.hMul (α := R) (↑(Nat.multinomial a.support b) : R)
            (∏ x ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x : R) (b x)) =
          0

Tactic:
_
-- 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
b : (a : σ) → ℕ
h : a.support.sum b = n
h_1 : ∀ (i : σ), ¬b i = 0 → ¬Eq.{u_1 + 1} (α := R) ((a : (a : σ) → R) i : R) (0 : R)
h₀ :
  ¬b = (⇑s : (a : σ) → ℕ) →
    (s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ b i) →
      HMul.hMul (α := R) (↑(Nat.multinomial a.support b) : R)
          (∏ x ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x : R) (b x)) =
        0
⊢ ¬b = (⇑s : (a : σ) → ℕ) →
    (s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ b i) →
      HMul.hMul (α := R) (↑(Nat.multinomial a.support b) : R)
          (∏ x ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x : R) (b x)) =
        0

Tactic:
_
-- 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
b : (a : σ) → ℕ
h : a.support.sum b = n
h_1 : ∀ (i : σ), ¬b i = 0 → ¬Eq.{u_1 + 1} (α := R) ((a : (a : σ) → R) i : R) (0 : R)
h_2 : ¬b = (⇑s : (a : σ) → ℕ)
hed : s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ b i
⊢ ∀ (a_1 : σ), (s : (a : σ) → ℕ) a_1 = if Eq.{u_1 + 1} (α := R) ((a : (a : σ) → R) a_1 : R) (0 : R) then 0 else b a_1

Tactic:
simp [Finsupp.ext_iff] at hed

Premises used: Finsupp.ext_iff
-- 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
b : (a : σ) → ℕ
h : a.support.sum b = n
h_1 : ∀ (i : σ), ¬b i = 0 → ¬Eq.{u_1 + 1} (α := R) ((a : (a : σ) → R) i : R) (0 : R)
h_2 : ¬b = (⇑s : (a : σ) → ℕ)
hed :
  ∀ (a_1 : σ), (s : (a : σ) → ℕ) a_1 = if Eq.{u_1 + 1} (α := R) ((a : (a : σ) → R) a_1 : R) (0 : R) then 0 else b a_1
⊢ HMul.hMul (α := R) (↑(Nat.multinomial a.support b) : R)
      (∏ x ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x : R) (b x)) =
    0

Tactic:
grind
-- 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
h₁ :
  (⇑s : (a : σ) → ℕ) ∉ a.support.piAntidiag n →
    (s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ (s : (a : σ) → ℕ) i) →
      HMul.hMul (α := R) (↑(Nat.multinomial a.support (⇑s : (a : σ) → ℕ)) : R)
          (∏ x ∈ a.support, HPow.hPow (α := R) (β := ℕ) ((a : (a : σ) → R) x : R) ((s : (a : σ) → ℕ) x : ℕ)) =
        0
⊢ (⇑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:
simp_rw [ite_eq_right_iff]

Premises used: ite_eq_right_iff
-- 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
hs' : (⇑s : (a : σ) → ℕ) ∉ a.support.piAntidiag n
hs'' : s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ (s : (a : σ) → ℕ) i
⊢ s.support ⊆ a.support

Tactic:
rw [eq_indicator_self_iff] at hs''

Premises used: Finsupp.eq_indicator_self_iff
-- 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
hs' : (⇑s : (a : σ) → ℕ) ∉ a.support.piAntidiag n
hs'' : s.support ⊆ a.support
h₁ : False
⊢ HMul.hMul (α := R) (↑(Nat.multinomial a.support (⇑s : (a : σ) → ℕ)) : R)
      (∏ x ∈ a.support, HPow.hPow (α := R) (β := ℕ) ((a : (a : σ) → R) x : R) ((s : (a : σ) → ℕ) x : ℕ)) =
    0

Tactic:
exfalso
-- 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
hs' : (⇑s : (a : σ) → ℕ) ∉ a.support.piAntidiag n
hs'' : s.support ⊆ a.support
⊢ ¬a.support.sum (⇑s : (a : σ) → ℕ) = n ∨ ¬∀ (i : σ), Ne (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) (0 : ℕ) → i ∈ a.support

Tactic:
rw [Finset.mem_piAntidiag, not_and_or] at hs'

Premises used: Finset.mem_piAntidiag, not_and_or
-- 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
hs' : (⇑s : (a : σ) → ℕ) ∉ a.support.piAntidiag n
hs'' : s.support ⊆ a.support
hs'₁ : ¬a.support.sum (⇑s : (a : σ) → ℕ) = n ∨ ¬∀ (i : σ), Ne (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) (0 : ℕ) → i ∈ a.support
⊢ s.support ⊆ a.support

Tactic:
rw [Finset.mem_piAntidiag, not_and_or] at hs'

Premises used: Finset.mem_piAntidiag, not_and_or
-- 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
hs' : ¬a.support.sum (⇑s : (a : σ) → ℕ) = n ∨ ¬∀ (i : σ), Ne (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) (0 : ℕ) → i ∈ a.support
hs'' : s.support ⊆ a.support
h₁ : ∀ (hs' : ¬a.support.sum (⇑s : (a : σ) → ℕ) = n), False
h₂ : ∀ (hs' : ¬∀ (i : σ), Ne (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) (0 : ℕ) → i ∈ a.support), False
⊢ False

Tactic:
rcases hs' with hs' | hs'
-- 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
hs'' : s.support ⊆ a.support
hs' : ¬a.support.sum (⇑s : (a : σ) → ℕ) = n
h₁ : a.support.sum (⇑s : (a : σ) → ℕ) = n
⊢ False

Tactic:
apply hs'
-- 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
hs'' : s.support ⊆ a.support
hs' : ¬a.support.sum (⇑s : (a : σ) → ℕ) = n
⊢ ∀ i ∈ a.support, Eq (α := ℕ) 0 0

Tactic:
simp
-- 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
hs'' : s.support ⊆ a.support
hs' : ¬a.support.sum (⇑s : (a : σ) → ℕ) = n
h₁ : Eq (α := ℕ) (a.support.sum (⇑s : (a : σ) → ℕ)) (s.sum fun (x : σ) (m : ℕ) ↦ m)
h₂ h₃ : Eq (α := ℕ) (a.support.sum (⇑s : (a : σ) → ℕ)) (∑ x ∈ a.support, (s : (a : σ) → ℕ) x)
⊢ a.support.sum (⇑s : (a : σ) → ℕ) = n

Tactic:
rw [← hs, sum_of_support_subset _ hs'' _ (by simp)]

Premises used: Finsupp.sum_of_support_subset
-- 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
hs'' : s.support ⊆ a.support
hs' : ¬∀ (i : σ), Ne (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) (0 : ℕ) → i ∈ a.support
⊢ False

Tactic:
grind
-- 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 :
  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

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]

Premises used: Finset.sum_pow_eq_sum_piAntidiag, Finset.prod_mul_distrib, Finsupp.sum, MvPolynomial.coeff_C_mul, mul_ite, map_pow, MvPolynomial.coeff_prod_X_pow, Finsupp.linearCombination_apply, map_prod, MulZeroClass.mul_zero, MvPolynomial.C_eq_coe_nat, MvPolynomial.smul_eq_C_mul, mul_one, mul_pow, MvPolynomial.coeff_sum
-- 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
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
⊢ 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:
apply Finset.sum_eq_zero (fun x hx ↦ ?_)

Premises used: Finset.sum_eq_zero