awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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'
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'
⊢ IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (p + q)) n'

Tactic:
rw [map_add]

Premises used: map_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
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 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:
hp.add hq

Premises used: MvPolynomial.IsWeightedHomogeneous.add, AddMonoidAlgebra
-- 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
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 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:
exact hp.add hq

Premises used: MvPolynomial.IsWeightedHomogeneous.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_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'
refine_4 :
  IsWeightedHomogeneous w
    (HSMul.hSMul (β := MvPolynomial σ R) r
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R))
    n'
⊢ IsWeightedHomogeneous.{u_1, u_3, u_2} (R := R) w ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (r • p)) n'

Tactic:
rw [(pderiv i).map_smul]

Premises used: MvPolynomial.pderiv, Derivation.map_smul
-- 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_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 w
    (HSMul.hSMul (β := MvPolynomial σ R) r
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R))
    n'

Tactic:
(weightedHomogeneousSubmodule ..).smul_mem _ h

Premises used: MvPolynomial.weightedHomogeneousSubmodule, Set.Mem, setOf, MvPolynomial.IsWeightedHomogeneous, Submodule.smul_mem
-- 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_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 w
    (HSMul.hSMul (β := MvPolynomial σ R) r
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R))
    n'

Tactic:
exact (weightedHomogeneousSubmodule ..).smul_mem _ h

Premises used: MvPolynomial.weightedHomogeneousSubmodule, Submodule.smul_mem
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
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)
succ :
  ∀ (n : ℕ) (h : φ.IsHomogeneous (n + 1)),
    IsHomogeneous.{u_2, u_1} (σ := σ) (R := R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) (n + 1 - 1)
⊢ IsHomogeneous.{u_2, u_1} (σ := σ) (R := R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) (n - 1)

Tactic:
obtain _ | n := n
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
i : σ
h : φ.IsHomogeneous 0
⊢ φ = (C : (a : R) → MvPolynomial σ R) (coeff 0 φ)

Tactic:
rw [← totalDegree_zero_iff_isHomogeneous, totalDegree_eq_zero_iff_eq_C] at h

Premises used: MvPolynomial.totalDegree_eq_zero_iff_eq_C, MvPolynomial.totalDegree_zero_iff_isHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
i : σ
h : φ = (C : (a : R) → MvPolynomial σ R) (coeff 0 φ)
zero : IsHomogeneous.{u_2, u_1} (σ := σ) (R := R) 0 (HSub.hSub (α := ℕ) 0 1)
⊢ IsHomogeneous.{u_2, u_1} (σ := σ) (R := R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)
    (HSub.hSub (α := ℕ) 0 1)

Tactic:
rw [h, pderiv_C]

Premises used: MvPolynomial.pderiv_C
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
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) 0 (HSub.hSub (α := ℕ) 0 1)

Tactic:
apply isHomogeneous_zero

Premises used: MvPolynomial.isHomogeneous_zero
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
i : σ
n : ℕ
h : φ.IsHomogeneous (n + 1)
⊢ IsHomogeneous.{u_2, u_1} (σ := σ) (R := R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) (n + 1 - 1)

Tactic:
IsWeightedHomogeneous.pderiv h rfl

Premises used: MvPolynomial.IsWeightedHomogeneous.pderiv, MvPolynomial.IsHomogeneous, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
i : σ
n : ℕ
h : φ.IsHomogeneous (n + 1)
⊢ IsHomogeneous.{u_2, u_1} (σ := σ) (R := R) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) (n + 1 - 1)

Tactic:
exact IsWeightedHomogeneous.pderiv h rfl

Premises used: MvPolynomial.IsWeightedHomogeneous.pderiv, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h : IsWeightedHomogeneous w φ n
⊢ 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

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
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 • φ

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
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)
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
⊢ ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → 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
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
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)
⊢ ∑ 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)

Tactic:
simp_rw [single_eq_monomial, X_mul_pderiv_monomial, smul_smul, ← sum_smul, mul_comm (w _)]

