-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
S : Type u_1
τ : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
p : MvPolynomial (σ ⊕ τ) R
f : τ → S
j : σ
C :
  ∀ (a : R),
    Eq (α := MvPolynomial σ S)
      ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
            (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
          ((pderiv (Sum.inl j) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial (σ ⊕ τ) R)
            ((MvPolynomial.C : (a : R) → MvPolynomial (σ ⊕ τ) R) a)) :
        MvPolynomial σ S)
      ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
          ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
              (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            ((MvPolynomial.C : (a : R) → MvPolynomial (σ ⊕ τ) R) a)) :
        MvPolynomial σ S)
add :
  ∀ (p q : MvPolynomial (σ ⊕ τ) R)
    (hp :
      Eq (α := MvPolynomial σ S)
        ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
              (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            ((pderiv (Sum.inl j) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial (σ ⊕ τ) R) p) :
          MvPolynomial σ S)
        ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
            ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
                (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
              p) :
          MvPolynomial σ S))
    (hq :
      Eq (α := MvPolynomial σ S)
        ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
              (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            ((pderiv (Sum.inl j) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial (σ ⊕ τ) R) q) :
          MvPolynomial σ S)
        ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
            ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
                (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
              q) :
          MvPolynomial σ S)),
    Eq (α := MvPolynomial σ S)
      ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
            (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
          ((pderiv (Sum.inl j) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial (σ ⊕ τ) R) (p + q)) :
        MvPolynomial σ S)
      ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
          ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
              (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            (p + q)) :
        MvPolynomial σ S)
mul_X :
  ∀ (p : MvPolynomial (σ ⊕ τ) R) (q : σ ⊕ τ)
    (h :
      Eq (α := MvPolynomial σ S)
        ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
              (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            ((pderiv (Sum.inl j) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial (σ ⊕ τ) R) p) :
          MvPolynomial σ S)
        ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
            ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
                (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
              p) :
          MvPolynomial σ S)),
    Eq (α := MvPolynomial σ S)
      ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
            (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
          ((pderiv (Sum.inl j) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial (σ ⊕ τ) R) (p * X q)) :
        MvPolynomial σ S)
      ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
          ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
              (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            (p * X q)) :
        MvPolynomial σ S)
⊢ Eq (α := MvPolynomial σ S)
    ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
          (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
        ((pderiv (Sum.inl j) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial (σ ⊕ τ) R) p) :
      MvPolynomial σ S)
    ((pderiv j : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
            (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
          p) :
      MvPolynomial σ S)

Tactic:
induction p using MvPolynomial.induction_on with
  | C a => simp
  | add p q hp hq => simp [hp, hq]
  | mul_X p q h =>
    simp only [Derivation.leibniz, pderiv_X, smul_eq_mul, map_add, map_mul, aeval_X, h]
    cases q <;> simp [Pi.single_apply]

Premises used: MvPolynomial.aeval_X, Pi.single_apply, MvPolynomial.pderiv_X, map_add, MvPolynomial.induction_on, Derivation.leibniz, map_mul, smul_eq_mul, MvPolynomial.C