awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst_2 : DecidableEq M
d : σ →₀ ℕ
this : DecidableEq M := Classical.decEq M
⊢ (if (weight w : (a : σ →₀ ℕ) → M) d = n then (φ : (a : σ →₀ ℕ) → R) d else 0) =
    if (weight w : (a : σ →₀ ℕ) → M) d = n then coeff d φ else 0

Tactic:
convert! rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst_2 : DecidableEq M
this : DecidableEq M := Classical.decEq M
⊢ Eq (α := Finsupp.{u_3, u_1} (σ →₀ ℕ) R)
    (∑ i ∈ φ.support with (weight w : (a : σ →₀ ℕ) → M) i = n, Finsupp.single i ((φ : (a : σ →₀ ℕ) → R) i))
    (∑ i ∈ φ.support with (weight w : (a : σ →₀ ℕ) → M) i = n, Finsupp.single i ((φ : (a : σ →₀ ℕ) → R) i))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst_2 : DecidableEq M
this : DecidableEq M := Classical.decEq M
⊢ Eq (α := Finsupp.{u_3, u_1} (σ →₀ ℕ) R)
    (∑ i ∈ φ.support with (weight w : (a : σ →₀ ℕ) → M) i = n, Finsupp.single i ((φ : (a : σ →₀ ℕ) → R) i))
    (∑ d ∈ φ.support with (weight w : (a : σ →₀ ℕ) → M) d = n, (monomial d : (a : R) → MvPolynomial σ R) (coeff d φ))

Tactic:
convert! rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hd :
  Ne.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
contrapose! :
  ∀ (hd : (weight w : (a : σ →₀ ℕ) → M) d ≠ n),
    Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
⊢ (weight w : (a : σ →₀ ℕ) → M) d = n

Tactic:
contrapose! hd
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → M) d ≠ n
rw : (if (weight w : (a : σ →₀ ℕ) → M) d = n then coeff d φ else 0) = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0

Tactic:
rw [coeff_weightedHomogeneousComponent, if_neg hd]

Premises used: MvPolynomial.coeff_weightedHomogeneousComponent, if_neg
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
intro intro₁ :
  ∀ ⦃d : σ →₀ ℕ⦄
    (hd :
      Ne.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
        0),
    (weight w : (a : σ →₀ ℕ) → M) d = n
intro₂ :
  ∀ ⦃d : σ →₀ ℕ⦄ (hd : (weight w : (a : σ →₀ ℕ) → M) d ≠ n),
    Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) n

Tactic:
classical
  intro d hd
  contrapose! hd
  rw [coeff_weightedHomogeneousComponent, if_neg hd]

Premises used: MvPolynomial.coeff_weightedHomogeneousComponent
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
m : M
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) m

Tactic:
weightedHomogeneousComponent_isWeightedHomogeneous m φ

Premises used: MvPolynomial.weightedHomogeneousComponent_isWeightedHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
m : M
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) m

Tactic:
exact weightedHomogeneousComponent_isWeightedHomogeneous m φ

Premises used: MvPolynomial.weightedHomogeneousComponent_isWeightedHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
n : M
r : R
⊢ (weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) φ) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)

Tactic:
simp only [C_mul', map_smul]

Premises used: MvPolynomial.C_mul', map_smul
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ n
rw :
  ∀ x ∈ {d ∈ φ.support | (weight w : (a : σ →₀ ℕ) → M) d = n},
    Eq (α := MvPolynomial σ R) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x φ) : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
rw [weightedHomogeneousComponent_apply, sum_eq_zero]

Premises used: Finset.sum_eq_zero, MvPolynomial.weightedHomogeneousComponent_apply
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ n
d : σ →₀ ℕ
hd : d ∈ {d ∈ φ.support | (weight w : (a : σ →₀ ℕ) → M) d = n}
⊢ d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n

Tactic:
rw [mem_filter] at hd

