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
inst_2 : DecidableEq σ
inst_3 : DecidableEq R
inst_4 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
⊢ Eq (α := MvPolynomial σ R)
    ((DirectSum.coeAddMonoidHom fun (i : M) ↦ weightedHomogeneousSubmodule R w i :
          (a : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x :
      MvPolynomial σ R)
    (DFinsupp.sum (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x
        fun (x : M) (x_1 : ↥(weightedHomogeneousSubmodule R w x)) ↦ (↑x_1 : MvPolynomial σ R) :
      MvPolynomial σ R)

Tactic:
DirectSum.coeLinearMap_eq_dfinsuppSum R w x

Premises used: MvPolynomial.DirectSum.coeLinearMap_eq_dfinsuppSum, Trunc.lift
-- 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
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
h :
  (Function.support (M := MvPolynomial σ R) fun (m : M) ↦
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)) ⊆
    (↑(DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x) : Set M)
⊢ Eq (α := MvPolynomial σ R)
    ((coeLinearMap fun (i : M) ↦ weightedHomogeneousSubmodule R w i :
          (a : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x :
      MvPolynomial σ R)
    (∑ᶠ (m : M), (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) : MvPolynomial σ R)

Tactic:
rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, finsum_eq_sum_of_support_subset]

Premises used: MvPolynomial.DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, finsum_eq_sum_of_support_subset
-- 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
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
⊢ (Function.support (M := MvPolynomial σ R) fun (m : M) ↦
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)) ⊆
    (↑(DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x) : Set M)

Tactic:
apply DirectSum.support_subset

Premises used: DirectSum.support_subset
-- 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
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
rw :
  Eq (α := MvPolynomial σ R)
    (DFinsupp.sum (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x
      fun (x : M) (x_1 : ↥(weightedHomogeneousSubmodule R w x)) ↦ (↑x_1 : MvPolynomial σ R))
    (∑ᶠ (m : M), (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R))
rw₁ :
  Eq (α := MvPolynomial σ R)
    (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R))
    (∑ᶠ (m : M), (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R))
rw₂ :
  Eq (α := MvPolynomial σ R)
    (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R))
    (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R))
s : Finset M
h :
  (Function.support (M := MvPolynomial σ R) fun (m : M) ↦
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)) ⊆
    (↑(DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x) : Set M)
rw₃ :
  Eq (α := MvPolynomial σ R)
    (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R))
    (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R))
s₁ : Finset M
h₁ h₂ :
  (Function.support (M := MvPolynomial σ R) fun (m : M) ↦
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)) ⊆
    (↑(DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x) : Set M)
⊢ Eq (α := MvPolynomial σ R)
    ((coeLinearMap fun (i : M) ↦ weightedHomogeneousSubmodule R w i :
          (a : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x :
      MvPolynomial σ R)
    (∑ᶠ (m : M), (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) : MvPolynomial σ R)

Tactic:
classical
  rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, finsum_eq_sum_of_support_subset]
  apply DirectSum.support_subset

Premises used: MvPolynomial.DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, finsum_eq_sum_of_support_subset, DirectSum.support_subset
-- 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
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
rw :
  ∑ x_1 ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) x_1) : MvPolynomial σ R) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
⊢ (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((coeLinearMap fun (i : M) ↦ weightedHomogeneousSubmodule R w i :
          (a : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)

Tactic:
rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, map_sum]

Premises used: MvPolynomial.DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, map_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
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ Eq (α := MvPolynomial σ R)
    (∑ x_1 ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
        (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
          (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) x_1) : MvPolynomial σ R) :
      MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) :
      MvPolynomial σ R)

Tactic:
@Finset.sum_eq_single M (MvPolynomial σ R) _ (DFinsupp.support x) _ m _ _

Premises used: Finset.sum_eq_single
-- 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
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
h :
  (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
convert_2 :
  ∀ b ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
    b ≠ m →
      Eq (α := MvPolynomial σ R)
        ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
            (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) b) : MvPolynomial σ R) :
          MvPolynomial σ R)
        (0 : MvPolynomial σ R)
convert_3 :
  m ∉ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x →
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
          (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) :
        MvPolynomial σ R)
      (0 : MvPolynomial σ R)
