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
φ : MvPolynomial σ R
d : σ →₀ ℕ
hm :
  ((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) φ)
      ⋯
a : coeff d φ = 0
⊢ (if Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) ((weight w : (a : σ →₀ ℕ) → M) d : M) then coeff d φ
    else 0) =
    0

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 : σ →₀ ℕ
hm :
  ((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) φ)
      ⋯
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w ((weight w : (a : σ →₀ ℕ) → M) d) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
simp only [Finite.mem_toFinset, mem_support, Ne, Classical.not_not] at hm

Premises used: Classical.not_not, Set.Finite.mem_toFinset, Ne, Function.mem_support
-- 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 : σ →₀ ℕ
hm :
  Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w ((weight w : (a : σ →₀ ℕ) → M) d) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)
⊢ coeff d
      ((weightedHomogeneousComponent w ((weight w : (a : σ →₀ ℕ) → M) d) : (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

Tactic:
have := coeff_weightedHomogeneousComponent (w := w) (weight w d) φ 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 : σ →₀ ℕ
hm :
  Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w ((weight w : (a : σ →₀ ℕ) → M) d) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)
this :
  coeff d
      ((weightedHomogeneousComponent w ((weight w : (a : σ →₀ ℕ) → M) d) : (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 = coeff d φ

Tactic:
rw [hm, if_pos rfl, coeff_zero] at this

Premises used: if_pos, MvPolynomial.coeff_zero, 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 : σ →₀ ℕ
hm :
  Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w ((weight w : (a : σ →₀ ℕ) → M) d) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)
this : 0 = coeff d φ
⊢ coeff d φ = 0

Tactic:
this.symm

Premises used: Eq.symm
-- 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 : σ →₀ ℕ
hm :
  Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w ((weight w : (a : σ →₀ ℕ) → M) d) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)
this : 0 = coeff d φ
⊢ coeff d φ = 0

Tactic:
exact this.symm

Premises used: Eq.symm
-- 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 rw₁ : φ = φ
⊢ ∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ

Tactic:
rw [sum_weightedHomogeneousComponent]

Premises used: MvPolynomial.sum_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
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
a :
  ∀ (x : σ →₀ ℕ), coeff x ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) p) = coeff x p
⊢ (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) p = p

Tactic:
ext x
-- 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
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
a : (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x p
⊢ coeff x ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) p) = coeff x p

Tactic:
rw [coeff_weightedHomogeneousComponent]

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
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
pos : ∀ (zero_coeff : coeff x p = 0), (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x p
neg : ∀ (zero_coeff : ¬coeff x p = 0), (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x p
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x p

Tactic:
by_cases zero_coeff : coeff x p = 0

Premises used: MvPolynomial.coeff
-- 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
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
pos : (weight w : (a : σ →₀ ℕ) → M) x = m → coeff x p = coeff x p
neg : ¬(weight w : (a : σ →₀ ℕ) → M) x = m → 0 = coeff x p
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x p

Tactic:
split_ifs
-- 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
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h : (weight w : (a : σ →₀ ℕ) → M) x = m
⊢ coeff x p = coeff x p

Tactic:
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
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h : ¬(weight w : (a : σ →₀ ℕ) → M) x = m
neg neg₁ : Eq.{u_1 + 1} (α := R) 0 0
⊢ 0 = coeff x p

Tactic:
rw [zero_coeff]
-- 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
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
neg : (if m = m then coeff x p else 0) = coeff x p
neg₁ neg₂ : coeff x p = coeff x p
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x p

Tactic:
rw [hp zero_coeff, 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
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
a :
  ∀ (x : σ →₀ ℕ), coeff x ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) p) = coeff x p
a₁ : ∀ (x : σ →₀ ℕ), (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x p
pos :
  ∀ (x : σ →₀ ℕ) (zero_coeff : coeff x p = 0),
    (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x p
neg neg₁ :
  ∀ (x : σ →₀ ℕ) (zero_coeff : ¬coeff x p = 0),
    (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x p
⊢ (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) p = p

Tactic:
classical
  ext x
  rw [coeff_weightedHomogeneousComponent]
  by_cases zero_coeff : coeff x p = 0
  · split_ifs
    · rfl
    rw [zero_coeff]
  · rw [hp zero_coeff, if_pos rfl]

Premises used: if_pos, MvPolynomial.coeff_weightedHomogeneousComponent, 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
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
a :
  ∀ (x : σ →₀ ℕ),
    Eq.{u_1 + 1} (α := R) (coeff x ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) p))
      (coeff x 0)
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
ext x
-- 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
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
a : (if (weight w : (a : σ →₀ ℕ) → M) x = n then coeff x p else 0) = coeff x 0
⊢ Eq.{u_1 + 1} (α := R) (coeff x ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) p))
    (coeff x 0)

