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
m : M
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial :
  ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w : (a : σ →₀ ℕ) → M) d = m),
    motive ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r) ⋯
p : MvPolynomial σ R
hp_1 : IsWeightedHomogeneous w p m
hp :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ Finsupp.single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m})) p
A : Submodule R (MvPolynomial σ R) :=
  {
    carrier :=
      {p : MvPolynomial σ R |
        ∃ (hp : IsWeightedHomogeneous w p m),
          ∀ (a : R),
            motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) ⋯},
    add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ ∀ (a : R), motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) ⋯
have refine : (fun (i : σ →₀ ℕ) ↦ Finsupp.single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m} ⊆
  (↑A : Set (MvPolynomial σ R))
Tactic: refine (Submodule.span_le (p := A) |>.mpr ?_ hp).2
-- 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
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial :
  ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w : (a : σ →₀ ℕ) → M) d = m),
    motive ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r) ⋯
p : MvPolynomial σ R
hp_1 : IsWeightedHomogeneous w p m
hp :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ Finsupp.single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m})) p
A : Submodule R (MvPolynomial σ R) :=
  {
    carrier :=
      {p : MvPolynomial σ R |
        ∃ (hp : IsWeightedHomogeneous w p m),
          ∀ (a : R),
            motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) ⋯},
    add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ (fun (i : σ →₀ ℕ) ↦ Finsupp.single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m} ⊆
    (↑A : Set (MvPolynomial σ R))
have rw : Subset.{u_3} (α := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m}
  ((fun (i : σ →₀ ℕ) ↦ Finsupp.single i 1) ⁻¹' (↑A : Set (MvPolynomial σ R)))
Tactic: rw [Set.image_subset_iff]
-- 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
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial :
  ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w : (a : σ →₀ ℕ) → M) d = m),
    motive ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r) ⋯
p : MvPolynomial σ R
hp_1 : IsWeightedHomogeneous w p m
hp :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ Finsupp.single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m})) p
A : Submodule R (MvPolynomial σ R) :=
  {
    carrier :=
      {p : MvPolynomial σ R |
        ∃ (hp : IsWeightedHomogeneous w p m),
          ∀ (a : R),
            motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) ⋯},
    add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
d : σ →₀ ℕ
hd : Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m} d
⊢ Membership.mem (γ := Set (σ →₀ ℕ)) ((fun (i : σ →₀ ℕ) ↦ Finsupp.single i 1) ⁻¹' (↑A : Set (MvPolynomial σ R))) d
have simp : (MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) 1 ∈ A
Tactic: simp only [single_eq_monomial, Set.mem_preimage, SetLike.mem_coe]
-- 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
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial :
  ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w : (a : σ →₀ ℕ) → M) d = m),
    motive ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r) ⋯
p : MvPolynomial σ R
hp_1 : IsWeightedHomogeneous w p m
hp :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ Finsupp.single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m})) p
A : Submodule R (MvPolynomial σ R) :=
  {
    carrier :=
      {p : MvPolynomial σ R |
        ∃ (hp : IsWeightedHomogeneous w p m),
          ∀ (a : R),
            motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) ⋯},
    add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
d : σ →₀ ℕ
hd : Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m} d
⊢ (MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) 1 ∈ A
have refine : ∀ (a : R),
  motive
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R))
    sorry
Tactic: refine ⟨isWeightedHomogeneous_monomial w d 1 hd, fun a ↦ ?_⟩
-- 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
d : σ →₀ ℕ
hd :
  Ne.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
⊢ (weight w : (a : σ →₀ ℕ) → M) d = n
have contrapose! : ∀ (hd : (weight w : (a : σ →₀ ℕ) → M) d ≠ n),
  Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
Tactic: contrapose! hd
Cleared hypotheses: hd
-- 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
d : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → M) d ≠ n
⊢ Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
have rw : (if (weight w : (a : σ →₀ ℕ) → M) d = n then coeff d φ else 0) = 0
Tactic: rw [coeff_weightedHomogeneousComponent, if_neg hd]
-- 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
d : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → M) d ≠ n
rw : (if (weight w : (a : σ →₀ ℕ) → M) d = n then coeff d φ else 0) = 0
⊢ Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
have rw₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [coeff_weightedHomogeneousComponent, if_neg hd]
-- 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
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) n
have intro : ∀ ⦃d : σ →₀ ℕ⦄,
  Ne.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0 →
    (weight w : (a : σ →₀ ℕ) → M) d = n
Tactic: classical
  intro d hd
  contrapose! hd
  rw [coeff_weightedHomogeneousComponent, if_neg hd]
-- 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
intro intro₁ :
  ∀ ⦃d : σ →₀ ℕ⦄
    (hd :
      Ne.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
        0),
    (weight w : (a : σ →₀ ℕ) → M) d = n
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) n
have intro₂ : ∀ ⦃d : σ →₀ ℕ⦄ (hd : (weight w : (a : σ →₀ ℕ) → M) d ≠ n),
  Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
Tactic: classical
  intro d hd
  contrapose! hd
  rw [coeff_weightedHomogeneousComponent, if_neg hd]
-- 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
h : ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ n
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have 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)
Tactic: rw [weightedHomogeneousComponent_apply, sum_eq_zero]
-- 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
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ n
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)
have hd₁ : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n
Tactic: rw [mem_filter] at hd
Cleared hypotheses: hd
-- 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
h : ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ n
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)
have exfalso : False
Tactic: exfalso
-- 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
h : ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ n
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have rw : Eq (α := MvPolynomial σ R)
  (∑ d ∈ φ.support with (weight w : (a : σ →₀ ℕ) → M) d = n, (monomial d : (a : R) → MvPolynomial σ R) (coeff d φ)) 0
