-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst : CommSemiring R
i : σ
simp :
  Eq (α := MvPolynomial σ R)
    (s.sum fun (a_1 : σ) (b : ℕ) ↦
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
          (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R) :
      MvPolynomial σ R)
    ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)
refine_1 :
  ∀ j ∈ s.support,
    ∀ (hne : j ≠ i),
      Eq (α := MvPolynomial σ R)
        ((fun (a_1 : σ) (b : ℕ) ↦
            HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
              ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
              (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R))
          j ((s : (a : σ) → ℕ) j))
        0
refine_2 :
  ∀ (hi : i ∉ s.support),
    Eq (α := MvPolynomial σ R)
      ((fun (a_1 : σ) (b : ℕ) ↦
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
            ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
            (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R))
        i ((s : (a : σ) → ℕ) i))
      0
refine_3 :
  Eq (α := MvPolynomial σ R)
    ((fun (a_1 : σ) (b : ℕ) ↦
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
            ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
            (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R))
        i ((s : (a : σ) → ℕ) i) :
      MvPolynomial σ R)
    ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)
refine_2₁ :
  ∀ (hi : i ∉ s.support),
    Eq (α := MvPolynomial σ R)
      ((fun (a_1 : σ) (b : ℕ) ↦
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
            ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
            (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R))
        i ((s : (a : σ) → ℕ) i))
      0
refine_3₁ refine_3₂ :
  Eq (α := MvPolynomial σ R)
    ((fun (a_1 : σ) (b : ℕ) ↦
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
            ((monomial (s - single a_1 1) : (a : R) → MvPolynomial σ R) (a * (↑b : R)) : MvPolynomial σ R)
            (Pi.single (M := fun (a : σ) ↦ MvPolynomial σ R) i (1 : MvPolynomial σ R) a_1 : MvPolynomial σ R))
        i ((s : (a : σ) → ℕ) i) :
      MvPolynomial σ R)
    ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) a) :
      MvPolynomial σ R)
    ((monomial (s - single i 1) : (a : R) → MvPolynomial σ R) (a * (↑((s : (a : σ) → ℕ) i) : R)) : MvPolynomial σ R)

Tactic:
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.notMem_support_iff] at hi; simp [hi]
  · simp

Premises used: Finsupp.notMem_support_iff, MvPolynomial.monomial, smul_mul_assoc, MvPolynomial.pderiv_def, Finset.sum_eq_single, MvPolynomial.mkDerivation_monomial, LinearMap.map_smul, Finsupp.smul_sum, smul_eq_mul, Eq.trans