Tactic:
rw [coeff_weightedHomogeneousComponent]

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
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
pos : ∀ (zero_coeff : coeff x p = 0), (if (weight w : (a : σ →₀ ℕ) → M) x = n then coeff x p else 0) = coeff x 0
neg : ∀ (zero_coeff : ¬coeff x p = 0), (if (weight w : (a : σ →₀ ℕ) → M) x = n then coeff x p else 0) = coeff x 0
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = n then coeff x p else 0) = coeff x 0

Tactic:
by_cases zero_coeff : coeff x p = 0

Premises used: MvPolynomial.coeff
-- 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
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = n then coeff x p else 0) = coeff x 0

Tactic:
simp [zero_coeff]
-- 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
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
neg : Eq.{u_1 + 1} (α := R) 0 (coeff x 0)
neg₁ : ¬(weight w : (a : σ →₀ ℕ) → M) x = n
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = n then coeff x p else 0) = coeff x 0

Tactic:
rw [if_neg]

Premises used: 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
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
neg neg₁ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := R) 0 (coeff x 0)

Tactic:
rw [coeff_zero]

Premises used: MvPolynomial.coeff_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
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
neg : ¬m = n
⊢ ¬(weight w : (a : σ →₀ ℕ) → M) x = n

Tactic:
rw [hp zero_coeff]
-- 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
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ ¬m = n

Tactic:
Ne.symm hn

Premises used: Ne.symm
-- 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
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ ¬m = n

Tactic:
exact Ne.symm hn

Premises used: Ne.symm
-- 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
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
intro :
  ∀ (hn : n ≠ m),
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
a :
  ∀ (hn : n ≠ m) (x : σ →₀ ℕ),
    Eq.{u_1 + 1} (α := R) (coeff x ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) p))
      (coeff x 0)
a₁ : ∀ (hn : n ≠ m) (x : σ →₀ ℕ), (if (weight w : (a : σ →₀ ℕ) → M) x = n then coeff x p else 0) = coeff x 0
pos :
  ∀ (hn : n ≠ m) (x : σ →₀ ℕ) (zero_coeff : coeff x p = 0),
    (if (weight w : (a : σ →₀ ℕ) → M) x = n then coeff x p else 0) = coeff x 0
neg neg₁ :
  ∀ (hn : n ≠ m) (x : σ →₀ ℕ) (zero_coeff : ¬coeff x p = 0),
    (if (weight w : (a : σ →₀ ℕ) → M) x = n then coeff x p else 0) = coeff x 0
⊢ n ≠ m →
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
      (0 : MvPolynomial σ R)

Tactic:
classical
  intro hn
  ext x
  rw [coeff_weightedHomogeneousComponent]
  by_cases zero_coeff : coeff x p = 0
  · simp [zero_coeff]
  · rw [if_neg]
    · rw [coeff_zero]
    · rw [hp zero_coeff]; exact Ne.symm hn

Premises used: MvPolynomial.coeff_zero, 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
inst_2 : DecidableEq M
m n : M
p : MvPolynomial σ R
h : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) p
⊢ IsWeightedHomogeneous w p n

Tactic:
simp only [mem_weightedHomogeneousSubmodule] at h

Premises used: MvPolynomial.mem_weightedHomogeneousSubmodule
-- 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
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
a :
  ∀ (x : σ →₀ ℕ),
    coeff x ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) p) =
      coeff x (if m = n then p else 0)
⊢ (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) p = if m = n then p else 0

Tactic:
ext x
-- 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
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
a : (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)
⊢ coeff x ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) p) =
    coeff x (if m = n then p else 0)

Tactic:
rw [coeff_weightedHomogeneousComponent]

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
inst_2 : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
pos :
  ∀ (zero_coeff : coeff x p = 0),
    (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)
neg :
  ∀ (zero_coeff : ¬coeff x p = 0),
    (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)

Tactic:
by_cases zero_coeff : coeff x p = 0