⊢ ∑ x_1 ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) x_1) : MvPolynomial σ R) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)

Tactic:
convert! @Finset.sum_eq_single M (MvPolynomial σ R) _ (DFinsupp.support x) _ m _ _

Premises used: Finset.sum_eq_single
-- 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
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
h h₁ :
  (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
⊢ (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)

Tactic:
rw [IsWeightedHomogeneous.weightedHomogeneousComponent_same (x m).prop]

Premises used: MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_same, Subtype.prop, 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
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m n : M
convert_2 :
  n ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x →
    n ≠ m →
      Eq (α := MvPolynomial σ R)
        ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
            (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) n) : MvPolynomial σ R) :
          MvPolynomial σ R)
        (0 : MvPolynomial σ R)
⊢ n ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x →
    n ≠ m →
      Eq (α := MvPolynomial σ R)
        ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
            (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) n) : MvPolynomial σ R) :
          MvPolynomial σ R)
        (0 : MvPolynomial σ R)

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
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m n : M
h : n ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x
hmn : n ≠ m
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) n) : MvPolynomial σ R) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
IsWeightedHomogeneous.weightedHomogeneousComponent_ne m (x n).prop hmn.symm

Premises used: MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_ne, Ne.symm, Subtype.prop, 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
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m n : M
h : n ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x
hmn : n ≠ m
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) n) : MvPolynomial σ R) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
exact IsWeightedHomogeneous.weightedHomogeneousComponent_ne m (x n).prop hmn.symm

Premises used: MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_ne, Ne.symm, Subtype.prop, 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
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
convert_3 :
  (x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m = 0 →
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
          (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) :
        MvPolynomial σ R)
      (0 : MvPolynomial σ R)
⊢ m ∉ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x →
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
          (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) :
        MvPolynomial σ R)
      (0 : MvPolynomial σ R)

Tactic:
rw [DFinsupp.notMem_support_iff]

Premises used: DFinsupp.notMem_support_iff
-- 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
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
hm : (x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m = 0
convert_3 :
  Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) (↑0 : MvPolynomial σ R)) 0
convert_3₁ :
  Eq (α := MvPolynomial σ R) ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) 0) 0
convert_3₂ convert_3₃ : Eq (α := MvPolynomial σ R) 0 0
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
rw [hm, Submodule.coe_zero, map_zero]

Premises used: map_zero, Submodule.coe_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
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
a :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
      (coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ) : 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
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
a :
  Eq.{u_1 + 1} (α := R)
    (coeff.{u_1, u_3} (σ := σ) 0 ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (coeff.{u_1, u_3} (σ := σ) 0 ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))
a₁ :
  ∀ (hd : ¬d = 0),
    Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
      (coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))
⊢ Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))

Tactic:
rcases Classical.em (d = 0) with (rfl | hd)

Premises used: Classical.em, OfNat.ofNat, Eq, 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
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
⊢ Eq.{u_1 + 1} (α := R)
    (coeff.{u_1, u_3} (σ := σ) 0 ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (coeff.{u_1, u_3} (σ := σ) 0 ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))

Tactic:
simp only [coeff_weightedHomogeneousComponent, if_pos, map_zero, coeff_zero_C]

Premises used: MvPolynomial.coeff_zero_C, map_zero, if_pos, 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
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
a : ¬Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) (0 : M)
⊢ Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))

Tactic:
rw [coeff_weightedHomogeneousComponent, if_neg, coeff_C, if_neg (Ne.symm hd)]

Premises used: MvPolynomial.coeff_C, Ne.symm, 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
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
a : ∃ (x : σ), ¬Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ) ∧ ¬w x = 0
⊢ ¬Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) (0 : M)

Tactic:
simp only [weight, LinearMap.toAddMonoidHom_coe, Finsupp.linearCombination_apply, Finsupp.sum,
      sum_eq_zero_iff, Finsupp.mem_support_iff, Ne, smul_eq_zero, not_forall, not_or,
      and_self_left, exists_prop]

