-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.PDeriv (goal)
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))
⊢ 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))
have 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))
Tactic: classical
  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]
Cleared hypotheses: p