awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
n : σ →₀ ℕ
h : n ∈ p.support
rw :
  Eq (α := Finsupp.{u, u_2} (σ →₀ ℕ) S)
    (Finsupp.mapRange (⇑f : (a : R) → S) ⋯ ((monomial n : (a : R) → MvPolynomial σ R) (coeff n p)))
    ((monomial n : (a : S) → MvPolynomial σ S) ((f : (a : R) → S) (coeff n p)))
rw₁ :
  Eq (α := Finsupp.{u, u_2} (σ →₀ ℕ) S) (Finsupp.mapRange (⇑f : (a : R) → S) ⋯ (Finsupp.single n (coeff n p)))
    ((monomial n : (a : S) → MvPolynomial σ S) ((f : (a : R) → S) (coeff n p)))
rw₂ :
  Eq (α := Finsupp.{u, u_2} (σ →₀ ℕ) S) (Finsupp.single n ((f : (a : R) → S) (coeff n p)) : Finsupp.{u, u_2} (σ →₀ ℕ) S)
    ((monomial n : (a : S) → MvPolynomial σ S) ((f : (a : R) → S) (coeff n p)) : MvPolynomial σ S)
⊢ Eq (α := Finsupp.{u, u_2} (σ →₀ ℕ) S)
    (Finsupp.mapRange (⇑f : (a : R) → S) ⋯ ((monomial n : (a : R) → MvPolynomial σ R) (coeff n p)))
    ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) ((monomial n : (a : R) → MvPolynomial σ R) (coeff n p)))
have rw₃ : Eq (α := Finsupp.{u, u_2} (σ →₀ ℕ) S)
  ((monomial n : (a : S) → MvPolynomial σ S) ((f : (a : R) → S) (coeff n p)) : MvPolynomial σ S)
  ((monomial n : (a : S) → MvPolynomial σ S) ((f : (a : R) → S) (coeff n p)) : MvPolynomial σ S)
Tactic: rw [map_monomial, ← single_eq_monomial, Finsupp.mapRange_single, single_eq_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
s : Set (σ →₀ ℕ)
m : σ →₀ ℕ
r : R
⊢ Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
      ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    m ∈ s ∨ r = 0
have pos : r = 0 →
  (Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
      ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    m ∈ s ∨ r = 0)
Tactic: by_cases r = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
s : Set (σ →₀ ℕ)
m : σ →₀ ℕ
r : R
pos :
  r = 0 →
    (Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
        ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
      m ∈ s ∨ r = 0)
⊢ Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
      ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    m ∈ s ∨ r = 0
have neg : ¬r = 0 →
  (Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
      ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    m ∈ s ∨ r = 0)
Tactic: by_cases r = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
s : Set (σ →₀ ℕ)
m : σ →₀ ℕ
r : R
⊢ Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
      ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    m ∈ s ∨ r = 0
have pos : r = 0 →
  (Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
      ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    m ∈ s ∨ r = 0)
Tactic: classical
  by_cases r = 0 <;> simp [mem_restrictSupport_iff, support_monomial, *]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
s : Set (σ →₀ ℕ)
m : σ →₀ ℕ
r : R
pos :
  r = 0 →
    (Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
        ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
      m ∈ s ∨ r = 0)
⊢ Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
      ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    m ∈ s ∨ r = 0
have neg : ¬r = 0 →
  (Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
      ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    m ∈ s ∨ r = 0)
Tactic: classical
  by_cases r = 0 <;> simp [mem_restrictSupport_iff, support_monomial, *]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (restrictSupport R 0) 1
have a : LE.le (α := Submodule R (MvPolynomial σ R)) (restrictSupport R 0) 1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
a : LE.le (α := Submodule R (MvPolynomial σ R)) (restrictSupport R 0) 1
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (restrictSupport R 0) 1
have a₁ : LE.le (α := Submodule R (MvPolynomial σ R)) 1 (restrictSupport R 0)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
⊢ LE.le (α := Submodule R (MvPolynomial σ R)) (restrictSupport R 0) 1
have a : Subset.{u} (α := Set (σ →₀ ℕ)) 0
  ((fun (x : σ →₀ ℕ) ↦ (monomial x : (a : R) → MvPolynomial σ R) 1) ⁻¹' (↑1 : Set (MvPolynomial σ R)))
Tactic: rw [restrictSupport_eq_span, Submodule.span_le, Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (restrictSupport R 0) 1
have a : LE.le (α := Submodule R (MvPolynomial σ R)) (restrictSupport R 0) 1
Tactic: classical
  apply le_antisymm
  · rw [restrictSupport_eq_span, Submodule.span_le, Set.image_subset_iff]
    simpa using ⟨1, by simp⟩
  · rintro _ ⟨x, rfl⟩
    simp [mem_restrictSupport_iff, Set.subset_def, coeff_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
a : LE.le (α := Submodule R (MvPolynomial σ R)) (restrictSupport R 0) 1
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (restrictSupport R 0) 1
have a₁ : LE.le (α := Submodule R (MvPolynomial σ R)) 1 (restrictSupport R 0)
Tactic: classical
  apply le_antisymm
  · rw [restrictSupport_eq_span, Submodule.span_le, Set.image_subset_iff]
    simpa using ⟨1, by simp⟩
  · rintro _ ⟨x, rfl⟩
    simp [mem_restrictSupport_iff, Set.subset_def, coeff_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (restrictSupport R univ) ⊤
have h : ∀ (x : MvPolynomial σ R),
  Membership.mem (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R univ) x ↔
    Membership.mem (γ := Submodule R (MvPolynomial σ R)) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
n : ℕ
s : Set (σ →₀ ℕ)
⊢ restrictSupport R (n • s) = HPow.hPow (α := Submodule R (MvPolynomial σ R)) (restrictSupport R s) n
have zero : restrictSupport R (HSMul.hSMul (α := ℕ) 0 s) =
  HPow.hPow (α := Submodule R (MvPolynomial σ R)) (β := ℕ) (restrictSupport R s) 0
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
n : ℕ
s : Set (σ →₀ ℕ)
zero :
  restrictSupport R (HSMul.hSMul (α := ℕ) 0 s) =
    HPow.hPow (α := Submodule R (MvPolynomial σ R)) (β := ℕ) (restrictSupport R s) 0
⊢ restrictSupport R (n • s) = HPow.hPow (α := Submodule R (MvPolynomial σ R)) (restrictSupport R s) n
have succ : ∀ (n : ℕ),
  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: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (hypothesis)
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
⊢ m ∈ s
have hm₁ : ¬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
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
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
⊢ m ∈ s
have 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
Tactic: obtain ⟨⟨i, j⟩, hij, e⟩ := Finset.exists_ne_zero_of_sum_ne_zero hm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
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
⊢ m ∈ s
have 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
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))
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
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
⊢ m ∈ s
have 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
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))
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
m : ℕ
p : MvPolynomial σ R
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R)) (restrictTotalDegree σ R m) p ↔ p.totalDegree ≤ m
have rw : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (restrictTotalDegree σ R m) p ↔
  ∀ b ∈ p.support, (b.sum fun (x : σ) (e : ℕ) ↦ e) ≤ m
