awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
s : Set (σ →₀ ℕ)
⊢ restrictSupport R (HSMul.hSMul (α := ℕ) 0 s) =
    HPow.hPow (α := Submodule R (MvPolynomial σ R)) (β := ℕ) (restrictSupport R s) 0

Tactic:
simp [add_smul, restrictSupport_add, *, pow_succ]

Premises used: pow_succ, add_smul, MvPolynomial.restrictSupport_add
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
s : Set (σ →₀ ℕ)
n : ℕ
h : restrictSupport R (n • s) = HPow.hPow (α := Submodule R (MvPolynomial σ R)) (restrictSupport R s) n
⊢ restrictSupport R ((n + 1) • s) = HPow.hPow (α := Submodule R (MvPolynomial σ R)) (restrictSupport R s) (n + 1)

Tactic:
simp [add_smul, restrictSupport_add, *, pow_succ]

Premises used: pow_succ, add_smul, MvPolynomial.restrictSupport_add
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m_1 : ℕ
s : Set (σ →₀ ℕ)
hs : IsUpperSet s
x y : MvPolynomial σ R
hy :
  Membership.mem (γ := Set (MvPolynomial σ R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (restrictSupport R s)))) y
m : σ →₀ ℕ
hm : m ∈ (x * y).support
⊢ ¬Eq.{v + 1} (α := R) (∑ x_1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ m, coeff x_1.1 x * coeff x_1.2 y) 0

Tactic:
simp only [mem_support_iff, coeff_mul, ne_eq] at hm

Premises used: MvPolynomial.mem_support_iff, ne_eq, MvPolynomial.coeff_mul
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m_1 : ℕ
s : Set (σ →₀ ℕ)
hs : IsUpperSet s
x y : MvPolynomial σ R
hy :
  Membership.mem (γ := Set (MvPolynomial σ R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (restrictSupport R s)))) y
m : σ →₀ ℕ
hm : ¬Eq.{v + 1} (α := R) (∑ x_1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ m, coeff x_1.1 x * coeff x_1.2 y) 0
obtain :
  ∀ (i j : σ →₀ ℕ) (hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ m)
    (e : coeff (i, j).1 x * coeff (i, j).2 y ≠ 0), m ∈ s
⊢ m ∈ s

Tactic:
obtain ⟨⟨i, j⟩, hij, e⟩ := Finset.exists_ne_zero_of_sum_ne_zero hm

Premises used: Finset.exists_ne_zero_of_sum_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m_1 : ℕ
s : Set (σ →₀ ℕ)
hs : IsUpperSet s
x y : MvPolynomial σ R
hy :
  Membership.mem (γ := Set (MvPolynomial σ R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (restrictSupport R s)))) y
m : σ →₀ ℕ
hm : ¬Eq.{v + 1} (α := R) (∑ x_1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ m, coeff x_1.1 x * coeff x_1.2 y) 0
i j : σ →₀ ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ m
e : coeff (i, j).1 x * coeff (i, j).2 y ≠ 0
⊢ j ≤ m

Tactic:
simp_all [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m_1 : ℕ
s : Set (σ →₀ ℕ)
hs : IsUpperSet s
x y : MvPolynomial σ R
hy :
  Membership.mem (γ := Set (MvPolynomial σ R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (restrictSupport R s)))) y
m : σ →₀ ℕ
hm : ¬Eq.{v + 1} (α := R) (∑ x_1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ m, coeff x_1.1 x * coeff x_1.2 y) 0
i j : σ →₀ ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ m
e : coeff (i, j).1 x * coeff (i, j).2 y ≠ 0
⊢ j ∈ y.support

Tactic:
aesop
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m_1 : ℕ
s : Set (σ →₀ ℕ)
hs : IsUpperSet s
x y : MvPolynomial σ R
hy :
  Membership.mem (γ := Set (MvPolynomial σ R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (restrictSupport R s)))) y
m : σ →₀ ℕ
hm : ¬Eq.{v + 1} (α := R) (∑ x_1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ m, coeff x_1.1 x * coeff x_1.2 y) 0
i j : σ →₀ ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ m
e : coeff (i, j).1 x * coeff (i, j).2 y ≠ 0
⊢ m ∈ s