Premises used: Finset.sum_smul, MvPolynomial.X_mul_pderiv_monomial, MvPolynomial.single_eq_monomial, smul_smul, mul_comm
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
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
refine_1 : ∑ x : σ, HMul.hMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = n
⊢ 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:
congr
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
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
refine_1 : ∀ (hm : (m.sum fun (i : σ) (c : ℕ) ↦ c • w i) = n) (i : σ), HSMul.hSMul (α := ℕ) 0 (w i) = 0
⊢ ∑ x : σ, HMul.hMul (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (w x) = n

Tactic:
rwa [Set.mem_setOf, weight_apply, sum_fintype] at hm

Premises used: Finsupp.sum_fintype, Set.mem_setOf, Finsupp.weight_apply
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
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 : (m.sum fun (i : σ) (c : ℕ) ↦ c • w i) = n
i : σ
⊢ HSMul.hSMul (α := ℕ) 0 (w i) = 0

Tactic:
apply zero_smul

Premises used: zero_smul
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
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) (X i) ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) 0) =
    HSMul.hSMul (β := MvPolynomial σ R) n 0

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h_1 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = 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 : σ →₀ ℕ) → ℕ) 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
refine_4 :
  ∑ x : σ,
      w x •
        (X x *
          HSMul.hSMul (β := MvPolynomial σ R) r
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
    n • r • p
refine_4₁ :
  ∑ x : σ,
      (↑(w x) : MvPolynomial σ R) *
        (X x *
          HSMul.hSMul (β := MvPolynomial σ R) r
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
    (↑n : MvPolynomial σ R) * r • p
refine_4₂ :
  ∑ x : σ,
      r •
        ((↑(w x) : MvPolynomial σ R) *
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
    r • ((↑n : MvPolynomial σ R) * p)
refine_4₃ :
  HSMul.hSMul (β := MvPolynomial σ R) r
      (∑ x : σ,
        (↑(w x) : MvPolynomial σ R) *
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
    r • ((↑n : MvPolynomial σ R) * p)
refine_4₄ :
  HSMul.hSMul (β := MvPolynomial σ R) r
      (∑ x : σ,
        w x •
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
    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:
simp_rw [(pderiv _).map_smul, nsmul_eq_mul, mul_smul_comm, ← Finset.smul_sum, ← nsmul_eq_mul, h]

Premises used: MvPolynomial.pderiv, Finset.smul_sum, Derivation.map_smul, nsmul_eq_mul, mul_smul_comm
-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
h : φ.IsHomogeneous n
simp_rw :
  Eq (α := MvPolynomial σ R)
    (∑ i : σ,
      HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R))
    (∑ i : σ,
      HSMul.hSMul (α := ℕ) (1 i)
        (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)))
simp_rw₁ :
  Eq (α := MvPolynomial σ R)
    (∑ i : σ,
      HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R))
    (∑ x : σ,
      HSMul.hSMul (α := ℕ) 1
        (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)))
⊢ ∑ i : σ,
      HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R) =
    n • φ

Tactic:
simp_rw [← h.sum_weight_X_mul_pderiv, Pi.one_apply, one_smul]

Premises used: Pi.one_apply, MvPolynomial.IsWeightedHomogeneous.sum_weight_X_mul_pderiv, one_smul
-- Module: Mathlib.RingTheory.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : MvPolynomial σ R
x : σ →₀ ℕ
x_1 : R
⊢ (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) ((monomial x : (a : R) → MvPolynomial σ R) x_1)) =
    HPow.hPow (α := MvPolynomial σ R) ((monomial x : (a : R) → MvPolynomial σ R) x_1 : MvPolynomial σ R) p

Tactic:
simp [monomial_pow, frobenius]

Premises used: frobenius, MvPolynomial.monomial_pow
-- Module: Mathlib.RingTheory.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f x x_1 : MvPolynomial σ R
ha :
  (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x) =
    x ^ p
hb :
  (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1) =
    x_1 ^ p
rw :
  (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x : MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1 : MvPolynomial σ R)) =
    (x + x_1) ^ p
rw₁ :
  HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x) :
        MvPolynomial σ R)
      ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1) :
        MvPolynomial σ R) =
    (x + x_1) ^ p
rw₂ :
  HAdd.hAdd (β := MvPolynomial σ R) (x ^ p)
      ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1) :
        MvPolynomial σ R) =
    (x + x_1) ^ p
rw₃ : x ^ p + x_1 ^ p = (x + x_1) ^ p
rw₄ rw₅ : x ^ p + x_1 ^ p = x ^ p + x_1 ^ p
⊢ (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) (x + x_1)) =
    (x + x_1) ^ p

Tactic:
rw [map_add, map_add, ha, hb, add_pow_expChar]

Premises used: map_add, add_pow_expChar