Tactic: rw [totalDegree, Finset.sup_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
inst_1 : DecidableEq σ
p : MvPolynomial σ R
n : ℕ
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R)) (restrictDegree σ R n) p ↔
    ∀ (i : σ), Multiset.count i p.degrees ≤ n
have simp : (∀ s ∈ p.support, ∀ (i : σ), (s : (a : σ) → ℕ) i ≤ n) ↔ ∀ (i : σ), ∀ b ∈ p.support, (b : (a : σ) → ℕ) i ≤ n
Tactic: simp only [mem_restrictDegree, degrees_def, Multiset.count_finset_sup, Finsupp.count_toMultiset,
    Finset.sup_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (hypothesis)
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)
⊢ Finite.{u + 1} (↑{s : σ →₀ ℕ | (s.sum fun (x : σ) (e : ℕ) ↦ e) ≤ N} : Type u)
have this₁ : Set.Finite.{u} (α := σ →₀ ℕ) {f : σ →₀ ℕ | ∀ (a : σ), (f : (a : σ) → ℕ) a ≤ N}
Tactic: rw [Set.finite_coe_iff] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (hypothesis)
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
⊢ IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) n'
have h₁ : 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
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
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'
have 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'
Tactic: refine Submodule.span_induction ?_ ?_ (fun p q _ _ hp hq ↦ ?_) (fun r p _ h ↦ ?_) h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
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'
⊢ IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) n'
have refine_2 : IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) 0) n'
Tactic: refine Submodule.span_induction ?_ ?_ (fun p q _ _ hp hq ↦ ?_) (fun r p _ h ↦ ?_) h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
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'
⊢ IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) n'
have 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'
Tactic: refine Submodule.span_induction ?_ ?_ (fun p q _ _ hp hq ↦ ?_) (fun r p _ h ↦ ?_) h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
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'
⊢ IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) n'
have 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'
Tactic: refine Submodule.span_induction ?_ ?_ (fun p q _ _ hp hq ↦ ?_) (fun r p _ h ↦ ?_) h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
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
⊢ 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'
have 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'
Tactic: simp_rw [single_eq_monomial, pderiv_monomial, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
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
⊢ IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w
    ((monomial (m - single i 1) : (a : R) → MvPolynomial σ R) (↑((m : (a : σ) → ℕ) i) : R)) n'
have 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'
Tactic: by_cases hi : m i = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
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'
⊢ IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w
    ((monomial (m - single i 1) : (a : R) → MvPolynomial σ R) (↑((m : (a : σ) → ℕ) i) : R)) n'
have 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'
Tactic: by_cases hi : m i = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
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'
have pos : IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w 0 n'
Tactic: rw [hi, Nat.cast_zero, monomial_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
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'
have neg : (weight w : (a : σ →₀ ℕ) → M) (m - single i 1) = n'
Tactic: convert! isWeightedHomogeneous_monomial ..