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
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)
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have rw₈ : ∀ (d : σ →₀ ℕ) (hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n), False
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
-- 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
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
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have rw₉ : ∀ (d : σ →₀ ℕ) (hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n), n < n
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
-- 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
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
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have rw₁₀ : ∀ (d : σ →₀ ℕ) (hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n), (weight w : (a : σ →₀ ℕ) → M) d < n
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
-- 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
⊢ HasFiniteSupport (M := MvPolynomial σ R) fun (m : M) ↦
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ
have 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 (σ →₀ ℕ)))
Tactic: apply ((fun d : σ →₀ ℕ => (weight w) d) '' (φ.support : Set (σ →₀ ℕ))).toFinite.subset
-- 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
hm :
  Membership.mem (γ := Set M)
    (Function.support (M := MvPolynomial σ R) fun (m : M) ↦
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
    m
⊢ Membership.mem (γ := Set M) ((fun (d : σ →₀ ℕ) ↦ (weight w : (a : σ →₀ ℕ) → M) d) '' (↑φ.support : Set (σ →₀ ℕ))) m
have by_contra : ∀ (hm' : m ∉ (fun (d : σ →₀ ℕ) ↦ (weight w : (a : σ →₀ ℕ) → M) d) '' (↑φ.support : Set (σ →₀ ℕ))), False
Tactic: by_contra hm'
-- 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
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 (σ →₀ ℕ))
⊢ False
have apply : ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ m
Tactic: apply hm (weightedHomogeneousComponent_eq_zero' m φ _)
-- 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 : ∑
    i ∈
      Finite.toFinset (s :=
        Function.support (M := MvPolynomial σ R) fun (m : M) ↦
          (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
        sorry,
    (weightedHomogeneousComponent w i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ =
  φ
Tactic: rw [finsum_eq_sum _ (weightedHomogeneousComponent_finsupp φ)]
-- 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
⊢ ∑
      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) φ =
    φ
have a : ∀ (d : σ →₀ ℕ),
  coeff d
      (∑
        i ∈
          Finite.toFinset (s :=
            Function.support (M := MvPolynomial σ R) fun (m : M) ↦
              (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
            sorry,
        (weightedHomogeneousComponent w i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) =
    coeff d φ
Tactic: ext1 d
-- 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
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 φ
have a : (∑
    x ∈
      Finite.toFinset (s :=
        Function.support (M := MvPolynomial σ R) fun (m : M) ↦
          (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
        sorry,
    if (weight w : (a : σ →₀ ℕ) → M) d = x then coeff d φ else 0) =
  coeff d φ
Tactic: simp only [coeff_sum, 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
φ : MvPolynomial σ R
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 φ
have 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 φ
Tactic: rw [Finset.sum_eq_single (weight w d)]
-- 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
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 φ
⊢ (∑
      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 φ
have 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) φ)
        sorry)
      b →
    b ≠ (weight w : (a : σ →₀ ℕ) → M) d → (if (weight w : (a : σ →₀ ℕ) → M) d = b then coeff d φ else 0) = 0
Tactic: rw [Finset.sum_eq_single (weight w d)]
-- 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
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
⊢ (∑
      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 φ
have 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) φ)
      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: rw [Finset.sum_eq_single (weight w d)]
-- 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
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 φ
have a : coeff d φ = coeff d φ
Tactic: rw [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
φ : 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
⊢ (if (weight w : (a : σ →₀ ℕ) → M) d = m then coeff d φ else 0) = 0
have a : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [if_neg hm'.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
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) φ)
      ⋯
⊢ (if Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) ((weight w : (a : σ →₀ ℕ) → M) d : M) then coeff d φ
    else 0) =
    0
have a : coeff d φ = 0
Tactic: rw [if_pos rfl]
-- 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
φ : 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) φ)
      ⋯
⊢ coeff d φ = 0
have hm₁ : 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
Cleared hypotheses: hm
-- 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
φ : 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 φ = 0
have 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
Tactic: have := coeff_weightedHomogeneousComponent (w := w) (weight w d) φ d
-- 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
φ : 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
⊢ coeff d φ = 0
have this₁ : 0 = coeff d φ
Tactic: rw [hm, if_pos rfl, coeff_zero] at this
Cleared hypotheses: this
-- 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 : ∑
    i ∈
      Finite.toFinset (s :=
        Function.support (M := MvPolynomial σ R) fun (m : M) ↦
          (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
        sorry,
    (weightedHomogeneousComponent w i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ =
  φ
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) φ =
    φ
⊢ ∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ
have a : ∀ (d : σ →₀ ℕ),
  coeff d
      (∑
        i ∈
          Finite.toFinset (s :=
            Function.support (M := MvPolynomial σ R) fun (m : M) ↦
              (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
            sorry,
        (weightedHomogeneousComponent w i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) =
    coeff d φ
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 φ
⊢ ∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ
have a₁ : ∀ (d : σ →₀ ℕ),
  (∑
      x ∈
        Finite.toFinset (s :=
          Function.support (M := MvPolynomial σ R) fun (m : M) ↦
            (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
          sorry,
      if (weight w : (a : σ →₀ ℕ) → M) d = x then coeff d φ else 0) =
    coeff d φ
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 φ
⊢ ∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ
have 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 φ
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