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
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
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
⊢ (↑((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ
have rw : Eq (α := MvPolynomial σ R)
  ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
  ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
Tactic: rw [decompose'_apply]
-- 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
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
⊢ Eq (α := MvPolynomial σ R)
    (∑ x ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ),
      (↑((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) x) : MvPolynomial σ R))
    (∑
      m ∈
        Finite.toFinset (s :=
          Function.support (M := MvPolynomial σ R) fun (m : M) ↦
            (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
          ⋯,
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
have apply : DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ) =
  Finite.toFinset (s :=
    Function.support (M := MvPolynomial σ R) fun (m : M) ↦
      (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
    sorry
Tactic: apply Finset.sum_congr _ (fun m _ ↦ by rw [decompose'_apply])
-- 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
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
⊢ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ) =
    Finite.toFinset (s :=
      Function.support (M := MvPolynomial σ R) fun (m : M) ↦
        (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
      ⋯
have h : ∀ (m : M),
  m ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ) ↔
    Membership.mem (γ := Finset M)
      (Finite.toFinset (s :=
        Function.support (M := MvPolynomial σ R) fun (m : M) ↦
          (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
        sorry)
      m
Tactic: ext 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
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
m : M
⊢ m ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ) ↔
    Membership.mem (γ := Finset M)
      (Finite.toFinset (s :=
        Function.support (M := MvPolynomial σ R) fun (m : M) ↦
          (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
        ⋯)
      m
have h : (decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m = 0 ↔
  Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
Tactic: simp only [DFinsupp.mem_support_toFun, ne_eq, Set.Finite.mem_toFinset, Function.mem_support,
      not_iff_not]
-- 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
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
m : M
| (decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m = 0
have rw : (↑((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) = (↑0 : MvPolynomial σ R)
Tactic: rw [← Subtype.coe_inj]
-- 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
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
m : M
⊢ (decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m = 0 ↔
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
have h : (↑((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
    (↑0 : MvPolynomial σ R) ↔
  Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
Tactic: conv_lhs => rw [← Subtype.coe_inj]
-- 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
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
m : M
⊢ (↑((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
      (↑0 : MvPolynomial σ R) ↔
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
have h : Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    ((↑0 : MvPolynomial σ R) : MvPolynomial σ R) ↔
  Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
Tactic: rw [decompose'_apply, Submodule.coe_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
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
m : M
h :
  Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
      ((↑0 : MvPolynomial σ R) : MvPolynomial σ R) ↔
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
⊢ (↑((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R) =
      (↑0 : MvPolynomial σ R) ↔
    Eq (α := MvPolynomial σ R)
      ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
have h₁ : Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R) ↔
  Eq (α := MvPolynomial σ R)
    ((weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
Tactic: rw [decompose'_apply, Submodule.coe_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
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
⊢ (DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
        (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
      (decompose' R w φ) =
    φ
have conv_rhs : (DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
      (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
    (decompose' R w φ) =
  φ
Tactic: classical
    conv_rhs => rw [← sum_weightedHomogeneousComponent w φ]
    rw [← DirectSum.sum_support_of (decompose' R w φ)]
    simp only [DirectSum.coeAddMonoidHom_of, map_sum,
      finsum_eq_sum _ (weightedHomogeneousComponent_finsupp φ)]
    apply Finset.sum_congr _ (fun m _ ↦ by rw [decompose'_apply])
    ext m
    simp only [DFinsupp.mem_support_toFun, ne_eq, Set.Finite.mem_toFinset, Function.mem_support,
      not_iff_not]
    conv_lhs => rw [← Subtype.coe_inj]
    rw [decompose'_apply, Submodule.coe_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
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
conv_rhs :
  (DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
        (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
      (decompose' R w φ) =
    φ
⊢ (DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
        (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
      (decompose' R w φ) =
    φ
have conv_rhs₁ : Eq (α := MvPolynomial σ R)
  ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
        (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
      (decompose' R w φ) :
    MvPolynomial σ R)
  (∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
Tactic: classical
    conv_rhs => rw [← sum_weightedHomogeneousComponent w φ]
    rw [← DirectSum.sum_support_of (decompose' R w φ)]
    simp only [DirectSum.coeAddMonoidHom_of, map_sum,
      finsum_eq_sum _ (weightedHomogeneousComponent_finsupp φ)]
    apply Finset.sum_congr _ (fun m _ ↦ by rw [decompose'_apply])
    ext m
    simp only [DFinsupp.mem_support_toFun, ne_eq, Set.Finite.mem_toFinset, Function.mem_support,
      not_iff_not]
    conv_lhs => rw [← Subtype.coe_inj]
    rw [decompose'_apply, Submodule.coe_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
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
conv_rhs :
  (DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
        (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
      (decompose' R w φ) =
    φ
conv_rhs₁ conv_rhs₂ :
  Eq (α := MvPolynomial σ R)
    ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
          (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        (decompose' R w φ) :
      MvPolynomial σ R)
    (∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
⊢ (DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
        (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
      (decompose' R w φ) =
    φ
have conv_rhs₃ : Eq (α := MvPolynomial σ R)
  ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
      (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
    (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ),
      ((DirectSum.of (fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) i :
            ↥(weightedHomogeneousSubmodule R w i) →+ DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) :
          (a : ↥(weightedHomogeneousSubmodule R w i)) → DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i))
        ((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i)))
  (∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
Tactic: classical
    conv_rhs => rw [← sum_weightedHomogeneousComponent w φ]
    rw [← DirectSum.sum_support_of (decompose' R w φ)]
    simp only [DirectSum.coeAddMonoidHom_of, map_sum,
      finsum_eq_sum _ (weightedHomogeneousComponent_finsupp φ)]
    apply Finset.sum_congr _ (fun m _ ↦ by rw [decompose'_apply])
    ext m
    simp only [DFinsupp.mem_support_toFun, ne_eq, Set.Finite.mem_toFinset, Function.mem_support,
      not_iff_not]
    conv_lhs => rw [← Subtype.coe_inj]
    rw [decompose'_apply, Submodule.coe_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
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
φ : MvPolynomial σ R
conv_rhs :
  (DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
        (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
      (decompose' R w φ) =
    φ
conv_rhs₁ conv_rhs₂ :
  Eq (α := MvPolynomial σ R)
    ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
          (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        (decompose' R w φ) :
      MvPolynomial σ R)
    (∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
conv_rhs₃ :
  Eq (α := MvPolynomial σ R)
    ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
        (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
      (∑ i ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ),
        ((DirectSum.of (fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) i :
              ↥(weightedHomogeneousSubmodule R w i) →+
                DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) :
            (a : ↥(weightedHomogeneousSubmodule R w i)) →
              DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i))
          ((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i)))
    (∑ᶠ (m : M), (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
⊢ (DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
        (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
      (decompose' R w φ) =
    φ
have conv_rhs₄ : Eq (α := MvPolynomial σ R)
  (∑ x ∈ DFinsupp.support (β := fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) (decompose' R w φ),
    (↑((decompose' R w φ : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) x) : MvPolynomial σ R))
  (∑
    m ∈
      Finite.toFinset (s :=
        Function.support (M := MvPolynomial σ R) fun (m : M) ↦
          (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
        sorry,
    (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
Tactic: classical
    conv_rhs => rw [← sum_weightedHomogeneousComponent w φ]
    rw [← DirectSum.sum_support_of (decompose' R w φ)]
    simp only [DirectSum.coeAddMonoidHom_of, map_sum,
      finsum_eq_sum _ (weightedHomogeneousComponent_finsupp φ)]
    apply Finset.sum_congr _ (fun m _ ↦ by rw [decompose'_apply])
    ext m
    simp only [DFinsupp.mem_support_toFun, ne_eq, Set.Finite.mem_toFinset, Function.mem_support,
      not_iff_not]
    conv_lhs => rw [← Subtype.coe_inj]
    rw [decompose'_apply, Submodule.coe_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
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
x : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)
⊢ decompose' R w
      ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
          (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x) =
    x
have h : ∀ (i : M),
  (decompose' R w
          ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
              (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
            x) :
        (a : M) → ↥(weightedHomogeneousSubmodule R w a))
      i =
    (x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i
Tactic: apply DFinsupp.ext
-- 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
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
x : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ (decompose' R w
          ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
              (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
            x) :
        (a : M) → ↥(weightedHomogeneousSubmodule R w a))
      m =
    (x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m
have h : (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
    ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
        (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
      x) =
  (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
Tactic: rw [← Subtype.coe_inj, decompose'_apply]
-- 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
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
x : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)
⊢ decompose' R w
      ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
          (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x) =
    x
have h : ∀ (i : M),
  (decompose' R w
          ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
              (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
            x) :
        (a : M) → ↥(weightedHomogeneousSubmodule R w a))
      i =
    (x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) i
Tactic: classical
    apply DFinsupp.ext
    intro m
    rw [← Subtype.coe_inj, decompose'_apply]
    exact weightedHomogeneousComponent_directSum R w x 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
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : DecidableEq M
x : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)
h h₁ :
  ∀ (m : M),
    (decompose' R w
            ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
                (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
              x) :
          (a : M) → ↥(weightedHomogeneousSubmodule R w a))
        m =
      (x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m
⊢ decompose' R w
      ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
          (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x) =
    x
have h₂ : ∀ (m : M),
  (weightedHomogeneousComponent w m : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w) :
          (a : DirectSum M fun (i : M) ↦ ↥(weightedHomogeneousSubmodule R w i)) → MvPolynomial σ R)
        x) =
    (↑((x : (a : M) → ↥(weightedHomogeneousSubmodule R w a)) m) : MvPolynomial σ R)
Tactic: classical
    apply DFinsupp.ext
    intro m
    rw [← Subtype.coe_inj, decompose'_apply]
    exact weightedHomogeneousComponent_directSum R w x m
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial (goal)
Goal:
σ : Type u
K : Type v
inst : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
⊢ Function.Injective (α := K) (β := MvPolynomial σ K ⧸ I)
    (⇑(RingHom.comp (Ideal.Quotient.mk I) C) : (a : K) → MvPolynomial σ K ⧸ I)
have refine : ∀ (x : K)
  (hx :
    Eq (α := MvPolynomial σ K ⧸ I)
      ((RingHom.comp (Ideal.Quotient.mk I) C : (a : K) → MvPolynomial σ K ⧸ I) x : MvPolynomial σ K ⧸ I)
      (0 : MvPolynomial σ K ⧸ I)),
  x = 0
Tactic: refine (injective_iff_map_eq_zero _).2 fun x hx => ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial (hypothesis)
Goal:
σ : Type u
K : Type v
inst : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx :
  Eq (α := MvPolynomial σ K ⧸ I)
    ((RingHom.comp (Ideal.Quotient.mk I) C : (a : K) → MvPolynomial σ K ⧸ I) x : MvPolynomial σ K ⧸ I)
    (0 : MvPolynomial σ K ⧸ I)
⊢ x = 0
have hx₁ : Membership.mem (α := MvPolynomial σ K) I ((C : (a : K) → MvPolynomial σ K) x : MvPolynomial σ K)
Tactic: rw [RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial (goal)
Goal:
σ : Type u
K : Type v
inst : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : Membership.mem (α := MvPolynomial σ K) I ((C : (a : K) → MvPolynomial σ K) x : MvPolynomial σ K)
⊢ x = 0
have refine : ∀ (hx0 : ¬x = 0), 1 ∈ I
Tactic: refine _root_.by_contradiction fun hx0 => absurd (I.eq_top_iff_one.2 ?_) hI
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial (hypothesis)
Goal:
σ : Type u
K : Type v
inst : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : Membership.mem (α := MvPolynomial σ K) I ((C : (a : K) → MvPolynomial σ K) x : MvPolynomial σ K)
hx0 : ¬x = 0
⊢ 1 ∈ I
have this : HMul.hMul (α := MvPolynomial σ K) (β := MvPolynomial σ K) ((C : (a : K) → MvPolynomial σ K) x⁻¹ : MvPolynomial σ K)
    ((C : (a : K) → MvPolynomial σ K) x : MvPolynomial σ K) ∈
  I
Tactic: have := I.mul_mem_left (MvPolynomial.C x⁻¹) hx
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial (goal)
Goal:
σ : Type u
K : Type v
inst : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : Membership.mem (α := MvPolynomial σ K) I ((C : (a : K) → MvPolynomial σ K) x : MvPolynomial σ K)
hx0 : ¬x = 0
this :
  HMul.hMul (α := MvPolynomial σ K) (β := MvPolynomial σ K) ((C : (a : K) → MvPolynomial σ K) x⁻¹ : MvPolynomial σ K)
      ((C : (a : K) → MvPolynomial σ K) x : MvPolynomial σ K) ∈
    I
⊢ 1 ∈ I
have rwa : ∀ (this : Membership.mem (α := MvPolynomial σ K) I ((C : (a : K) → MvPolynomial σ K) (x⁻¹ * x) : MvPolynomial σ K)),
  1 ∈ I
Tactic: rwa [← MvPolynomial.C.map_mul, inv_mul_cancel₀ hx0, MvPolynomial.C_1] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial (goal)
Goal:
σ : Type u
K : Type v
inst : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : Membership.mem (α := MvPolynomial σ K) I ((C : (a : K) → MvPolynomial σ K) x : MvPolynomial σ K)
hx0 : ¬x = 0
this :
  HMul.hMul (α := MvPolynomial σ K) (β := MvPolynomial σ K) ((C : (a : K) → MvPolynomial σ K) x⁻¹ : MvPolynomial σ K)
      ((C : (a : K) → MvPolynomial σ K) x : MvPolynomial σ K) ∈
    I
rwa :
  ∀ (this : Membership.mem (α := MvPolynomial σ K) I ((C : (a : K) → MvPolynomial σ K) (x⁻¹ * x) : MvPolynomial σ K)),
    1 ∈ I
⊢ 1 ∈ I
have rwa₁ : ∀ (this : (C : (a : K) → MvPolynomial σ K) 1 ∈ I), 1 ∈ I
Tactic: rwa [← MvPolynomial.C.map_mul, inv_mul_cancel₀ hx0, MvPolynomial.C_1] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial (goal)
Goal:
σ : Type u
K : Type v
inst : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : Membership.mem (α := MvPolynomial σ K) I ((C : (a : K) → MvPolynomial σ K) x : MvPolynomial σ K)
hx0 : ¬x = 0
this :
  HMul.hMul (α := MvPolynomial σ K) (β := MvPolynomial σ K) ((C : (a : K) → MvPolynomial σ K) x⁻¹ : MvPolynomial σ K)
      ((C : (a : K) → MvPolynomial σ K) x : MvPolynomial σ K) ∈
    I
rwa :
  ∀ (this : Membership.mem (α := MvPolynomial σ K) I ((C : (a : K) → MvPolynomial σ K) (x⁻¹ * x) : MvPolynomial σ K)),
    1 ∈ I
rwa₁ : ∀ (this : (C : (a : K) → MvPolynomial σ K) 1 ∈ I), 1 ∈ I
⊢ 1 ∈ I
have rwa₂ : ∀ (this : 1 ∈ I), 1 ∈ I
Tactic: rwa [← MvPolynomial.C.map_mul, inv_mul_cancel₀ hx0, MvPolynomial.C_1] at this
Cleared hypotheses: this