Premises used: LinearMap.toAddMonoidHom_coe, Finsupp.mem_support_iff, Finsupp.weight, Finsupp.sum, Ne, exists_prop, Finsupp.linearCombination_apply, not_or, and_self_left, Classical.not_forall, Finset.sum_eq_zero_iff, smul_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
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ∃ (x : σ), ¬Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
simp only [DFunLike.ext_iff, Finsupp.coe_zero, Pi.zero_apply, not_forall] at hd

Premises used: Pi.zero_apply, DFunLike.ext_iff, Classical.not_forall, Finsupp.coe_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
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ∃ (x : σ), ¬Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
a :
  ∀ (i : σ) (hi : ¬Eq (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (0 : ℕ)),
    ∃ (x : σ), ¬Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ) ∧ ¬w x = 0
⊢ ∃ (x : σ), ¬Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ) ∧ ¬w x = 0

Tactic:
obtain ⟨i, hi⟩ := 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
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
i : σ
hi : ¬Eq (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ ∃ (x : σ), ¬Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ) ∧ ¬w x = 0

Tactic:
⟨i, hi, hw i⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
i : σ
hi : ¬Eq (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ ∃ (x : σ), ¬Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ) ∧ ¬w x = 0

Tactic:
exact ⟨i, hi, hw i⟩
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
a a₁ a₂ a₃ a₄ :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
      (coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))
a₅ :
  Eq.{u_1 + 1} (α := R)
    (coeff.{u_1, u_3} (σ := σ) 0 ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (coeff.{u_1, u_3} (σ := σ) 0 ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))
a₆ a₇ :
  ∀ (d : σ →₀ ℕ) (hd : ¬d = 0),
    Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
      (coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ) : MvPolynomial σ R)

Tactic:
classical
  ext1 d
  rcases Classical.em (d = 0) with (rfl | hd)
  · simp only [coeff_weightedHomogeneousComponent, if_pos, map_zero, coeff_zero_C]
  · rw [coeff_weightedHomogeneousComponent, if_neg, coeff_C, if_neg (Ne.symm hd)]
    simp only [weight, LinearMap.toAddMonoidHom_coe, Finsupp.linearCombination_apply, Finsupp.sum,
      sum_eq_zero_iff, Finsupp.mem_support_iff, Ne, smul_eq_zero, not_forall, not_or,
      and_self_left, exists_prop]
    simp only [DFunLike.ext_iff, Finsupp.coe_zero, Pi.zero_apply, not_forall] at hd
    obtain ⟨i, hi⟩ := hd
    exact ⟨i, hi, hw i⟩

Premises used: LinearMap.toAddMonoidHom_coe, Finsupp.mem_support_iff, Finsupp.weight, MvPolynomial.coeff_C, Finsupp.sum, MvPolynomial.coeff_zero_C, Pi.zero_apply, map_zero, Ne, DFunLike.ext_iff, exists_prop, Finsupp.linearCombination_apply, if_pos, not_or, and_self_left, MvPolynomial.coeff_weightedHomogeneousComponent, Classical.not_forall, if_neg, Finset.sum_eq_zero_iff, rfl, Finsupp.coe_zero, smul_eq_zero
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
M : Type u_2
σ : Type u_3
inst : AddCommMonoid M
w : σ → M
inst_1 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
⊢ NonTorsionWeight w

Tactic:
fun _ x hnx => (smul_eq_zero_iff_left (hw x)).mp hnx

Premises used: smul_eq_zero_iff_left, MvPolynomial.NonTorsionWeight, Iff.mp
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
M : Type u_2
σ : Type u_3
inst : AddCommMonoid M
inst_1 : PartialOrder M
w : σ → M
inst_2 : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
simp :
  Eq.{u_2 + 1} (α := M) (m.sum fun (i : σ) (c : ℕ) ↦ c • w i) 0 ↔
    ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
⊢ Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) m : M) (0 : M) ↔
    ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
simp only [weight, Finsupp.linearCombination, LinearMap.toAddMonoidHom_coe, coe_lsum,
    LinearMap.coe_smulRight, LinearMap.id_coe, id_eq]

Premises used: LinearMap.toAddMonoidHom_coe, Finsupp.weight, LinearMap.id_coe, Finsupp.coe_lsum, LinearMap.coe_smulRight, Finsupp.linearCombination, id_eq