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))
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))
simp only [pderiv_def, mkDerivation_monomial, Finsupp.smul_sum, smul_eq_mul, ← smul_mul_assoc,
  ← (monomial _).map_smul]
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

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

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))
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))
refine' (Finset.sum_eq_single i (fun j _ hne => _) fun hi => _).trans _
no goals
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
simp [Pi.single_eq_of_ne hne]
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
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
rw [Finsupp.not_mem_support_iff] at hi
no goals
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
simp [hi]
no goals
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))
simp