Premises used: MvPolynomial.coeff
-- 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
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
pos : (weight w : (a : σ →₀ ℕ) → M) x = m → m = n → coeff x p = coeff x p
neg : (weight w : (a : σ →₀ ℕ) → M) x = m → ¬m = n → coeff x p = coeff x 0
pos₁ : ¬(weight w : (a : σ →₀ ℕ) → M) x = m → m = n → 0 = coeff x p
neg₁ : ¬(weight w : (a : σ →₀ ℕ) → M) x = m → ¬m = n → Eq.{u_1 + 1} (α := R) 0 (coeff x 0)
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)

Tactic:
split_ifs
-- 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
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h_1 : (weight w : (a : σ →₀ ℕ) → M) x = m
h_2 : m = n
⊢ coeff x p = coeff x p

Tactic:
simp only [zero_coeff, coeff_zero]

Premises used: MvPolynomial.coeff_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
inst_2 : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h_1 : (weight w : (a : σ →₀ ℕ) → M) x = m
h_2 : ¬m = n
⊢ coeff x p = coeff x 0

Tactic:
simp only [zero_coeff, coeff_zero]

Premises used: MvPolynomial.coeff_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
inst_2 : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h_1 : ¬(weight w : (a : σ →₀ ℕ) → M) x = m
h_2 : m = n
⊢ 0 = coeff x p

Tactic:
simp only [zero_coeff, coeff_zero]

Premises used: MvPolynomial.coeff_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
inst_2 : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h_1 : ¬(weight w : (a : σ →₀ ℕ) → M) x = m
h_2 : ¬m = n
⊢ Eq.{u_1 + 1} (α := R) 0 (coeff x 0)

Tactic:
simp only [zero_coeff, coeff_zero]

Premises used: MvPolynomial.coeff_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
inst_2 : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
neg : (if n = m then coeff x p else 0) = coeff x (if m = n then p else 0)
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)

Tactic:
rw [h zero_coeff]
-- 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
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
neg : (if m = n then coeff x p else 0) = coeff x (if m = n then p else 0)
⊢ (if n = m then coeff x p else 0) = coeff x (if m = n then p else 0)

Tactic:
simp only [show n = m ↔ m = n from eq_comm]

Premises used: eq_comm
-- 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
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
pos : ∀ (h1 : m = n), coeff x p = coeff x p
neg : ∀ (h1 : ¬m = n), Eq.{u_1 + 1} (α := R) 0 (coeff x 0)
⊢ (if m = n then coeff x p else 0) = coeff x (if m = n then p else 0)

Tactic:
split_ifs with h1
-- 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
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
h1 : m = n
⊢ coeff x p = coeff x p

Tactic:
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
inst_2 : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
h1 : ¬m = n
⊢ Eq.{u_1 + 1} (α := R) 0 (coeff x 0)

Tactic:
simp only [coeff_zero]

Premises used: MvPolynomial.coeff_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
inst_2 : DecidableEq M
n : M
p : MvPolynomial σ R
h :
  ∀ (c : σ →₀ ℕ),
    Membership.mem (γ := Finset (σ →₀ ℕ))
        (support.{u_1, u_3} (R := R) ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) p))
        c ↔
      c ∈ {c ∈ p.support | (weight w : (a : σ →₀ ℕ) → M) c = n}
⊢ support.{u_1, u_3} (R := R) ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) p) =
    {c ∈ p.support | (weight w : (a : σ →₀ ℕ) → M) c = n}

Tactic:
ext c
-- 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
n : M
p : MvPolynomial σ R
c : σ →₀ ℕ
⊢ Membership.mem (γ := Finset (σ →₀ ℕ))
      (support.{u_1, u_3} (R := R) ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) p))
      c ↔
    c ∈ {c ∈ p.support | (weight w : (a : σ →₀ ℕ) → M) c = n}

Tactic:
simp [coeff_weightedHomogeneousComponent, And.comm]

Premises used: And.comm, 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
inst_2 : DecidableEq σ
inst_3 : DecidableEq R
inst_4 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
rw rw₁ :
  Eq (α := MvPolynomial σ R)
    (DFinsupp.sum (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x
      fun (i : M) (x : ↥(weightedHomogeneousSubmodule R w i)) ↦ (↑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))
⊢ Eq (α := MvPolynomial σ R)
    ((coeLinearMap 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:
rw [_root_.DirectSum.coeLinearMap_eq_dfinsuppSum]

Premises used: DirectSum.coeLinearMap_eq_dfinsuppSum