Tactic:
refine hs (by simp_all [eq_comm]) (hy (show j ∈ y.support by aesop))
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m_1 : ℕ
s : Set (σ →₀ ℕ)
hs : IsUpperSet s
x y : MvPolynomial σ R
hy :
  Membership.mem (γ := Set (MvPolynomial σ R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (restrictSupport R s)))) y
m : σ →₀ ℕ
hm : m ∈ (x * y).support
simp :
  ∀
    (hm :
      ¬Eq.{v + 1} (α := R) (∑ x_1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ m, coeff x_1.1 x * coeff x_1.2 y) 0),
    m ∈ s
simp₁ :
  ∀
    (hm :
      ¬Eq.{v + 1} (α := R) (∑ x_1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ m, coeff x_1.1 x * coeff x_1.2 y) 0)
    (i j : σ →₀ ℕ) (hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ m)
    (e : coeff (i, j).1 x * coeff (i, j).2 y ≠ 0), m ∈ s
⊢ m ∈ s

Tactic:
classical
    simp only [mem_support_iff, coeff_mul, ne_eq] at hm
    obtain ⟨⟨i, j⟩, hij, e⟩ := Finset.exists_ne_zero_of_sum_ne_zero hm
    refine hs (by simp_all [eq_comm]) (hy (show j ∈ y.support by aesop))

Premises used: MvPolynomial.mem_support_iff, ne_eq, MvPolynomial.coeff_mul
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
s : Set (σ →₀ ℕ)
hs : IsUpperSet s
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (Submodule.restrictScalars R (restrictSupportIdeal R s hs))
    (restrictSupport R s)

Tactic:
rfl

Premises used: Submodule.restrictScalars, Finsupp.supported, setOf, AddMonoidAlgebra, rfl, MvPolynomial.restrictSupport
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
m : ℕ
p : MvPolynomial σ R
rw :
  Membership.mem (γ := Submodule R (MvPolynomial σ R)) (restrictTotalDegree σ R m) p ↔
    ∀ b ∈ p.support, (b.sum fun (x : σ) (e : ℕ) ↦ e) ≤ m
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R)) (restrictTotalDegree σ R m) p ↔ p.totalDegree ≤ m

Tactic:
rw [totalDegree, Finset.sup_le_iff]

Premises used: MvPolynomial.totalDegree, Finset.sup_le_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
m : ℕ
p : MvPolynomial σ R
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R)) (restrictTotalDegree σ R m) p ↔
    ∀ b ∈ p.support, (b.sum fun (x : σ) (e : ℕ) ↦ e) ≤ m

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p : MvPolynomial σ R
n : ℕ
⊢ (↑p.support : Set (σ →₀ ℕ)) ⊆ {n_1 : σ →₀ ℕ | ∀ (i : σ), (n_1 : (a : σ) → ℕ) i ≤ n} ↔
    ∀ s ∈ p.support, ∀ (i : σ), (s : (a : σ) → ℕ) i ≤ n

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
inst_1 : DecidableEq σ
p : MvPolynomial σ R
n : ℕ
simp : (∀ s ∈ p.support, ∀ (i : σ), (s : (a : σ) → ℕ) i ≤ n) ↔ ∀ (i : σ), ∀ b ∈ p.support, (b : (a : σ) → ℕ) i ≤ n
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R)) (restrictDegree σ R n) p ↔
    ∀ (i : σ), Multiset.count i p.degrees ≤ n

Tactic:
simp only [mem_restrictDegree, degrees_def, Multiset.count_finset_sup, Finsupp.count_toMultiset,
    Finset.sup_le_iff]

Premises used: MvPolynomial.degrees_def, Finsupp.count_toMultiset, MvPolynomial.mem_restrictDegree, Multiset.count_finset_sup, Finset.sup_le_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
inst_1 : DecidableEq σ
p : MvPolynomial σ R
n : ℕ
⊢ (∀ s ∈ p.support, ∀ (i : σ), (s : (a : σ) → ℕ) i ≤ n) ↔ ∀ (i : σ), ∀ b ∈ p.support, (b : (a : σ) → ℕ) i ≤ n

