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