-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_2
inst : CommRing R
n : ℕ
p : R[X]
monomial :
  ∀ (p q : 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)
              ((Polynomial.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])
                ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) 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)
                ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) 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])
                  ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) 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)
                ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) (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])
                  ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) (p + q)))) :
            MvPolynomial (Fin 2) R)
monomial₁ :
  ∀ (m : ℕ) (a : 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)
            ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) ((Polynomial.monomial m : (a : R) → R[X]) a))) :
        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])
              ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) ((Polynomial.monomial m : (a : R) → R[X]) a)))) :
        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)
          ((Polynomial.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])
            ((Polynomial.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 m a =>
    simp_rw [← Polynomial.C_mul_X_pow_eq_monomial]
    simp [map_nsmul]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.monomial, map_nsmul