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
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
hm : (x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m = 0
convert_3 :
  Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) (↑0 : MvPolynomial σ R)) 0
convert_3₁ :
  Eq (α := MvPolynomial σ R) ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) 0) 0
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have convert_3₂ : Eq (α := MvPolynomial σ R) 0 0
Tactic: rw [hm, Submodule.coe_zero, map_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
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((coeLinearMap fun (i : M) ↦ weightedHomogeneousSubmodule R w i :
          (a : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
have rw : (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → 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)) =
  (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
Tactic: classical
  rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, map_sum]
  convert! @Finset.sum_eq_single M (MvPolynomial σ R) _ (DFinsupp.support x) _ m _ _
  · rw [IsWeightedHomogeneous.weightedHomogeneousComponent_same (x m).prop]
  · intro n _ hmn
    exact IsWeightedHomogeneous.weightedHomogeneousComponent_ne m (x n).prop hmn.symm
  · rw [DFinsupp.notMem_support_iff]
    intro hm; rw [hm, Submodule.coe_zero, map_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
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
rw :
  (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → 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)) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
⊢ (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((coeLinearMap fun (i : M) ↦ weightedHomogeneousSubmodule R w i :
          (a : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
have rw₁ : (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
    (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R)) =
  (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
Tactic: classical
  rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, map_sum]
  convert! @Finset.sum_eq_single M (MvPolynomial σ R) _ (DFinsupp.support x) _ m _ _
  · rw [IsWeightedHomogeneous.weightedHomogeneousComponent_same (x m).prop]
  · intro n _ hmn
    exact IsWeightedHomogeneous.weightedHomogeneousComponent_ne m (x n).prop hmn.symm
  · rw [DFinsupp.notMem_support_iff]
    intro hm; rw [hm, Submodule.coe_zero, map_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
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
rw :
  (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → 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)) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
rw₁ :
  (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R)) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
⊢ (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((coeLinearMap fun (i : M) ↦ weightedHomogeneousSubmodule R w i :
          (a : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
have rw₂ : ∑ x_1 ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) x_1) : MvPolynomial σ R) =
  (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
Tactic: classical
  rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, map_sum]
  convert! @Finset.sum_eq_single M (MvPolynomial σ R) _ (DFinsupp.support x) _ m _ _
  · rw [IsWeightedHomogeneous.weightedHomogeneousComponent_same (x m).prop]
  · intro n _ hmn
    exact IsWeightedHomogeneous.weightedHomogeneousComponent_ne m (x n).prop hmn.symm
  · rw [DFinsupp.notMem_support_iff]
    intro hm; rw [hm, Submodule.coe_zero, map_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
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
rw :
  (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → 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)) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
rw₁ :
  (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R)) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
rw₂ rw₃ rw₄ :
  ∑ x_1 ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) x_1) : MvPolynomial σ R) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
⊢ (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((coeLinearMap fun (i : M) ↦ weightedHomogeneousSubmodule R w i :
          (a : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
have h : (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
  (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
Tactic: classical
  rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, map_sum]
  convert! @Finset.sum_eq_single M (MvPolynomial σ R) _ (DFinsupp.support x) _ m _ _
  · rw [IsWeightedHomogeneous.weightedHomogeneousComponent_same (x m).prop]
  · intro n _ hmn
    exact IsWeightedHomogeneous.weightedHomogeneousComponent_ne m (x n).prop hmn.symm
  · rw [DFinsupp.notMem_support_iff]
    intro hm; rw [hm, Submodule.coe_zero, map_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
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
rw :
  (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → 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)) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
rw₁ :
  (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R)) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
rw₂ rw₃ rw₄ :
  ∑ x_1 ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) x_1) : MvPolynomial σ R) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
h :
  (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
⊢ (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((coeLinearMap fun (i : M) ↦ weightedHomogeneousSubmodule R w i :
          (a : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
have convert_2 : ∀ b ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
  b ≠ m →
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
          (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) b) : MvPolynomial σ R) :
        MvPolynomial σ R)
      (0 : MvPolynomial σ R)
Tactic: classical
  rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, map_sum]
  convert! @Finset.sum_eq_single M (MvPolynomial σ R) _ (DFinsupp.support x) _ m _ _
  · rw [IsWeightedHomogeneous.weightedHomogeneousComponent_same (x m).prop]
  · intro n _ hmn
    exact IsWeightedHomogeneous.weightedHomogeneousComponent_ne m (x n).prop hmn.symm
  · rw [DFinsupp.notMem_support_iff]
    intro hm; rw [hm, Submodule.coe_zero, map_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
inst_2 : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
rw :
  (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → 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)) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
rw₁ :
  (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i) : MvPolynomial σ R)) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
rw₂ rw₃ rw₄ :
  ∑ x_1 ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) x_1) : MvPolynomial σ R) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
h :
  (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
convert_2 :
  ∀ b ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x,
    b ≠ m →
      Eq (α := MvPolynomial σ R)
        ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
            (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) b) : MvPolynomial σ R) :
          MvPolynomial σ R)
        (0 : MvPolynomial σ R)
⊢ (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((coeLinearMap fun (i : M) ↦ weightedHomogeneousSubmodule R w i :
          (a : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
have convert_3 : m ∉ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) x →
  Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)
Tactic: classical
  rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, map_sum]
  convert! @Finset.sum_eq_single M (MvPolynomial σ R) _ (DFinsupp.support x) _ m _ _
  · rw [IsWeightedHomogeneous.weightedHomogeneousComponent_same (x m).prop]
  · intro n _ hmn
    exact IsWeightedHomogeneous.weightedHomogeneousComponent_ne m (x n).prop hmn.symm
  · rw [DFinsupp.notMem_support_iff]
    intro hm; rw [hm, Submodule.coe_zero, map_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
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ) : MvPolynomial σ R)
have a : ∀ (d : σ →₀ ℕ),
  Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))
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
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
⊢ Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))
have a : Eq.{u_1 + 1} (α := R)
  (coeff.{u_1, u_3} (σ := σ) 0 ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
  (coeff.{u_1, u_3} (σ := σ) 0 ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))
