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
⊢ (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)
have 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)
Tactic: simp_rw [eq_indicator_self_iff]
-- 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
⊢ (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)
have 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)
Tactic: split_ifs with 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
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)
⊢ (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)
have 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)
Tactic: split_ifs with 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
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)
have 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 : ℕ))
Tactic: rw [prod_of_support_subset _ hs' _ (by simp), Finsupp.multinomial_of_support_subset 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
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 : ℕ))
⊢ 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)
have 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 : ℕ))
Tactic: rw [prod_of_support_subset _ hs' _ (by simp), Finsupp.multinomial_of_support_subset hs']
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (hypothesis)
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
⊢ 0 =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
have hs'₁ : ¬∀ ⦃x : σ⦄, x ∈ s.support → x ∈ a.support
Tactic: rw [Finset.subset_iff] at hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (hypothesis)
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
⊢ 0 =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
have hs'₁ : ∃ (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'
Cleared hypotheses: 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
hs' :
  ∃ (x : σ) (_ : ¬Eq (α := ℕ) ((s : (a : σ) → ℕ) x : ℕ) (0 : ℕ)),
    Eq.{u_1 + 1} (α := R) ((a : (a : σ) → R) x : R) (0 : R)
⊢ 0 =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
have 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)
Tactic: obtain ⟨i, hsi, hai⟩ := hs'
Cleared hypotheses: 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
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)
have 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)
Tactic: rw [← mul_prod_erase _ i _ (by simpa), hai, zero_pow hsi, zero_mul, 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
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)
⊢ 0 =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
have 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)
Tactic: rw [← mul_prod_erase _ i _ (by simpa), hai, zero_pow hsi, zero_mul, 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
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)
⊢ 0 =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
have 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)
Tactic: rw [← mul_prod_erase _ i _ (by simpa), hai, zero_pow hsi, zero_mul, 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
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)
⊢ 0 =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
have neg₃ : 0 = HMul.hMul (α := R) (↑s.multinomial : R) 0
Tactic: rw [← mul_prod_erase _ i _ (by simpa), hai, zero_pow hsi, zero_mul, 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
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
⊢ 0 =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
have neg₄ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← mul_prod_erase _ i _ (by simpa), hai, zero_pow hsi, zero_mul, 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
⊢ ∀ 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
have 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
Tactic: simp only [Finset.mem_piAntidiag, ne_eq, Finsupp.mem_support_iff, ite_eq_right_iff, and_imp]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (hypothesis)
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
⊢ HMul.hMul (α := R) (↑(Nat.multinomial a.support b) : R)
      (∏ x ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x : R) (b x)) =
    0
have 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
Tactic: simp [Finsupp.ext_iff] at hed
Cleared hypotheses: hed
-- 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
⊢ (⇑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
have 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
Tactic: simp_rw [ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (hypothesis)
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
⊢ 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
have hs''₁ : s.support ⊆ a.support
Tactic: rw [eq_indicator_self_iff] at hs''
Cleared hypotheses: 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
hs' : (⇑s : (a : σ) → ℕ) ∉ a.support.piAntidiag n
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 : ℕ)) =
    0
have h₁ : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (hypothesis)
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
⊢ False
have hs'₁ : ¬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'
Cleared hypotheses: hs', 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
hs' : ¬a.support.sum (⇑s : (a : σ) → ℕ) = n ∨ ¬∀ (i : σ), Ne (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) (0 : ℕ) → i ∈ a.support
hs'' : s.support ⊆ a.support
⊢ False
have h₁ : ∀ (hs' : ¬a.support.sum (⇑s : (a : σ) → ℕ) = n), False
Tactic: rcases hs' with hs' | hs'
Cleared hypotheses: 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
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
⊢ False
have h₂ : ∀ (hs' : ¬∀ (i : σ), Ne (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) (0 : ℕ) → i ∈ a.support), False
Tactic: rcases hs' with hs' | hs'
Cleared hypotheses: 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
hs'' : s.support ⊆ a.support
hs' : ¬a.support.sum (⇑s : (a : σ) → ℕ) = n
⊢ False
have h₁ : a.support.sum (⇑s : (a : σ) → ℕ) = n
Tactic: apply 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
hs'' : s.support ⊆ a.support
hs' : ¬a.support.sum (⇑s : (a : σ) → ℕ) = n
⊢ a.support.sum (⇑s : (a : σ) → ℕ) = n
have h₁ : Eq (α := ℕ) (a.support.sum (⇑s : (a : σ) → ℕ)) (s.sum fun (x : σ) (m : ℕ) ↦ m)
Tactic: rw [← hs, sum_of_support_subset _ hs'' _ (by simp)]
-- 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
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)
⊢ a.support.sum (⇑s : (a : σ) → ℕ) = n
have h₂ : Eq (α := ℕ) (a.support.sum (⇑s : (a : σ) → ℕ)) (∑ x ∈ a.support, (s : (a : σ) → ℕ) x)
Tactic: rw [← hs, sum_of_support_subset _ hs'' _ (by simp)]
-- 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) =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
have 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)
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)
⊢ 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 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)
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