awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst_2 : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
⊢ ∃ (d : σ →₀ ℕ), coeff d φ ≠ 0

Tactic:
exists_coeff_ne_zero h

Premises used: MvPolynomial.exists_coeff_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst_2 : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
a :
  ∀ (d : σ →₀ ℕ) (hd : coeff d φ ≠ 0),
    (↑n : WithBot M) ≤ φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M)
⊢ (↑n : WithBot M) ≤ φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M)

Tactic:
obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero h

Premises used: MvPolynomial.exists_coeff_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst_2 : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
a :
  LE.le.{u_2} (α := WithBot M) ((↑((weight w : (a : σ →₀ ℕ) → M) d) : WithBot M) : WithBot M)
    (φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M) : WithBot M)
⊢ (↑n : WithBot M) ≤ φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M)

Tactic:
simp only [← hφ hd]
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst_2 : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ d ∈ φ.support

Tactic:
replace hd := Finsupp.mem_support_iff.mpr hd
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst_2 : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ LE.le.{u_2} (α := WithBot M) ((↑((weight w : (a : σ →₀ ℕ) → M) d) : WithBot M) : WithBot M)
    (φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M) : WithBot M)

Tactic:
apply Finset.le_sup hd

Premises used: Finset.le_sup
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
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 : IsWeightedHomogeneous w p m
h : ∀ (a : R), motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) ⋯
⊢ motive p hp

Tactic:
simpa using h 1

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
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 : IsWeightedHomogeneous w p m
suffices :
  ∀ (a : R), motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) ⋯
⊢ motive p hp

Tactic:
suffices h : ∀ a, motive (C a * p) (.C_mul hp _) by simpa using h 1
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
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 : IsWeightedHomogeneous w p m
a_1 b : MvPolynomial σ R
h :
  Membership.mem (γ := Set (MvPolynomial σ R))
    {p : MvPolynomial σ R |
      ∃ (hp : IsWeightedHomogeneous w p m),
        ∀ (a : R),
          motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) ⋯}
    a_1
h_1 :
  Membership.mem (γ := Set (MvPolynomial σ R))
    {p : MvPolynomial σ R |
      ∃ (hp : IsWeightedHomogeneous w p m),
        ∀ (a : R),
          motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) ⋯}
    b
w_1 : IsWeightedHomogeneous w a_1 m
hx : ∀ (a : R), motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) a_1) ⋯
w_2 : IsWeightedHomogeneous w b m
hy : ∀ (a : R), motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) b) ⋯
a : R
⊢ motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) (a_1 + b)) ⋯

Tactic:
simp [mul_add, add _ _ _ _ (hx a) (hy a)]

Premises used: mul_add
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
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 : IsWeightedHomogeneous w p m
⊢ ∀ (a : R),
    motive
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
        (0 : MvPolynomial σ R))
      ⋯

Tactic:
simp [zero]
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
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 : IsWeightedHomogeneous w p m
a : R
x : MvPolynomial σ R
h :
  Membership.mem (γ := Set (MvPolynomial σ R))
    {p : MvPolynomial σ R |
      ∃ (hp : IsWeightedHomogeneous w p m),
        ∀ (a : R),
          motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) ⋯}
    x
w_1 : IsWeightedHomogeneous w x m
hx : ∀ (a : R), motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) x) ⋯
⊢ IsWeightedHomogeneous w (a • x) m

Tactic:
simp [Algebra.smul_def, C_mul ‹_› a]

Premises used: MvPolynomial.IsWeightedHomogeneous.C_mul, Algebra.smul_def
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
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 : IsWeightedHomogeneous w p m
a_1 : R
x : MvPolynomial σ R
h :
  Membership.mem (γ := Set (MvPolynomial σ R))
    {p : MvPolynomial σ R |
      ∃ (hp : IsWeightedHomogeneous w p m),
        ∀ (a : R),
          motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) ⋯}
    x
w_1 : IsWeightedHomogeneous w x m
hx : ∀ (a : R), motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) x) ⋯
a : R
simp_rw : motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (a * a_1) : MvPolynomial σ R) x) ⋯
⊢ motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) (a_1 • x)) ⋯

Tactic:
simp_rw [Algebra.smul_def, algebraMap_eq, ← mul_assoc, ← map_mul]

