awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ)
⊢ (weight w : (a : σ →₀ ℕ) → M) (m - single i 1) = n'
have neg : HAdd.hAdd (α := M) ((weight w : (a : σ →₀ ℕ) → M) (m - single i 1) : M) (w i) = n' + w i
Tactic: rw [← add_right_cancel_iff (a := w i), h', ← hm, weight_sub_single_add hi]
-- 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 : ℕ)
neg : HAdd.hAdd (α := M) ((weight w : (a : σ →₀ ℕ) → M) (m - single i 1) : M) (w i) = n' + w i
⊢ (weight w : (a : σ →₀ ℕ) → M) (m - single i 1) = n'
have neg₁ : HAdd.hAdd (α := M) ((weight w : (a : σ →₀ ℕ) → M) (m - single i 1) : M) (w i) = n
Tactic: rw [← add_right_cancel_iff (a := w i), h', ← hm, weight_sub_single_add hi]
-- 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 : ℕ)
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
⊢ (weight w : (a : σ →₀ ℕ) → M) (m - single i 1) = n'
have neg₂ : HAdd.hAdd (α := M) ((weight w : (a : σ →₀ ℕ) → M) (m - single i 1) : M) (w i) = (weight w : (a : σ →₀ ℕ) → M) m
Tactic: rw [← add_right_cancel_iff (a := w i), h', ← hm, weight_sub_single_add hi]
-- 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 : ℕ)
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
⊢ (weight w : (a : σ →₀ ℕ) → M) (m - single i 1) = n'
have neg₃ : Eq.{u_3 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) m : M) ((weight w : (a : σ →₀ ℕ) → M) m : M)
Tactic: rw [← add_right_cancel_iff (a := w i), h', ← hm, weight_sub_single_add hi]
-- 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
p q : MvPolynomial σ R
h_1 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = n})) p
h_2 :
  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'
have refine_3 : IsWeightedHomogeneous w
  (HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
    ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R))
  n'
Tactic: rw [map_add]
-- 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_1 :
  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
r : R
p : MvPolynomial σ R
h_2 :
  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'
have refine_4 : IsWeightedHomogeneous w
  (HSMul.hSMul (β := MvPolynomial σ R) r ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R))
  n'
Tactic: rw [(pderiv i).map_smul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
i : σ
h : φ.IsHomogeneous n
⊢ IsHomogeneous.{u_2, u_1} (σ := σ) (R := R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) (n - 1)
have zero : ∀ (h : φ.IsHomogeneous 0),
  IsHomogeneous.{u_2, u_1} (σ := σ) (R := R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
    (HSub.hSub (α := ℕ) 0 1)
Tactic: obtain _ | n := n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
i : σ
h : φ.IsHomogeneous n
zero :
  ∀ (h : φ.IsHomogeneous 0),
    IsHomogeneous.{u_2, u_1} (σ := σ) (R := R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
      (HSub.hSub (α := ℕ) 0 1)
⊢ IsHomogeneous.{u_2, u_1} (σ := σ) (R := R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) (n - 1)
have succ : ∀ (n : ℕ) (h : φ.IsHomogeneous (n + 1)),
  IsHomogeneous.{u_2, u_1} (σ := σ) (R := R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) (n + 1 - 1)
Tactic: obtain _ | n := n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (hypothesis)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
i : σ
h : φ.IsHomogeneous 0
⊢ IsHomogeneous.{u_2, u_1} (σ := σ) (R := R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
    (HSub.hSub (α := ℕ) 0 1)
have h₁ : φ = (C : (a : R) → MvPolynomial σ R) (coeff 0 φ)
Tactic: rw [← totalDegree_zero_iff_isHomogeneous, totalDegree_eq_zero_iff_eq_C] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
i : σ
h : φ = (C : (a : R) → MvPolynomial σ R) (coeff 0 φ)
⊢ IsHomogeneous.{u_2, u_1} (σ := σ) (R := R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
    (HSub.hSub (α := ℕ) 0 1)
have zero : IsHomogeneous.{u_2, u_1} (σ := σ) (R := R) 0 (HSub.hSub (α := ℕ) 0 1)
Tactic: rw [h, pderiv_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (hypothesis)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h : IsWeightedHomogeneous w φ n
⊢ ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → 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 : σ →₀ ℕ) → ℕ) d = n})) φ
Tactic: rw [← mem_weightedHomogeneousSubmodule, weightedHomogeneousSubmodule_eq_finsupp_supported,
    supported_eq_span_single] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) φ
⊢ ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → 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 : σ →₀ ℕ) → ℕ) d = n}) x),
  ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) x : MvPolynomial σ R) =
    n • x
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
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) φ
refine_1 :
  ∀ (x : MvPolynomial σ R)
    (h :
      Membership.mem (γ := Set (MvPolynomial σ R))
        ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n}) x),
    ∑ i : σ,
        w i •
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
            ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) x : MvPolynomial σ R) =
      n • x
⊢ ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R) =
    n • φ
