[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
⊢ pderiv i = mkDerivation R (Pi.single i 1)
[PROOFSTEP]
unfold pderiv
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
⊢ mkDerivation R (Pi.single i 1) = mkDerivation R (Pi.single i 1)
[PROOFSTEP]
congr!
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
⊢ ↑(pderiv i) (↑(monomial s) a) = ↑(monomial (s - single i 1)) (a * ↑(↑s i))
[PROOFSTEP]
classical
simp only [pderiv_def, mkDerivation_monomial, Finsupp.smul_sum, smul_eq_mul, ← smul_mul_assoc, ← (monomial _).map_smul]
refine' (Finset.sum_eq_single i (fun j _ hne => _) fun hi => _).trans _
· simp [Pi.single_eq_of_ne hne]
· rw [Finsupp.not_mem_support_iff] at hi ; simp [hi]
· simp
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
⊢ ↑(pderiv i) (↑(monomial s) a) = ↑(monomial (s - single i 1)) (a * ↑(↑s i))
[PROOFSTEP]
simp only [pderiv_def, mkDerivation_monomial, Finsupp.smul_sum, smul_eq_mul, ← smul_mul_assoc, ← (monomial _).map_smul]
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
⊢ (sum s fun a_1 b => ↑(monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) =
    ↑(monomial (s - single i 1)) (a * ↑(↑s i))
[PROOFSTEP]
refine' (Finset.sum_eq_single i (fun j _ hne => _) fun hi => _).trans _
[GOAL]
case refine'_1
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i j : σ
x✝ : j ∈ s.support
hne : j ≠ i
⊢ (fun a_1 b => ↑(monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) j (↑s j) = 0
[PROOFSTEP]
simp [Pi.single_eq_of_ne hne]
[GOAL]
case refine'_2
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
hi : ¬i ∈ s.support
⊢ (fun a_1 b => ↑(monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) i (↑s i) = 0
[PROOFSTEP]
rw [Finsupp.not_mem_support_iff] at hi 
[GOAL]
case refine'_2
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
hi : ↑s i = 0
⊢ (fun a_1 b => ↑(monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) i (↑s i) = 0
[PROOFSTEP]
simp [hi]
[GOAL]
case refine'_3
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
⊢ (fun a_1 b => ↑(monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) i (↑s i) =
    ↑(monomial (s - single i 1)) (a * ↑(↑s i))
[PROOFSTEP]
simp
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i j : σ
⊢ ↑(pderiv i) (X j) = Pi.single i 1 j
[PROOFSTEP]
rw [pderiv_def, mkDerivation_X]
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
⊢ ↑(pderiv i) (X i) = 1
[PROOFSTEP]
classical simp
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
⊢ ↑(pderiv i) (X i) = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i j : σ
h : j ≠ i
⊢ ↑(pderiv i) (X j) = 0
[PROOFSTEP]
classical simp [h]
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i j : σ
h : j ≠ i
⊢ ↑(pderiv i) (X j) = 0
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
n : ℕ
⊢ ↑(pderiv i) (↑(monomial (single i n)) a) = ↑(monomial (single i (n - 1))) (a * ↑n)
[PROOFSTEP]
simp
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ ↑(pderiv i) (f * g) = ↑(pderiv i) f * g + f * ↑(pderiv i) g
[PROOFSTEP]
simp only [(pderiv i).leibniz f g, smul_eq_mul, mul_comm, add_comm]
[GOAL]
R : Type u
σ : Type v
a a' a₁ a₂ : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : MvPolynomial σ R
i : σ
⊢ ↑(pderiv i) (↑C a * f) = ↑C a * ↑(pderiv i) f
[PROOFSTEP]
rw [C_mul', Derivation.map_smul, C_mul']