Premises used: Finset.mem_filter
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n
exfalso : False
⊢ Eq (α := MvPolynomial σ R) ((monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) : MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
exfalso
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n
⊢ False

Tactic:
h _ hd.1 hd.2

Premises used: And.right, And.left
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n
⊢ False

Tactic:
exact h _ hd.1 hd.2

Premises used: And.right, And.left
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ n
rw :
  Eq (α := MvPolynomial σ R)
    (∑ d ∈ φ.support with (weight w : (a : σ →₀ ℕ) → M) d = n, (monomial d : (a : R) → MvPolynomial σ R) (coeff d φ)) 0
rw₁ : Eq (α := MvPolynomial σ R) 0 0
rw₂ :
  ∀ x ∈ {d ∈ φ.support | (weight w : (a : σ →₀ ℕ) → M) d = n},
    Eq (α := MvPolynomial σ R) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x φ) : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
rw₃ : Eq (α := MvPolynomial σ R) 0 0
rw₄ rw₅ rw₆ rw₇ :
  ∀ (d : σ →₀ ℕ) (hd : d ∈ {d ∈ φ.support | (weight w : (a : σ →₀ ℕ) → M) d = n}),
    Eq (α := MvPolynomial σ R) ((monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
rw₈ :
  ∀ (d : σ →₀ ℕ) (hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n),
    Eq (α := MvPolynomial σ R) ((monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
rw₉ rw₁₀ : ∀ (d : σ →₀ ℕ) (hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n), False
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
classical
  rw [weightedHomogeneousComponent_apply, sum_eq_zero]
  intro d hd; rw [mem_filter] at hd
  exfalso; exact h _ hd.1 hd.2

Premises used: Finset.sum_eq_zero, Finset.mem_filter, MvPolynomial.weightedHomogeneousComponent_apply
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
h : weightedTotalDegree w φ < n
rw :
  ∀ x ∈ {d ∈ φ.support | (weight w : (a : σ →₀ ℕ) → M) d = n},
    Eq (α := MvPolynomial σ R) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x φ) : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
rw [weightedHomogeneousComponent_apply, sum_eq_zero]

Premises used: Finset.sum_eq_zero, MvPolynomial.weightedHomogeneousComponent_apply
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ {d ∈ φ.support | (weight w : (a : σ →₀ ℕ) → M) d = n}
⊢ d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n

Tactic:
rw [Finset.mem_filter] at hd

Premises used: Finset.mem_filter
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n
exfalso : False
⊢ Eq (α := MvPolynomial σ R) ((monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) : MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
exfalso
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n
apply : n < n
⊢ False

Tactic:
apply lt_irrefl n

Premises used: lt_irrefl
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n
nth_rw : (weight w : (a : σ →₀ ℕ) → M) d < n
⊢ n < n

Tactic:
nth_rw 1 [← hd.2]

Premises used: And.right
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n
⊢ (weight w : (a : σ →₀ ℕ) → M) d < n

Tactic:
lt_of_le_of_lt (le_weightedTotalDegree w hd.1) h

Premises used: lt_of_le_of_lt, MvPolynomial.le_weightedTotalDegree, And.left
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n
⊢ (weight w : (a : σ →₀ ℕ) → M) d < n

Tactic:
exact lt_of_le_of_lt (le_weightedTotalDegree w hd.1) h

Premises used: lt_of_le_of_lt, MvPolynomial.le_weightedTotalDegree, And.left
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
h : weightedTotalDegree w φ < n
rw :
  Eq (α := MvPolynomial σ R)
    (∑ d ∈ φ.support with (weight w : (a : σ →₀ ℕ) → M) d = n, (monomial d : (a : R) → MvPolynomial σ R) (coeff d φ)) 0
rw₁ : Eq (α := MvPolynomial σ R) 0 0
rw₂ :
  ∀ x ∈ {d ∈ φ.support | (weight w : (a : σ →₀ ℕ) → M) d = n},
    Eq (α := MvPolynomial σ R) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x φ) : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
rw₃ : Eq (α := MvPolynomial σ R) 0 0
rw₄ rw₅ rw₆ :
  ∀ (d : σ →₀ ℕ) (hd : d ∈ {d ∈ φ.support | (weight w : (a : σ →₀ ℕ) → M) d = n}),
    Eq (α := MvPolynomial σ R) ((monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
rw₇ :
  ∀ (d : σ →₀ ℕ) (hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n),
    Eq (α := MvPolynomial σ R) ((monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
rw₈ : ∀ (d : σ →₀ ℕ) (hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n), False
rw₉ : ∀ (d : σ →₀ ℕ) (hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n), n < n
rw₁₀ : ∀ (d : σ →₀ ℕ) (hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n), (weight w : (a : σ →₀ ℕ) → M) d < n
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
classical
  rw [weightedHomogeneousComponent_apply, sum_eq_zero]
  intro d hd
  rw [Finset.mem_filter] at hd
  exfalso
  apply lt_irrefl n
  nth_rw 1 [← hd.2]
  exact lt_of_le_of_lt (le_weightedTotalDegree w hd.1) h

Premises used: lt_irrefl, Finset.sum_eq_zero, Finset.mem_filter, MvPolynomial.weightedHomogeneousComponent_apply
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
apply :
  Subset.{u_2} (α := Set M)
    (Function.support (M := MvPolynomial σ R) fun (m : M) ↦
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
    ((fun (d : σ →₀ ℕ) ↦ (weight w : (a : σ →₀ ℕ) → M) d) '' (↑φ.support : Set (σ →₀ ℕ)))
⊢ HasFiniteSupport (M := MvPolynomial σ R) fun (m : M) ↦
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ

Tactic:
apply ((fun d : σ →₀ ℕ => (weight w) d) '' (φ.support : Set (σ →₀ ℕ))).toFinite.subset

Premises used: Finsupp.weight, Set.Finite.subset, MvPolynomial.support, Set.toFinite, SetLike.coe, Set.image, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
m : M
hm :
  Membership.mem (γ := Set M)
    (Function.support (M := MvPolynomial σ R) fun (m : M) ↦
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
    m
by_contra : ∀ (hm' : m ∉ (fun (d : σ →₀ ℕ) ↦ (weight w : (a : σ →₀ ℕ) → M) d) '' (↑φ.support : Set (σ →₀ ℕ))), False
⊢ Membership.mem (γ := Set M) ((fun (d : σ →₀ ℕ) ↦ (weight w : (a : σ →₀ ℕ) → M) d) '' (↑φ.support : Set (σ →₀ ℕ))) m

Tactic:
by_contra hm'
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
m : M
hm :
  Membership.mem (γ := Set M)
    (Function.support (M := MvPolynomial σ R) fun (m : M) ↦
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
    m
hm' : m ∉ (fun (d : σ →₀ ℕ) ↦ (weight w : (a : σ →₀ ℕ) → M) d) '' (↑φ.support : Set (σ →₀ ℕ))
apply : ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ m
⊢ False

Tactic:
apply hm (weightedHomogeneousComponent_eq_zero' m φ _)

Premises used: MvPolynomial.weightedHomogeneousComponent_eq_zero'
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
m : M
hm :
  Membership.mem (γ := Set M)
    (Function.support (M := MvPolynomial σ R) fun (m : M) ↦
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
    m
hm' : m ∉ (fun (d : σ →₀ ℕ) ↦ (weight w : (a : σ →₀ ℕ) → M) d) '' (↑φ.support : Set (σ →₀ ℕ))
⊢ ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ m

Tactic:
simpa only [Set.mem_image, not_exists, not_and] using hm'

Premises used: Set.mem_image, not_exists, not_and
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
rw :
  ∑
      i ∈
        Finite.toFinset (s :=
          Function.support (M := MvPolynomial σ R) fun (m : M) ↦
            (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
          ⋯,
      (weightedHomogeneousComponent w i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ =
    φ
⊢ ∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ

Tactic:
rw [finsum_eq_sum _ (weightedHomogeneousComponent_finsupp φ)]

Premises used: finsum_eq_sum, MvPolynomial.weightedHomogeneousComponent_finsupp
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
a :
  ∀ (d : σ →₀ ℕ),
    coeff d
        (∑
          i ∈
            Finite.toFinset (s :=
              Function.support (M := MvPolynomial σ R) fun (m : M) ↦
                (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
              ⋯,
          (weightedHomogeneousComponent w i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) =
      coeff d φ
⊢ ∑
      i ∈
        Finite.toFinset (s :=
          Function.support (M := MvPolynomial σ R) fun (m : M) ↦
            (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
          ⋯,
      (weightedHomogeneousComponent w i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ =
    φ

Tactic:
ext1 d
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
a :
  (∑
      x ∈
        Finite.toFinset (s :=
          Function.support (M := MvPolynomial σ R) fun (m : M) ↦
            (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
          ⋯,
      if (weight w : (a : σ →₀ ℕ) → M) d = x then coeff d φ else 0) =
    coeff d φ
⊢ coeff d
      (∑
        i ∈
          Finite.toFinset (s :=
            Function.support (M := MvPolynomial σ R) fun (m : M) ↦
              (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
            ⋯,
        (weightedHomogeneousComponent w i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) =
    coeff d φ

Tactic:
simp only [coeff_sum, coeff_weightedHomogeneousComponent]

Premises used: MvPolynomial.coeff_weightedHomogeneousComponent, MvPolynomial.coeff_sum
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
a :
  (if Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) ((weight w : (a : σ →₀ ℕ) → M) d : M) then coeff d φ
    else 0) =
    coeff d φ
a₁ :
  ∀ (b : M),
    Membership.mem (γ := Finset M)
        (Finite.toFinset (s :=
          Function.support (M := MvPolynomial σ R) fun (m : M) ↦
            (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
          ⋯)
        b →
      b ≠ (weight w : (a : σ →₀ ℕ) → M) d → (if (weight w : (a : σ →₀ ℕ) → M) d = b then coeff d φ else 0) = 0
a₂ :
  ((weight w : (a : σ →₀ ℕ) → M) d : M) ∉
      Finite.toFinset (s :=
        Function.support (M := MvPolynomial σ R) fun (m : M) ↦
          (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
        ⋯ →
    (if Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) ((weight w : (a : σ →₀ ℕ) → M) d : M) then coeff d φ
      else 0) =
      0
⊢ (∑
      x ∈
        Finite.toFinset (s :=
          Function.support (M := MvPolynomial σ R) fun (m : M) ↦
            (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
          ⋯,
      if (weight w : (a : σ →₀ ℕ) → M) d = x then coeff d φ else 0) =
    coeff d φ

Tactic:
rw [Finset.sum_eq_single (weight w d)]

Premises used: Finsupp.weight, Finset.sum_eq_single, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
a a₁ : coeff d φ = coeff d φ
⊢ (if Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) ((weight w : (a : σ →₀ ℕ) → M) d : M) then coeff d φ
    else 0) =
    coeff d φ

Tactic:
rw [if_pos rfl]

Premises used: if_pos, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
m : M
a :
  Membership.mem (γ := Finset M)
      (Finite.toFinset (s :=
        Function.support (M := MvPolynomial σ R) fun (m : M) ↦
          (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
        ⋯)
      m →
    m ≠ (weight w : (a : σ →₀ ℕ) → M) d → (if (weight w : (a : σ →₀ ℕ) → M) d = m then coeff d φ else 0) = 0
⊢ Membership.mem (γ := Finset M)
      (Finite.toFinset (s :=
        Function.support (M := MvPolynomial σ R) fun (m : M) ↦
          (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
        ⋯)
      m →
    m ≠ (weight w : (a : σ →₀ ℕ) → M) d → (if (weight w : (a : σ →₀ ℕ) → M) d = m then coeff d φ else 0) = 0

Tactic:
_
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
m : M
h :
  Membership.mem (γ := Finset M)
    (Finite.toFinset (s :=
      Function.support (M := MvPolynomial σ R) fun (m : M) ↦
        (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
      ⋯)
    m
hm' : m ≠ (weight w : (a : σ →₀ ℕ) → M) d
a a₁ : Eq.{u_1 + 1} (α := R) 0 0
⊢ (if (weight w : (a : σ →₀ ℕ) → M) d = m then coeff d φ else 0) = 0

Tactic:
rw [if_neg hm'.symm]

Premises used: Ne.symm, if_neg