-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
ι : Type u_2
p : MvPolynomial (σ ⊕ ι) R
i : σ
C :
  ∀ (a : R),
    Eq (α := MvPolynomial σ (MvPolynomial ι R))
      ((pderiv i : (a : MvPolynomial σ (MvPolynomial ι R)) → MvPolynomial σ (MvPolynomial ι R))
          ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
            ((MvPolynomial.C : (a : R) → MvPolynomial (σ ⊕ ι) R) a)) :
        MvPolynomial σ (MvPolynomial ι R))
      ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
          ((pderiv (Sum.inl i) : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial (σ ⊕ ι) R)
            ((MvPolynomial.C : (a : R) → MvPolynomial (σ ⊕ ι) R) a)) :
        MvPolynomial σ (MvPolynomial ι R))
add :
  ∀ (p q : MvPolynomial (σ ⊕ ι) R),
    Eq (α := MvPolynomial σ (MvPolynomial ι R))
        ((pderiv i : (a : MvPolynomial σ (MvPolynomial ι R)) → MvPolynomial σ (MvPolynomial ι R))
            ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R)) p) :
          MvPolynomial σ (MvPolynomial ι R))
        ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
            ((pderiv (Sum.inl i) : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial (σ ⊕ ι) R) p) :
          MvPolynomial σ (MvPolynomial ι R)) →
      Eq (α := MvPolynomial σ (MvPolynomial ι R))
          ((pderiv i : (a : MvPolynomial σ (MvPolynomial ι R)) → MvPolynomial σ (MvPolynomial ι R))
              ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R)) q) :
            MvPolynomial σ (MvPolynomial ι R))
          ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
              ((pderiv (Sum.inl i) : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial (σ ⊕ ι) R) q) :
            MvPolynomial σ (MvPolynomial ι R)) →
        Eq (α := MvPolynomial σ (MvPolynomial ι R))
          ((pderiv i : (a : MvPolynomial σ (MvPolynomial ι R)) → MvPolynomial σ (MvPolynomial ι R))
              ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R)) (p + q)) :
            MvPolynomial σ (MvPolynomial ι R))
          ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
              ((pderiv (Sum.inl i) : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial (σ ⊕ ι) R) (p + q)) :
            MvPolynomial σ (MvPolynomial ι R))
mul_X :
  ∀ (p : MvPolynomial (σ ⊕ ι) R) (n : σ ⊕ ι),
    Eq (α := MvPolynomial σ (MvPolynomial ι R))
        ((pderiv i : (a : MvPolynomial σ (MvPolynomial ι R)) → MvPolynomial σ (MvPolynomial ι R))
            ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R)) p) :
          MvPolynomial σ (MvPolynomial ι R))
        ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
            ((pderiv (Sum.inl i) : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial (σ ⊕ ι) R) p) :
          MvPolynomial σ (MvPolynomial ι R)) →
      Eq (α := MvPolynomial σ (MvPolynomial ι R))
        ((pderiv i : (a : MvPolynomial σ (MvPolynomial ι R)) → MvPolynomial σ (MvPolynomial ι R))
            ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R)) (p * X n)) :
          MvPolynomial σ (MvPolynomial ι R))
        ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
            ((pderiv (Sum.inl i) : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial (σ ⊕ ι) R) (p * X n)) :
          MvPolynomial σ (MvPolynomial ι R))
⊢ Eq (α := MvPolynomial σ (MvPolynomial ι R))
    ((pderiv i : (a : MvPolynomial σ (MvPolynomial ι R)) → MvPolynomial σ (MvPolynomial ι R))
        ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R)) p) :
      MvPolynomial σ (MvPolynomial ι R))
    ((sumToIter R σ ι : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial σ (MvPolynomial ι R))
        ((pderiv (Sum.inl i) : (a : MvPolynomial (σ ⊕ ι) R) → MvPolynomial (σ ⊕ ι) R) p) :
      MvPolynomial σ (MvPolynomial ι R))

Tactic:
induction p using MvPolynomial.induction_on with
  | C a => simp
  | add p q _ _ => simp_all
  | mul_X p n _ => cases n <;> simp_all [pderiv_X, Pi.single_apply, apply_ite]

Premises used: Pi.single_apply, MvPolynomial.pderiv_X, apply_ite, MvPolynomial.induction_on, MvPolynomial.C