Tactic:
⟨fun h n s hs => h s hs n, fun h s hs n => h n s hs⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
inst_1 : DecidableEq σ
p : MvPolynomial σ R
n : ℕ
⊢ (∀ s ∈ p.support, ∀ (i : σ), (s : (a : σ) → ℕ) i ≤ n) ↔ ∀ (i : σ), ∀ b ∈ p.support, (b : (a : σ) → ℕ) i ≤ n

Tactic:
exact ⟨fun h n s hs => h s hs n, fun h s hs n => h n s hs⟩
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
m : ℕ
⊢ LE.le (α := Submodule R (MvPolynomial σ R)) (restrictTotalDegree σ R m) (restrictDegree σ R m)

Tactic:
fun p hp ↦ (mem_restrictDegree _ _ _).mpr fun s hs i ↦ (degreeOf_le_iff.mp
    (degreeOf_le_totalDegree p i) s hs).trans ((mem_restrictTotalDegree _ _ _).mp hp)

Premises used: Iff.mpr, Set.Mem, MvPolynomial.degreeOf_le_totalDegree, MvPolynomial.degreeOf_le_iff, MvPolynomial.mem_restrictDegree, Iff.mp, LE.le.trans, MvPolynomial.mem_restrictTotalDegree
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
⊢ Eq (α := (a : σ →₀ ℕ) → MvPolynomial σ R) (⇑(basisMonomials σ R) : (a : σ →₀ ℕ) → MvPolynomial σ R) fun (s : σ →₀ ℕ) ↦
    (monomial s : (a : R) → MvPolynomial σ R) 1

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m : ℕ
⊢ Free R (MvPolynomial σ R)

Tactic:
Module.Free.of_basis (MvPolynomial.basisMonomials σ R)

Premises used: MvPolynomial.basisMonomials, Module.Free.of_basis
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
⊢ LinearIndependent (ι := σ) R (M := MvPolynomial σ R) X

Tactic:
(basisMonomials σ R).linearIndependent.comp (fun s : σ => Finsupp.single s 1)
    (Finsupp.single_left_injective one_ne_zero)

Premises used: MvPolynomial.X, Finsupp.single_left_injective, MvPolynomial.basisMonomials, Module.Basis.linearIndependent, one_ne_zero, OfNat.ofNat, LinearIndependent.comp, Finsupp.single
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
α : Type u_1
inst : Finite α
n : ℕ
⊢ Finite.{u_1 + 1} (↑{f : α →₀ ℕ | ∀ (a : α), (f : (a : α) → ℕ) a ≤ n} : Type u_1)

