-- Mathlib/RingTheory/MvPolynomial/EulerIdentity.lean
protected lemma IsWeightedHomogeneous.pderiv [AddCancelCommMonoid M] {w : σ → M} {n n' : M} {i : σ}
    (h : φ.IsWeightedHomogeneous w n) (h' : n' + w i = n) :
    (pderiv i φ).IsWeightedHomogeneous w n'

Proof state:
case neg.convert_10
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
h' : n' + w i = n
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
hi : ¬m i = 0
⊢ (weight w) (m - single i 1) = n'

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

Result:
no goals

Proof state:
case refine_2
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
h' : n' + w i = n
⊢ IsWeightedHomogeneous w ((pderiv i) 0) n'

Tactic:
rw [map_zero]

Result:
case refine_2
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
h' : n' + w i = n
⊢ IsWeightedHomogeneous w 0 n'

Proof state:
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : IsWeightedHomogeneous w φ n
h' : n' + w i = n
⊢ IsWeightedHomogeneous w ((pderiv i) φ) n'

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

Result:
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
h' : n' + w i = n
⊢ IsWeightedHomogeneous w ((pderiv i) φ) n'

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

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

Result:
no goals

Proof state:
case refine_3
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
h' : n' + w i = 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 : IsWeightedHomogeneous w ((pderiv i) p) n'
hq : IsWeightedHomogeneous w ((pderiv i) q) n'
⊢ IsWeightedHomogeneous w ((pderiv i) p + (pderiv i) q) n'

Tactic:
exact hp.add hq

Result:
no goals

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

Tactic:
simp_rw [single_eq_monomial, pderiv_monomial, one_mul]

Result:
case refine_1.intro.intro
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
h' : n' + w i = n
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
⊢ IsWeightedHomogeneous w ((monomial (m - single i 1)) ↑(m i)) n'

Proof state:
case neg
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
h' : n' + w i = n
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
hi : ¬m i = 0
⊢ IsWeightedHomogeneous w ((monomial (m - single i 1)) ↑(m i)) n'

Tactic:
convert isWeightedHomogeneous_monomial ..

Result:
case neg.convert_10
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun i => single i 1) '' {d | (weight w) d = n})
h' : n' + w i = n
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
hi : ¬m i = 0
⊢ (weight w) (m - single i 1) = n'