Premises used: mul_assoc, map_mul, MvPolynomial.algebraMap_eq, Algebra.smul_def
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
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 : IsWeightedHomogeneous w p m
a_1 : R
x : MvPolynomial σ R
h :
  Membership.mem (γ := Set (MvPolynomial σ R))
    {p : MvPolynomial σ R |
      ∃ (hp : IsWeightedHomogeneous w p m),
        ∀ (a : R),
          motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) ⋯}
    x
w_1 : IsWeightedHomogeneous w x m
hx : ∀ (a : R), motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) x) ⋯
a : R
⊢ motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (a * a_1) : MvPolynomial σ R) x) ⋯

Tactic:
apply hx
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
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 : IsWeightedHomogeneous w p m
let : ∀ (a : R), motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) ⋯
⊢ ∀ (a : R), motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) ⋯

Tactic:
let A : Submodule R (MvPolynomial σ R) :=
    { carrier := { p | ∃ hp, ∀ a, motive (C a * p) (.C_mul hp _) }
      add_mem' := fun ⟨_, hx⟩ ⟨_, hy⟩ ↦
        ⟨.add ‹_› ‹_›, fun a ↦ by simp [mul_add, add _ _ _ _ (hx a) (hy a)]⟩
      zero_mem' := ⟨isWeightedHomogeneous_zero R w m, by simp [zero]⟩
      smul_mem' := fun a x ⟨_, hx⟩ ↦ ⟨by simp [Algebra.smul_def, C_mul ‹_› a], fun a ↦ by
        simp_rw [Algebra.smul_def, algebraMap_eq, ← mul_assoc, ← map_mul]
        apply hx⟩ }
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
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 : IsWeightedHomogeneous w p m
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' := ⋯ }
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ Finsupp.single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m})) p

Tactic:
rw [← mem_weightedHomogeneousSubmodule, weightedHomogeneousSubmodule_eq_finsupp_supported,
    Finsupp.supported_eq_span_single] at hp

Premises used: Finsupp.supported_eq_span_single, MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported, MvPolynomial.mem_weightedHomogeneousSubmodule
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
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) ⋯

Tactic:
(Submodule.span_le (p := A) |>.mpr ?_ hp).2

Premises used: Iff.mpr, Submodule.span_le
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
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' := ⋯ }
refine :
  (fun (i : σ →₀ ℕ) ↦ Finsupp.single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m} ⊆
    (↑A : Set (MvPolynomial σ R))
⊢ ∀ (a : R), motive (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p) ⋯

Tactic:
refine (Submodule.span_le (p := A) |>.mpr ?_ hp).2

Premises used: Iff.mpr, Submodule.span_le
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
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' := ⋯ }
rw :
  Subset.{u_3} (α := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m}
    ((fun (i : σ →₀ ℕ) ↦ Finsupp.single i 1) ⁻¹' (↑A : Set (MvPolynomial σ R)))
⊢ (fun (i : σ →₀ ℕ) ↦ Finsupp.single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m} ⊆
    (↑A : Set (MvPolynomial σ R))

Tactic:
rw [Set.image_subset_iff]

Premises used: Set.image_subset_iff
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
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
simp : (MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) 1 ∈ A
⊢ Membership.mem (γ := Set (σ →₀ ℕ)) ((fun (i : σ →₀ ℕ) ↦ Finsupp.single i 1) ⁻¹' (↑A : Set (MvPolynomial σ R))) d

Tactic:
simp only [single_eq_monomial, Set.mem_preimage, SetLike.mem_coe]

Premises used: MvPolynomial.single_eq_monomial, SetLike.mem_coe, Set.mem_preimage
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
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

Tactic:
⟨isWeightedHomogeneous_monomial w d 1 hd, fun a ↦ ?_⟩

Premises used: Set.Mem, setOf, MvPolynomial.isWeightedHomogeneous_monomial, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
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
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))
      ⋯
⊢ (MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) 1 ∈ A

Tactic:
refine ⟨isWeightedHomogeneous_monomial w d 1 hd, fun a ↦ ?_⟩
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
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
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))
    ⋯

Tactic:
simp [MvPolynomial.C_mul_monomial, monomial _ _ hd]

Premises used: MvPolynomial.C_mul_monomial
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
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 : DecidableEq M
d : σ →₀ ℕ
this : DecidableEq M := Classical.decEq M
⊢ Eq.{u_1 + 1} (α := R) (if (weight w : (a : σ →₀ ℕ) → M) d = n then (φ : (a : σ →₀ ℕ) → R) d else 0 : R)
    (if (weight w : (a : σ →₀ ℕ) → M) d = n then (φ : (a : σ →₀ ℕ) → R) d else 0 : R)

Tactic:
rfl

Premises used: rfl