-- Mathlib/RingTheory/MvPolynomial/EulerIdentity.lean
theorem IsWeightedHomogeneous.sum_weight_X_mul_pderiv {w : σ → ℕ}
    (h : φ.IsWeightedHomogeneous w n) : ∑ i : σ, w i • (X i * pderiv i φ) = n • φ

Proof state:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : IsWeightedHomogeneous w φ n
⊢ ∑ i : σ, w i • (X i * (pderiv i) φ) = n • φ

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

Result:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
⊢ ∑ i : σ, w i • (X i * (pderiv i) φ) = n • φ

Proof state:
case refine_1.intro.intro
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
⊢ ∑ i : σ, w i • (X i * (pderiv i) ((fun i => single i 1) m)) = n • (fun i => single i 1) m

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

Result:
case refine_1.intro.intro
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
⊢ (∑ x : σ, m x * w x) • (monomial m) 1 = n • (monomial m) 1

Proof state:
case refine_1.intro.intro.e_a
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
⊢ ∑ x : σ, m x * w x = n

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

Result:
case refine_1.intro.intro.e_a.h
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
m : σ →₀ ℕ
hm : (m.sum fun i c => c • w i) = n
⊢ ∀ (i : σ), 0 • w i = 0

Proof state:
case refine_1
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
⊢ ∀ x ∈ (fun i => single i 1) '' {d | (weight w) d = n}, ∑ i : σ, w i • (X i * (pderiv i) x) = n • x

Tactic:
rintro _ ⟨m, hm, rfl⟩

Result:
case refine_1.intro.intro
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
⊢ ∑ i : σ, w i • (X i * (pderiv i) ((fun i => single i 1) m)) = n • (fun i => single i 1) m

Proof state:
case refine_3
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
p q : MvPolynomial σ R
x✝¹ : p ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
x✝ : q ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
hp : ∑ i : σ, w i • (X i * (pderiv i) p) = n • p
hq : ∑ i : σ, w i • (X i * (pderiv i) q) = n • q
⊢ ∑ i : σ, w i • (X i * (pderiv i) (p + q)) = n • (p + q)

Tactic:
simp_rw [map_add, left_distrib, smul_add, sum_add_distrib, hp, hq]

Result:
no goals

Proof state:
case refine_1.intro.intro.e_a.h
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
m : σ →₀ ℕ
hm : (m.sum fun i c => c • w i) = n
⊢ ∀ (i : σ), 0 • w i = 0

Tactic:
intro

Result:
case refine_1.intro.intro.e_a.h
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
m : σ →₀ ℕ
hm : (m.sum fun i c => c • w i) = n
i✝ : σ
⊢ 0 • w i✝ = 0

Proof state:
case refine_1.intro.intro
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
⊢ (∑ x : σ, m x * w x) • (monomial m) 1 = n • (monomial m) 1

Tactic:
congr

Result:
case refine_1.intro.intro.e_a
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
⊢ ∑ x : σ, m x * w x = n

Proof state:
case refine_2
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
⊢ ∑ i : σ, w i • (X i * (pderiv i) 0) = n • 0

Tactic:
simp

Result:
no goals

Proof state:
case refine_1.intro.intro.e_a.h
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
m : σ →₀ ℕ
hm : (m.sum fun i c => c • w i) = n
i✝ : σ
⊢ 0 • w i✝ = 0

Tactic:
apply zero_smul

Result:
no goals

Proof state:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
⊢ ∑ i : σ, w i • (X i * (pderiv i) φ) = n • φ

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

Result:
case refine_1
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
⊢ ∀ x ∈ (fun i => single i 1) '' {d | (weight w) d = n}, ∑ i : σ, w i • (X i * (pderiv i) x) = n • x

case refine_2
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
⊢ ∑ i : σ, w i • (X i * (pderiv i) 0) = n • 0

case refine_3
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
p q : MvPolynomial σ R
x✝¹ : p ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
x✝ : q ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
hp : ∑ i : σ, w i • (X i * (pderiv i) p) = n • p
hq : ∑ i : σ, w i • (X i * (pderiv i) q) = n • q
⊢ ∑ i : σ, w i • (X i * (pderiv i) (p + q)) = n • (p + q)

case refine_4
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h✝ : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
r : R
p : MvPolynomial σ R
x✝ : p ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
h : ∑ i : σ, w i • (X i * (pderiv i) p) = n • p
⊢ ∑ i : σ, w i • (X i * (pderiv i) (r • p)) = n • r • p

Proof state:
case refine_4
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h✝ : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
r : R
p : MvPolynomial σ R
x✝ : p ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
h : ∑ i : σ, w i • (X i * (pderiv i) p) = n • p
⊢ ∑ i : σ, w i • (X i * (pderiv i) (r • p)) = n • r • p

Tactic:
simp_rw [(pderiv _).map_smul, nsmul_eq_mul, mul_smul_comm, ← Finset.smul_sum, ← nsmul_eq_mul, h]

Result:
no goals