have refine_2 : ∑ i : σ, w i • HMul.hMul (α := MvPolynomial σ R) (X i) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) 0) =
  HSMul.hSMul (β := MvPolynomial σ R) n 0
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
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) φ
refine_1 :
  ∀ (x : MvPolynomial σ R)
    (h :
      Membership.mem (γ := Set (MvPolynomial σ R))
        ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n}) x),
    ∑ i : σ,
        w i •
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
            ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) x : MvPolynomial σ R) =
      n • x
refine_2 :
  ∑ i : σ, w i • HMul.hMul (α := MvPolynomial σ R) (X i) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) 0) =
    HSMul.hSMul (β := MvPolynomial σ R) n 0
⊢ ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → 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 : σ →₀ ℕ) → ℕ) d = n})) p →
    Membership.mem (γ := Submodule R (MvPolynomial σ R))
        (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) q →
      ∀
        (hp :
          ∑ i : σ,
              w i •
                HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                  ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) =
            n • p)
        (hq :
          ∑ i : σ,
              w i •
                HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                  ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R) =
            n • q),
        ∑ i : σ,
            w i •
              HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (p + q) : MvPolynomial σ R) =
          n • (p + q)
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
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) φ
refine_1 :
  ∀ (x : MvPolynomial σ R)
    (h :
      Membership.mem (γ := Set (MvPolynomial σ R))
        ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n}) x),
    ∑ i : σ,
        w i •
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
            ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) x : MvPolynomial σ R) =
      n • x
refine_2 :
  ∑ i : σ, w i • HMul.hMul (α := MvPolynomial σ R) (X i) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) 0) =
    HSMul.hSMul (β := MvPolynomial σ R) n 0
refine_3 :
  ∀ (p q : MvPolynomial σ R),
    Membership.mem (γ := Submodule R (MvPolynomial σ R))
        (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) p →
      Membership.mem (γ := Submodule R (MvPolynomial σ R))
          (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) q →
        ∀
          (hp :
            ∑ i : σ,
                w i •
                  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                    ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) =
              n • p)
          (hq :
            ∑ i : σ,
                w i •
                  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                    ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R) =
              n • q),
          ∑ i : σ,
              w i •
                HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                  ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (p + q) : MvPolynomial σ R) =
            n • (p + q)
⊢ ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → 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 : σ →₀ ℕ) → ℕ) d = n})) p →
    ∀
      (h :
        ∑ i : σ,
            w i •
              HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
                ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) =
          n • p),
      ∑ i : σ,
          w i •
            HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
              ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (r • p) : MvPolynomial σ R) =
        n • r • p
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
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) φ
m : σ →₀ ℕ
hm : Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n} m
⊢ ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((fun (i : σ →₀ ℕ) ↦ (single i 1 : Finsupp.{u_2, u_1} (σ →₀ ℕ) R)) m)) =
    HSMul.hSMul (β := MvPolynomial σ R) n ((fun (i : σ →₀ ℕ) ↦ (single i 1 : Finsupp.{u_2, u_1} (σ →₀ ℕ) R)) m)
have refine_1 : HSMul.hSMul (α := ℕ) (β := MvPolynomial σ R) (∑ x : σ, HMul.hMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x))
    ((monomial m : (a : R) → MvPolynomial σ R) 1) =
  HSMul.hSMul (β := MvPolynomial σ R) n ((monomial m : (a : R) → MvPolynomial σ R) 1)
Tactic: simp_rw [single_eq_monomial, X_mul_pderiv_monomial, smul_smul, ← sum_smul, mul_comm (w _)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) φ
m : σ →₀ ℕ
hm : Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n} m
⊢ HSMul.hSMul (α := ℕ) (β := MvPolynomial σ R) (∑ x : σ, HMul.hMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x))
      ((monomial m : (a : R) → MvPolynomial σ R) 1) =
    HSMul.hSMul (β := MvPolynomial σ R) n ((monomial m : (a : R) → MvPolynomial σ R) 1)
have refine_1 : ∑ x : σ, HMul.hMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = n
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) φ
m : σ →₀ ℕ
hm : Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n} m
⊢ ∑ x : σ, HMul.hMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = n
have refine_1 : ∀ (hm : (m.sum fun (i : σ) (c : ℕ) ↦ c • w i) = n) (i : σ), HSMul.hSMul (α := ℕ) 0 (w i) = 0
Tactic: rwa [Set.mem_setOf, weight_apply, sum_fintype] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) φ
p q : MvPolynomial σ R
h_1 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) p
h_2 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) q
hp :
  ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) =
    n • p
hq :
  ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R) =
    n • q
⊢ ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (p + q) : MvPolynomial σ R) =
    n • (p + q)
have refine_3 : ∑ x : σ,
    w x •
      (X x *
        HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) =
  n • (p + q)
Tactic: simp_rw [map_add, left_distrib, smul_add, sum_add_distrib, hp, hq]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) φ
p q : MvPolynomial σ R
h_1 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) p
h_2 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) q
hp :
  ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) =
    n • p
hq :
  ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R) =
    n • q
refine_3 :
  ∑ x : σ,
      w x •
        (X x *
          HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) =
    n • (p + q)
⊢ ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (p + q) : MvPolynomial σ R) =
    n • (p + q)
have refine_3₁ : ∑ x : σ,
    w x •
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) +
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) =
  n • (p + q)
Tactic: simp_rw [map_add, left_distrib, smul_add, sum_add_distrib, hp, hq]