-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_2
inst : CommRing R
p : R[X][Y]
add :
  ∀ (p q : R[X][Y]),
    Eq (α := MvPolynomial (Fin 2) R)
        ((MvPolynomial.pderiv 0 : (a : MvPolynomial (Fin 2) R) → MvPolynomial (Fin 2) R)
            ((equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R) p) :
          MvPolynomial (Fin 2) R)
        ((equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
            ((PolynomialModule.equivPolynomialSelf : (a : PolynomialModule R[X] R[X]) → R[X][Y])
              ((Derivation.mapCoeffs derivative' : (a : R[X][Y]) → PolynomialModule R[X] R[X]) p)) :
          MvPolynomial (Fin 2) R) →
      Eq (α := MvPolynomial (Fin 2) R)
          ((MvPolynomial.pderiv 0 : (a : MvPolynomial (Fin 2) R) → MvPolynomial (Fin 2) R)
              ((equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R) q) :
            MvPolynomial (Fin 2) R)
          ((equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
              ((PolynomialModule.equivPolynomialSelf : (a : PolynomialModule R[X] R[X]) → R[X][Y])
                ((Derivation.mapCoeffs derivative' : (a : R[X][Y]) → PolynomialModule R[X] R[X]) q)) :
            MvPolynomial (Fin 2) R) →
        Eq (α := MvPolynomial (Fin 2) R)
          ((MvPolynomial.pderiv 0 : (a : MvPolynomial (Fin 2) R) → MvPolynomial (Fin 2) R)
              ((equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R) (p + q)) :
            MvPolynomial (Fin 2) R)
          ((equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
              ((PolynomialModule.equivPolynomialSelf : (a : PolynomialModule R[X] R[X]) → R[X][Y])
                ((Derivation.mapCoeffs derivative' : (a : R[X][Y]) → PolynomialModule R[X] R[X]) (p + q))) :
            MvPolynomial (Fin 2) R)
⊢ Eq (α := MvPolynomial (Fin 2) R)
    ((MvPolynomial.pderiv 0 : (a : MvPolynomial (Fin 2) R) → MvPolynomial (Fin 2) R)
        ((equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R) p) :
      MvPolynomial (Fin 2) R)
    ((equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
        ((PolynomialModule.equivPolynomialSelf : (a : PolynomialModule R[X] R[X]) → R[X][Y])
          ((Derivation.mapCoeffs derivative' : (a : R[X][Y]) → PolynomialModule R[X] R[X]) p)) :
      MvPolynomial (Fin 2) R)
have monomial : ∀ (n : ℕ) (p : R[X]),
  Eq (α := MvPolynomial (Fin 2) R)
    ((MvPolynomial.pderiv 0 : (a : MvPolynomial (Fin 2) R) → MvPolynomial (Fin 2) R)
        ((equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R) ((monomial n : (a : R[X]) → R[X][Y]) p)) :
      MvPolynomial (Fin 2) R)
    ((equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
        ((PolynomialModule.equivPolynomialSelf : (a : PolynomialModule R[X] R[X]) → R[X][Y])
          ((Derivation.mapCoeffs derivative' : (a : R[X][Y]) → PolynomialModule R[X] R[X])
            ((monomial n : (a : R[X]) → R[X][Y]) p))) :
      MvPolynomial (Fin 2) R)
Tactic: induction p using Polynomial.induction_on' with
  | add p q _ _ => aesop
  | monomial n p =>
  induction p using Polynomial.induction_on' with
  | add p q _ _ => aesop
  | monomial m a =>
    simp_rw [← Polynomial.C_mul_X_pow_eq_monomial]
    simp [map_nsmul]
Cleared hypotheses: p