Tactic: rcases Classical.em (d = 0) with (rfl | hd)
Cleared hypotheses: 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
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
a :
  Eq.{u_1 + 1} (α := R)
    (coeff.{u_1, u_3} (σ := σ) 0 ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (coeff.{u_1, u_3} (σ := σ) 0 ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))
⊢ Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))
have a₁ : ∀ (hd : ¬d = 0),
  Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))
Tactic: rcases Classical.em (d = 0) with (rfl | 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
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))
have a : ¬Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) (0 : M)
Tactic: rw [coeff_weightedHomogeneousComponent, if_neg, coeff_C, if_neg (Ne.symm 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
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ¬Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) (0 : M)
have a : ∃ (x : σ), ¬Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ) ∧ ¬w x = 0
Tactic: simp only [weight, LinearMap.toAddMonoidHom_coe, Finsupp.linearCombination_apply, Finsupp.sum,
      sum_eq_zero_iff, Finsupp.mem_support_iff, Ne, smul_eq_zero, not_forall, not_or,
      and_self_left, exists_prop]
-- 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
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ∃ (x : σ), ¬Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ) ∧ ¬w x = 0
have hd₁ : ∃ (x : σ), ¬Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
Tactic: simp only [DFunLike.ext_iff, Finsupp.coe_zero, Pi.zero_apply, not_forall] 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
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ∃ (x : σ), ¬Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
⊢ ∃ (x : σ), ¬Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ) ∧ ¬w x = 0
have a : ∀ (i : σ) (hi : ¬Eq (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (0 : ℕ)),
  ∃ (x : σ), ¬Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ) ∧ ¬w x = 0
Tactic: obtain ⟨i, hi⟩ := 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
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ) : MvPolynomial σ R)
have a : ∀ (m : σ →₀ ℕ),
  Eq.{u_1 + 1} (α := R) (coeff m ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (coeff m ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))
Tactic: classical
  ext1 d
  rcases Classical.em (d = 0) with (rfl | hd)
  · simp only [coeff_weightedHomogeneousComponent, if_pos, map_zero, coeff_zero_C]
  · rw [coeff_weightedHomogeneousComponent, if_neg, coeff_C, if_neg (Ne.symm hd)]
    simp only [weight, LinearMap.toAddMonoidHom_coe, Finsupp.linearCombination_apply, Finsupp.sum,
      sum_eq_zero_iff, Finsupp.mem_support_iff, Ne, smul_eq_zero, not_forall, not_or,
      and_self_left, exists_prop]
    simp only [DFunLike.ext_iff, Finsupp.coe_zero, Pi.zero_apply, not_forall] at hd
    obtain ⟨i, hi⟩ := hd
    exact ⟨i, hi, hw i⟩
-- 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
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
a a₁ a₂ a₃ a₄ :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
      (coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ) : MvPolynomial σ R)
have a₅ : Eq.{u_1 + 1} (α := R)
  (coeff.{u_1, u_3} (σ := σ) 0 ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
  (coeff.{u_1, u_3} (σ := σ) 0 ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))
Tactic: classical
  ext1 d
  rcases Classical.em (d = 0) with (rfl | hd)
  · simp only [coeff_weightedHomogeneousComponent, if_pos, map_zero, coeff_zero_C]
  · rw [coeff_weightedHomogeneousComponent, if_neg, coeff_C, if_neg (Ne.symm hd)]
    simp only [weight, LinearMap.toAddMonoidHom_coe, Finsupp.linearCombination_apply, Finsupp.sum,
      sum_eq_zero_iff, Finsupp.mem_support_iff, Ne, smul_eq_zero, not_forall, not_or,
      and_self_left, exists_prop]
    simp only [DFunLike.ext_iff, Finsupp.coe_zero, Pi.zero_apply, not_forall] at hd
    obtain ⟨i, hi⟩ := hd
    exact ⟨i, hi, hw i⟩
-- 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
inst_2 : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst_3 : CanonicallyOrderedAdd M
inst_4 : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
a a₁ a₂ a₃ a₄ :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
      (coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))
a₅ :
  Eq.{u_1 + 1} (α := R)
    (coeff.{u_1, u_3} (σ := σ) 0 ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (coeff.{u_1, u_3} (σ := σ) 0 ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))
⊢ Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ) : MvPolynomial σ R)
have a₆ : ∀ (d : σ →₀ ℕ) (hd : ¬d = 0),
  Eq.{u_1 + 1} (α := R) (coeff d ((weightedHomogeneousComponent w 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 φ)))
Tactic: classical
  ext1 d
  rcases Classical.em (d = 0) with (rfl | hd)
  · simp only [coeff_weightedHomogeneousComponent, if_pos, map_zero, coeff_zero_C]
  · rw [coeff_weightedHomogeneousComponent, if_neg, coeff_C, if_neg (Ne.symm hd)]
    simp only [weight, LinearMap.toAddMonoidHom_coe, Finsupp.linearCombination_apply, Finsupp.sum,
      sum_eq_zero_iff, Finsupp.mem_support_iff, Ne, smul_eq_zero, not_forall, not_or,
      and_self_left, exists_prop]
    simp only [DFunLike.ext_iff, Finsupp.coe_zero, Pi.zero_apply, not_forall] at hd
    obtain ⟨i, hi⟩ := hd
    exact ⟨i, hi, hw i⟩