Tactic: classical
  rw [weightedHomogeneousComponent_apply, sum_eq_zero]
  intro d hd; rw [mem_filter] at hd
  exfalso; exact h _ hd.1 hd.2
-- 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
h : ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ n
rw :
  Eq (α := MvPolynomial σ R)
    (∑ d ∈ φ.support with (weight w : (a : σ →₀ ℕ) → M) d = n, (monomial d : (a : R) → MvPolynomial σ R) (coeff d φ)) 0
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have rw₁ : Eq (α := MvPolynomial σ R) 0 0
Tactic: classical
  rw [weightedHomogeneousComponent_apply, sum_eq_zero]
  intro d hd; rw [mem_filter] at hd
  exfalso; exact h _ hd.1 hd.2
-- 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
h : ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ n
rw :
  Eq (α := MvPolynomial σ R)
    (∑ d ∈ φ.support with (weight w : (a : σ →₀ ℕ) → M) d = n, (monomial d : (a : R) → MvPolynomial σ R) (coeff d φ)) 0
rw₁ : Eq (α := MvPolynomial σ R) 0 0
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have 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)
Tactic: classical
  rw [weightedHomogeneousComponent_apply, sum_eq_zero]
  intro d hd; rw [mem_filter] at hd
  exfalso; exact h _ hd.1 hd.2
-- 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
h : ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ n
rw :
  Eq (α := MvPolynomial σ R)
    (∑ d ∈ φ.support with (weight w : (a : σ →₀ ℕ) → M) d = n, (monomial d : (a : R) → MvPolynomial σ R) (coeff d φ)) 0
rw₁ : Eq (α := MvPolynomial σ R) 0 0
rw₂ :
  ∀ x ∈ {d ∈ φ.support | (weight w : (a : σ →₀ ℕ) → M) d = n},
    Eq (α := MvPolynomial σ R) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x φ) : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
rw₃ : Eq (α := MvPolynomial σ R) 0 0
rw₄ rw₅ rw₆ rw₇ :
  ∀ (d : σ →₀ ℕ) (hd : d ∈ {d ∈ φ.support | (weight w : (a : σ →₀ ℕ) → M) d = n}),
    Eq (α := MvPolynomial σ R) ((monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
⊢ 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),
  Eq (α := MvPolynomial σ R) ((monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
Tactic: classical
  rw [weightedHomogeneousComponent_apply, sum_eq_zero]
  intro d hd; rw [mem_filter] at hd
  exfalso; exact h _ hd.1 hd.2
-- 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
h : ∀ d ∈ φ.support, (weight w : (a : σ →₀ ℕ) → M) d ≠ n
rw :
  Eq (α := MvPolynomial σ R)
    (∑ d ∈ φ.support with (weight w : (a : σ →₀ ℕ) → M) d = n, (monomial d : (a : R) → MvPolynomial σ R) (coeff d φ)) 0
rw₁ : Eq (α := MvPolynomial σ R) 0 0
rw₂ :
  ∀ x ∈ {d ∈ φ.support | (weight w : (a : σ →₀ ℕ) → M) d = n},
    Eq (α := MvPolynomial σ R) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x φ) : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
rw₃ : Eq (α := MvPolynomial σ R) 0 0
rw₄ rw₅ rw₆ rw₇ :
  ∀ (d : σ →₀ ℕ) (hd : d ∈ {d ∈ φ.support | (weight w : (a : σ →₀ ℕ) → M) d = n}),
    Eq (α := MvPolynomial σ R) ((monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
rw₈ :
  ∀ (d : σ →₀ ℕ) (hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n),
    Eq (α := MvPolynomial σ R) ((monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
⊢ 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 [mem_filter] at hd
  exfalso; exact h _ hd.1 hd.2
-- 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
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have 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)
Tactic: rw [weightedHomogeneousComponent_apply, sum_eq_zero]
-- 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
n : M
φ : MvPolynomial σ R
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ {d ∈ φ.support | (weight w : (a : σ →₀ ℕ) → M) d = n}
⊢ Eq (α := MvPolynomial σ R) ((monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have hd₁ : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n
Tactic: rw [Finset.mem_filter] at hd
Cleared hypotheses: hd
-- 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
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)
have exfalso : False
Tactic: exfalso
-- 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
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n
⊢ False
have apply : n < n
Tactic: apply lt_irrefl n
-- 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
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w : (a : σ →₀ ℕ) → M) d = n
⊢ n < n
have nth_rw : (weight w : (a : σ →₀ ℕ) → M) d < n
Tactic: nth_rw 1 [← hd.2]
-- 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
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have rw : Eq (α := MvPolynomial σ R)
  (∑ d ∈ φ.support with (weight w : (a : σ →₀ ℕ) → M) d = n, (monomial d : (a : R) → MvPolynomial σ R) (coeff d φ)) 0
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
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have rw₁ : Eq (α := MvPolynomial σ R) 0 0
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
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w n : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have 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)
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)
⊢ 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),
  Eq (α := MvPolynomial σ R) ((monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
Tactic: classical
  rw [weightedHomogeneousComponent_apply, sum_eq_zero]
  intro d hd
  rw [Finset.mem_filter] at hd
  exfalso
  apply lt_irrefl n
  nth_rw 1 [← hd.2]
  exact lt_of_le_of_lt (le_weightedTotalDegree w hd.1) h