Tactic:
((Set.Finite.pi' fun _ ↦ Set.finite_le_nat _).preimage DFunLike.coe_injective.injOn).to_subtype

Premises used: Set.Mem, Function.Injective.injOn, setOf, Set.Finite.to_subtype, Set.Finite.pi', Set.preimage, DFunLike.coe_injective, Set.finite_le_nat, Set.Finite.preimage
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m : ℕ
inst_1 : Finite σ
N : ℕ
⊢ Module.Finite R ↥(restrictDegree σ R N)

Tactic:
have := finite_setOf_bounded σ N
  Module.Finite.of_basis (basisRestrictSupport R _)

Premises used: setOf, _private.0.MvPolynomial.finite_setOf_bounded, MvPolynomial.basisRestrictSupport, Module.Finite.of_basis
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m : ℕ
inst_1 : Finite σ
N : ℕ
this : Finite.{u + 1} (↑{f : σ →₀ ℕ | ∀ (a : σ), (f : (a : σ) → ℕ) a ≤ N} : Type u)
⊢ Set.Finite.{u} (α := σ →₀ ℕ) {f : σ →₀ ℕ | ∀ (a : σ), (f : (a : σ) → ℕ) a ≤ N}

Tactic:
rw [Set.finite_coe_iff] at this ⊢

Premises used: Set.finite_coe_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m : ℕ
inst_1 : Finite σ
N : ℕ
this : Set.Finite.{u} (α := σ →₀ ℕ) {f : σ →₀ ℕ | ∀ (a : σ), (f : (a : σ) → ℕ) a ≤ N}
⊢ Set.Finite.{u} (α := σ →₀ ℕ) {s : σ →₀ ℕ | (s.sum fun (x : σ) (e : ℕ) ↦ e) ≤ N}

Tactic:
this.subset fun n hn i ↦ (eq_or_ne (n i) 0).elim
      (fun h ↦ h.trans_le N.zero_le) fun h ↦
        (Finset.single_le_sum (fun _ _ ↦ Nat.zero_le _) <| Finsupp.mem_support_iff.mpr h).trans hn

Premises used: Iff.mpr, Finsupp.mem_support_iff, Nat.zero_le, Set.Finite.subset, Eq.trans_le, Finset.single_le_sum, eq_or_ne, LE.le.trans, Or.elim, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m : ℕ
inst_1 : Finite σ
N : ℕ
this : Set.Finite.{u} (α := σ →₀ ℕ) {f : σ →₀ ℕ | ∀ (a : σ), (f : (a : σ) → ℕ) a ≤ N}
⊢ Set.Finite.{u} (α := σ →₀ ℕ) {s : σ →₀ ℕ | (s.sum fun (x : σ) (e : ℕ) ↦ e) ≤ N}

Tactic:
exact this.subset fun n hn i ↦ (eq_or_ne (n i) 0).elim
      (fun h ↦ h.trans_le N.zero_le) fun h ↦
        (Finset.single_le_sum (fun _ _ ↦ Nat.zero_le _) <| Finsupp.mem_support_iff.mpr h).trans hn

Premises used: Iff.mpr, Finsupp.mem_support_iff, Nat.zero_le, Set.Finite.subset, Eq.trans_le, Finset.single_le_sum, eq_or_ne, LE.le.trans, Or.elim, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
M : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : IsWeightedHomogeneous w φ n
h' : n' + w i = n
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n})) φ

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

Premises used: Finsupp.supported_eq_span_single, MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported, MvPolynomial.mem_weightedHomogeneousSubmodule
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
M : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : IsWeightedHomogeneous w φ n
h' : n' + w i = n
h₁ :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n})) φ
⊢ n' + w i = n

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

Premises used: Finsupp.supported_eq_span_single, MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported, MvPolynomial.mem_weightedHomogeneousSubmodule
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
M : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n})) φ
h' : n' + w i = n
⊢ IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) n'

Tactic:
Submodule.span_induction ?_ ?_ (fun p q _ _ hp hq ↦ ?_) (fun r p _ h ↦ ?_) h

Premises used: Submodule.span_induction
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
M : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n})) φ
h' : n' + w i = n
refine_1 :
  ∀ (x : MvPolynomial σ R)
    (h :
      Membership.mem (γ := Set (MvPolynomial σ R))
        ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n}) x),
    IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) x) n'
refine_2 :
  IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) 0) n'
refine_3 :
  ∀ (p q : MvPolynomial σ R),
    Membership.mem (γ := Submodule R (MvPolynomial σ R))
        (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n})) p →
      Membership.mem (γ := Submodule R (MvPolynomial σ R))
          (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n})) q →
        ∀
          (hp :
            IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p)
              n')
          (hq :
            IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) q)
              n'),
          IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w
            ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (p + q)) n'
refine_4 :
  ∀ (r : R) (p : MvPolynomial σ R),
    Membership.mem (γ := Submodule R (MvPolynomial σ R))
        (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n})) p →
      ∀
        (h :
          IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p)
            n'),
        IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (r • p)) n'
⊢ IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) n'

Tactic:
refine Submodule.span_induction ?_ ?_ (fun p q _ _ hp hq ↦ ?_) (fun r p _ h ↦ ?_) h
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
M : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n})) φ
h' : n' + w i = n
m : σ →₀ ℕ
hm : Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n} m
refine_1 :
  IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w
    ((monomial (m - single i 1) : (a : R) → MvPolynomial σ R) (↑((m : (a : σ) → ℕ) i) : R)) n'
