awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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₁ 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) φ =
    φ
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 φ
a₁ :
  ∀ (d : σ →₀ ℕ),
    (∑
        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 φ
a₂ :
  ∀ (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 φ
⊢ ∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ
have a₃ : ∀ (d : σ →₀ ℕ) (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) φ)
        sorry)
      b →
    b ≠ (weight w : (a : σ →₀ ℕ) → M) d → (if (weight w : (a : σ →₀ ℕ) → M) d = b then coeff d φ else 0) = 0
Tactic: classical
  rw [finsum_eq_sum _ (weightedHomogeneousComponent_finsupp φ)]
  ext1 d
  simp only [coeff_sum, coeff_weightedHomogeneousComponent]
  rw [Finset.sum_eq_single (weight w d)]
  · rw [if_pos rfl]
  · intro m _ hm'
    rw [if_neg hm'.symm]
  · intro hm
    rw [if_pos rfl]
    simp only [Finite.mem_toFinset, mem_support, Ne, Classical.not_not] at hm
    have := coeff_weightedHomogeneousComponent (w := w) (weight w d) φ d
    rw [hm, if_pos rfl, coeff_zero] at this
    exact this.symm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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₁ 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) φ =
    φ
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 φ
a₁ :
  ∀ (d : σ →₀ ℕ),
    (∑
        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 φ
a₂ :
  ∀ (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 φ
a₃ :
  ∀ (d : σ →₀ ℕ) (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
⊢ ∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ
have a₄ : ∀ (d : σ →₀ ℕ),
  ((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) φ)
        sorry →
    (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: classical
  rw [finsum_eq_sum _ (weightedHomogeneousComponent_finsupp φ)]
  ext1 d
  simp only [coeff_sum, coeff_weightedHomogeneousComponent]
  rw [Finset.sum_eq_single (weight w d)]
  · rw [if_pos rfl]
  · intro m _ hm'
    rw [if_neg hm'.symm]
  · intro hm
    rw [if_pos rfl]
    simp only [Finite.mem_toFinset, mem_support, Ne, Classical.not_not] at hm
    have := coeff_weightedHomogeneousComponent (w := w) (weight w d) φ d
    rw [hm, if_pos rfl, coeff_zero] at this
    exact this.symm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ
have rw : φ = φ
Tactic: rw [sum_weightedHomogeneousComponent]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) p = p
have a : ∀ (x : σ →₀ ℕ), coeff x ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) p) = coeff x p
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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 : σ →₀ ℕ
⊢ coeff x ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) p) = coeff x p
have a : (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x p
Tactic: rw [coeff_weightedHomogeneousComponent]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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 : σ →₀ ℕ
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x p
have pos : ∀ (zero_coeff : coeff x p = 0), (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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x p
have neg : ∀ (zero_coeff : ¬coeff x p = 0), (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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x p
have pos : (weight w : (a : σ →₀ ℕ) → M) x = m → coeff x p = coeff x p
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x p
have neg : ¬(weight w : (a : σ →₀ ℕ) → M) x = m → 0 = coeff x p
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ 0 = coeff x p
have neg : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [zero_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x p
have neg : (if m = m then coeff x p else 0) = coeff x p
Tactic: rw [hp zero_coeff, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x p
have neg₁ : coeff x p = coeff x p
Tactic: rw [hp zero_coeff, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) p = p
have a : ∀ (x : σ →₀ ℕ), coeff x ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) p) = coeff x 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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
have a₁ : ∀ (x : σ →₀ ℕ), (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x 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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) p = p
have pos : ∀ (x : σ →₀ ℕ) (zero_coeff : coeff x p = 0), (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x 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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) p = p
have neg : ∀ (x : σ →₀ ℕ) (zero_coeff : ¬coeff x p = 0), (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x 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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have a : ∀ (x : σ →₀ ℕ),
  Eq.{u_1 + 1} (α := R) (coeff x ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) p))
    (coeff x 0)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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 : σ →₀ ℕ
⊢ Eq.{u_1 + 1} (α := R) (coeff x ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) p))
    (coeff x 0)
have a : (if (weight w : (a : σ →₀ ℕ) → M) x = n then coeff x p else 0) = coeff x 0
Tactic: rw [coeff_weightedHomogeneousComponent]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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 : σ →₀ ℕ
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = n then coeff x p else 0) = coeff x 0
have pos : ∀ (zero_coeff : coeff x p = 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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = n then coeff x p else 0) = coeff x 0
have neg : ∀ (zero_coeff : ¬coeff x p = 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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
have neg : Eq.{u_1 + 1} (α := R) 0 (coeff x 0)
Tactic: rw [if_neg]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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)
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = n then coeff x p else 0) = coeff x 0
have neg₁ : ¬(weight w : (a : σ →₀ ℕ) → M) x = n
Tactic: rw [if_neg]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ Eq.{u_1 + 1} (α := R) 0 (coeff x 0)
have neg : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [coeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ ¬(weight w : (a : σ →₀ ℕ) → M) x = n
have neg : ¬m = n
Tactic: rw [hp zero_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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)
⊢ n ≠ m →
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
have a : ∀ (hn : n ≠ m) (x : σ →₀ ℕ),
  Eq.{u_1 + 1} (α := R) (coeff x ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) p))
    (coeff x 0)
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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)
⊢ n ≠ m →
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
have a₁ : ∀ (hn : n ≠ m) (x : σ →₀ ℕ), (if (weight w : (a : σ →₀ ℕ) → M) x = n then coeff x p else 0) = coeff x 0
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ n ≠ m →
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ n ≠ m →
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (hypothesis)
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
⊢ (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) p = if m = n then p else 0
have h₁ : IsWeightedHomogeneous w p n
Tactic: simp only [mem_weightedHomogeneousSubmodule] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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
⊢ (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) p = if m = n then p else 0
have a : ∀ (x : σ →₀ ℕ),
  coeff x ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) p) =
    coeff x (if m = n then p else 0)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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 : σ →₀ ℕ
⊢ coeff x ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) p) =
    coeff x (if m = n then p else 0)
have a : (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)
Tactic: rw [coeff_weightedHomogeneousComponent]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
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 : σ →₀ ℕ
⊢ (if (weight w : (a : σ →₀ ℕ) → M) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)
have 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)
Tactic: by_cases zero_coeff : coeff x p = 0