-- Module: Mathlib.Algebra.MvPolynomial.PDeriv
Goal:
R : Type u
σ : Type v
inst : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
C :
  ∀ (a : R),
    Eq (α := MvPolynomial τ R)
      ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        MvPolynomial τ R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        MvPolynomial τ R)
add :
  ∀ (p q : MvPolynomial σ R)
    (hp :
      Eq (α := MvPolynomial τ R)
        ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
            ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
          MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial τ R))
    (hq :
      Eq (α := MvPolynomial τ R)
        ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
            ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) q) :
          MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q) :
          MvPolynomial τ R)),
    Eq (α := MvPolynomial τ R)
      ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (p + q)) :
        MvPolynomial τ R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) (p + q)) :
        MvPolynomial τ R)
mul_X :
  ∀ (p : MvPolynomial σ R) (a : σ)
    (h :
      Eq (α := MvPolynomial τ R)
        ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
            ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
          MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
          MvPolynomial τ R)),
    Eq (α := MvPolynomial τ R)
      ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (p * X a)) :
        MvPolynomial τ R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) (p * X a)) :
        MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    ((pderiv (f x) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p) :
      MvPolynomial τ R)

Tactic:
induction p using MvPolynomial.induction_on with
  | C a => simp
  | add p q hp hq => simp [hp, hq]
  | mul_X p a h =>
    simp only [map_mul, MvPolynomial.rename_X, Derivation.leibniz, MvPolynomial.pderiv_X,
      Pi.single_apply, hf.eq_iff, smul_eq_mul, mul_ite, mul_one, mul_zero, h, map_add]
    split_ifs <;> simp

Premises used: Pi.single_apply, Function.Injective.eq_iff, mul_ite, MvPolynomial.pderiv_X, map_add, MvPolynomial.induction_on, MulZeroClass.mul_zero, Derivation.leibniz, map_mul, MvPolynomial.rename_X, smul_eq_mul, mul_one, MvPolynomial.C