⊢ IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w
    ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((fun (i : σ →₀ ℕ) ↦ (single i 1 : Finsupp.{u_2, u_1} (σ →₀ ℕ) R)) m))
    n'

Tactic:
simp_rw [single_eq_monomial, pderiv_monomial, one_mul]

Premises used: MvPolynomial.single_eq_monomial, MvPolynomial.pderiv_monomial, one_mul
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
M : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n})) φ
h' : n' + w i = n
m : σ →₀ ℕ
hm : Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n} m
pos :
  ∀ (hi : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)),
    IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w
      ((monomial (m - single i 1) : (a : R) → MvPolynomial σ R) (↑((m : (a : σ) → ℕ) i) : R)) n'
neg :
  ∀ (hi : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)),
    IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w
      ((monomial (m - single i 1) : (a : R) → MvPolynomial σ R) (↑((m : (a : σ) → ℕ) i) : R)) n'
⊢ IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w
    ((monomial (m - single i 1) : (a : R) → MvPolynomial σ R) (↑((m : (a : σ) → ℕ) i) : R)) n'

Tactic:
by_cases hi : m i = 0

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
M : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n})) φ
h' : n' + w i = n
m : σ →₀ ℕ
hm : Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n} m
hi : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
pos : IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w 0 n'
⊢ IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w
    ((monomial (m - single i 1) : (a : R) → MvPolynomial σ R) (↑((m : (a : σ) → ℕ) i) : R)) n'

Tactic:
rw [hi, Nat.cast_zero, monomial_zero]

Premises used: MvPolynomial.monomial_zero, Nat.cast_zero
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
M : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n})) φ
h' : n' + w i = n
m : σ →₀ ℕ
hm : Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n} m
hi : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w 0 n'

Tactic:
apply isWeightedHomogeneous_zero

Premises used: MvPolynomial.isWeightedHomogeneous_zero
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
M : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n})) φ
h' : n' + w i = n
m : σ →₀ ℕ
hm : Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n} m
hi : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w
    ((monomial (m - single i 1) : (a : R) → MvPolynomial σ R) (↑((m : (a : σ) → ℕ) i) : R)) n'

Tactic:
isWeightedHomogeneous_monomial ..

Premises used: MvPolynomial.isWeightedHomogeneous_monomial
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
M : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n})) φ
h' : n' + w i = n
m : σ →₀ ℕ
hm : Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n} m
hi : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
neg : (weight w : (a : σ →₀ ℕ) → M) (m - single i 1) = n'
⊢ IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w
    ((monomial (m - single i 1) : (a : R) → MvPolynomial σ R) (↑((m : (a : σ) → ℕ) i) : R)) n'

Tactic:
convert! isWeightedHomogeneous_monomial ..

Premises used: MvPolynomial.isWeightedHomogeneous_monomial
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
M : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n})) φ
h' : n' + w i = n
m : σ →₀ ℕ
hm : Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n} m
hi : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
neg : HAdd.hAdd (α := M) ((weight w : (a : σ →₀ ℕ) → M) (m - single i 1) : M) (w i) = n' + w i
neg₁ : HAdd.hAdd (α := M) ((weight w : (a : σ →₀ ℕ) → M) (m - single i 1) : M) (w i) = n
neg₂ : HAdd.hAdd (α := M) ((weight w : (a : σ →₀ ℕ) → M) (m - single i 1) : M) (w i) = (weight w : (a : σ →₀ ℕ) → M) m
neg₃ neg₄ : Eq.{u_3 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) m : M) ((weight w : (a : σ →₀ ℕ) → M) m : M)
⊢ (weight w : (a : σ →₀ ℕ) → M) (m - single i 1) = n'

Tactic:
rw [← add_right_cancel_iff (a := w i), h', ← hm, weight_sub_single_add hi]

Premises used: add_right_cancel_iff, Finsupp.weight_sub_single_add
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
M : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n})) φ
h' : n' + w i = n
⊢ IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w 0 n'

Tactic:
apply isWeightedHomogeneous_zero

Premises used: MvPolynomial.isWeightedHomogeneous_zero