awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
hC :
  ∀ (n n_1 : ℕ),
    Eq.{u_1 + 1} (α := R)
      (coeff
        (coeff
          (((AlgHom.comp
                  (AlgHom.comp (B := MvPolynomial (Fin 2) R) (MvPolynomial.aeval ![(C : (a : R[X]) → R[X][Y]) X, Y])
                    (aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1)))
                  CAlgHom :
                R[X] →ₐ[R] R[X][Y]) :
              (a : R[X]) → R[X][Y])
            X)
          n)
        n_1)
      (coeff (coeff ((AlgHom.comp (AlgHom.id R R[X][Y]) CAlgHom : (a : R[X]) → R[X][Y]) X) n) n_1)
hX :
  ∀ (n n_1 : ℕ),
    Eq.{u_1 + 1} (α := R)
      (coeff
        (coeff
          (((AlgHom.comp (B := MvPolynomial (Fin 2) R) (MvPolynomial.aeval ![(C : (a : R[X]) → R[X][Y]) X, Y])
                  (aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1)) :
                R[X][Y] →ₐ[R] R[X][Y]) :
              (a : R[X][Y]) → R[X][Y])
            Y)
          n)
        n_1)
      (coeff (coeff ((AlgHom.id R R[X][Y] : (a : R[X][Y]) → R[X][Y]) Y) n) n_1)
⊢ Eq.{u_1 + 1} (α := R[X][Y] →ₐ[R] R[X][Y])
    (AlgHom.comp (B := MvPolynomial (Fin 2) R) (MvPolynomial.aeval ![(C : (a : R[X]) → R[X][Y]) X, Y])
        (aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1)) :
      R[X][Y] →ₐ[R] R[X][Y])
    (AlgHom.id R R[X][Y] : R[X][Y] →ₐ[R] R[X][Y])

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
n n_1 : ℕ
⊢ Eq.{u_1 + 1} (α := R)
    (coeff
      (coeff
        (((AlgHom.comp
                (AlgHom.comp (B := MvPolynomial (Fin 2) R) (MvPolynomial.aeval ![(C : (a : R[X]) → R[X][Y]) X, Y])
                  (aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1)))
                CAlgHom :
              R[X] →ₐ[R] R[X][Y]) :
            (a : R[X]) → R[X][Y])
          X)
        n)
      n_1)
    (coeff (coeff ((AlgHom.comp (AlgHom.id R R[X][Y]) CAlgHom : (a : R[X]) → R[X][Y]) X) n) n_1)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
n n_1 : ℕ
⊢ Eq.{u_1 + 1} (α := R)
    (coeff
      (coeff
        (((AlgHom.comp (B := MvPolynomial (Fin 2) R) (MvPolynomial.aeval ![(C : (a : R[X]) → R[X][Y]) X, Y])
                (aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1)) :
              R[X][Y] →ₐ[R] R[X][Y]) :
            (a : R[X][Y]) → R[X][Y])
          Y)
        n)
      n_1)
    (coeff (coeff ((AlgHom.id R R[X][Y] : (a : R[X][Y]) → R[X][Y]) Y) n) n_1)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
a : R
⊢ Eq (α := MvPolynomial (Fin 2) R)
    ((equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
        ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a)) :
      MvPolynomial (Fin 2) R)
    ((MvPolynomial.C : (a : R) → MvPolynomial (Fin 2) R) a : MvPolynomial (Fin 2) R)

Tactic:
simp [equivMvPolynomial]

Premises used: Polynomial.Bivariate.equivMvPolynomial
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq (α := MvPolynomial (Fin 2) R)
    ((equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R) ((C : (a : R[X]) → R[X][Y]) X) :
      MvPolynomial (Fin 2) R)
    (MvPolynomial.X 0 : MvPolynomial (Fin 2) R)

Tactic:
simp [equivMvPolynomial]

Premises used: Polynomial.Bivariate.equivMvPolynomial
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq (α := MvPolynomial (Fin 2) R)
    ((equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R) Y : MvPolynomial (Fin 2) R)
    (MvPolynomial.X 1 : MvPolynomial (Fin 2) R)

Tactic:
simp [equivMvPolynomial]

Premises used: Polynomial.Bivariate.equivMvPolynomial
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq (α := R[X][Y])
    ((AlgEquiv.symm (equivMvPolynomial R) : (a : MvPolynomial (Fin 2) R) → R[X][Y]) (MvPolynomial.X 0) : R[X][Y])
    ((C : (a : R[X]) → R[X][Y]) X : R[X][Y])

Tactic:
simp [equivMvPolynomial]

Premises used: Polynomial.Bivariate.equivMvPolynomial
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq (α := R[X][Y])
    ((AlgEquiv.symm (equivMvPolynomial R) : (a : MvPolynomial (Fin 2) R) → R[X][Y]) (MvPolynomial.X 1) : R[X][Y])
    (Y : R[X][Y])

Tactic:
simp [equivMvPolynomial]

Premises used: Polynomial.Bivariate.equivMvPolynomial
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
a : R
⊢ Eq (α := R[X][Y])
    ((AlgEquiv.symm (equivMvPolynomial R) : (a : MvPolynomial (Fin 2) R) → R[X][Y])
        ((MvPolynomial.C : (a : R) → MvPolynomial (Fin 2) R) a) :
      R[X][Y])
    ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a) : R[X][Y])

Tactic:
simp [equivMvPolynomial]

Premises used: Polynomial.Bivariate.equivMvPolynomial
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_2
inst : CommRing R
p q : R[X][Y]
h :
  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)
h_1 :
  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)

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_2
inst : CommRing R
n : ℕ
p q : R[X]
h :
  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)
h_1 :
  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]) 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])
            ((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) ((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])
            ((monomial n : (a : R[X]) → R[X][Y]) (p + q)))) :
      MvPolynomial (Fin 2) R)

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_2
inst : CommRing R
n m : ℕ
a : R
monomial :
  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)
          (HMul.hMul (α := R[X][Y])
            ((C : (a : R[X]) → R[X][Y])
                (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X m)) :
              R[X][Y])
            (HPow.hPow (α := R[X][Y]) Y n))) :
      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])
            (HMul.hMul (α := R[X][Y])
              ((C : (a : R[X]) → R[X][Y])
                  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X m)) :
                R[X][Y])
              (HPow.hPow (α := R[X][Y]) Y n)))) :
      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]) ((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)

Tactic:
simp_rw [← Polynomial.C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_2
inst : CommRing R
n 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)
          (HMul.hMul (α := R[X][Y])
            ((C : (a : R[X]) → R[X][Y])
                (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X m)) :
              R[X][Y])
            (HPow.hPow (α := R[X][Y]) Y n))) :
      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])
            (HMul.hMul (α := R[X][Y])
              ((C : (a : R[X]) → R[X][Y])
                  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X m)) :
                R[X][Y])
              (HPow.hPow (α := R[X][Y]) Y n)))) :
      MvPolynomial (Fin 2) R)

Tactic:
simp [map_nsmul]

Premises used: map_nsmul
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X][Y]
h :
  Eq (α := MvPolynomial (Fin 2) R)
    ((MvPolynomial.pderiv 1 : (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) ((derivative : (a : R[X][Y]) → R[X][Y]) p) :
      MvPolynomial (Fin 2) R)
h_1 :
  Eq (α := MvPolynomial (Fin 2) R)
    ((MvPolynomial.pderiv 1 : (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) ((derivative : (a : R[X][Y]) → R[X][Y]) q) :
      MvPolynomial (Fin 2) R)
⊢ Eq (α := MvPolynomial (Fin 2) R)
    ((MvPolynomial.pderiv 1 : (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) ((derivative : (a : R[X][Y]) → R[X][Y]) (p + q)) :
      MvPolynomial (Fin 2) R)

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
p q : R[X]
h :
  Eq (α := MvPolynomial (Fin 2) R)
    ((MvPolynomial.pderiv 1 : (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)
        ((derivative : (a : R[X][Y]) → R[X][Y]) ((monomial n : (a : R[X]) → R[X][Y]) p)) :
      MvPolynomial (Fin 2) R)
h_1 :
  Eq (α := MvPolynomial (Fin 2) R)
    ((MvPolynomial.pderiv 1 : (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]) q)) :
      MvPolynomial (Fin 2) R)
    ((equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
        ((derivative : (a : R[X][Y]) → R[X][Y]) ((monomial n : (a : R[X]) → R[X][Y]) q)) :
      MvPolynomial (Fin 2) R)
⊢ Eq (α := MvPolynomial (Fin 2) R)
    ((MvPolynomial.pderiv 1 : (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 + q))) :
      MvPolynomial (Fin 2) R)
    ((equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
        ((derivative : (a : R[X][Y]) → R[X][Y]) ((monomial n : (a : R[X]) → R[X][Y]) (p + q))) :
      MvPolynomial (Fin 2) R)

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
n m : ℕ
a : R
monomial :
  Eq (α := MvPolynomial (Fin 2) R)
    ((MvPolynomial.pderiv 1 : (a : MvPolynomial (Fin 2) R) → MvPolynomial (Fin 2) R)
        ((equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
          (HMul.hMul (α := R[X][Y])
            ((C : (a : R[X]) → R[X][Y])
                (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X m)) :
              R[X][Y])
            (HPow.hPow (α := R[X][Y]) Y n))) :
      MvPolynomial (Fin 2) R)
    ((equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
        ((derivative : (a : R[X][Y]) → R[X][Y])
          (HMul.hMul (α := R[X][Y])
            ((C : (a : R[X]) → R[X][Y])
                (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X m)) :
              R[X][Y])
            (HPow.hPow (α := R[X][Y]) Y n))) :
      MvPolynomial (Fin 2) R)
⊢ Eq (α := MvPolynomial (Fin 2) R)
    ((MvPolynomial.pderiv 1 : (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)
        ((derivative : (a : R[X][Y]) → R[X][Y])
          ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) ((Polynomial.monomial m : (a : R) → R[X]) a))) :
      MvPolynomial (Fin 2) R)

Tactic:
simp_rw [← Polynomial.C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
n m : ℕ
a : R
⊢ Eq (α := MvPolynomial (Fin 2) R)
    ((MvPolynomial.pderiv 1 : (a : MvPolynomial (Fin 2) R) → MvPolynomial (Fin 2) R)
        ((equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
          (HMul.hMul (α := R[X][Y])
            ((C : (a : R[X]) → R[X][Y])
                (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X m)) :
              R[X][Y])
            (HPow.hPow (α := R[X][Y]) Y n))) :
      MvPolynomial (Fin 2) R)
    ((equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
        ((derivative : (a : R[X][Y]) → R[X][Y])
          (HMul.hMul (α := R[X][Y])
            ((C : (a : R[X]) → R[X][Y])
                (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X m)) :
              R[X][Y])
            (HPow.hPow (α := R[X][Y]) Y n))) :
      MvPolynomial (Fin 2) R)

Tactic:
simp [derivative_pow]

Premises used: Polynomial.derivative_pow
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
p : R[X]
monomial :
  ∀ (p q : R[X]),
    Eq (α := MvPolynomial (Fin 2) R)
        ((MvPolynomial.pderiv 1 : (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)
            ((derivative : (a : R[X][Y]) → R[X][Y]) ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) p)) :
          MvPolynomial (Fin 2) R) →
      Eq (α := MvPolynomial (Fin 2) R)
          ((MvPolynomial.pderiv 1 : (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)
              ((derivative : (a : R[X][Y]) → R[X][Y]) ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) q)) :
            MvPolynomial (Fin 2) R) →
        Eq (α := MvPolynomial (Fin 2) R)
          ((MvPolynomial.pderiv 1 : (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)
              ((derivative : (a : R[X][Y]) → R[X][Y]) ((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 1 : (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)
          ((derivative : (a : R[X][Y]) → R[X][Y])
            ((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 1 : (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)
        ((derivative : (a : R[X][Y]) → R[X][Y]) ((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 [derivative_pow]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.monomial, Polynomial.derivative_pow
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X][Y]
add :
  ∀ (p q : R[X][Y]),
    Eq (α := MvPolynomial (Fin 2) R)
        ((MvPolynomial.pderiv 1 : (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) ((derivative : (a : R[X][Y]) → R[X][Y]) p) :
          MvPolynomial (Fin 2) R) →
      Eq (α := MvPolynomial (Fin 2) R)
          ((MvPolynomial.pderiv 1 : (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) ((derivative : (a : R[X][Y]) → R[X][Y]) q) :
            MvPolynomial (Fin 2) R) →
        Eq (α := MvPolynomial (Fin 2) R)
          ((MvPolynomial.pderiv 1 : (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)
              ((derivative : (a : R[X][Y]) → R[X][Y]) (p + q)) :
            MvPolynomial (Fin 2) R)
monomial :
  ∀ (n : ℕ) (p : R[X]),
    Eq (α := MvPolynomial (Fin 2) R)
      ((MvPolynomial.pderiv 1 : (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)
          ((derivative : (a : R[X][Y]) → R[X][Y]) ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) p)) :
        MvPolynomial (Fin 2) R)
⊢ Eq (α := MvPolynomial (Fin 2) R)
    ((MvPolynomial.pderiv 1 : (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) ((derivative : (a : R[X][Y]) → 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 [derivative_pow]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.monomial, Polynomial.derivative_pow
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : R[X][Y]
h : Polynomial.evalEval x y p = 0
g : R[X][Y]
rw :
  (lift (evalRingHom x) y ⋯ : (a : AdjoinRoot p) → R) ((mk p : (a : R[X][Y]) → AdjoinRoot p) g : AdjoinRoot p) =
    Polynomial.evalEval x y g
rw₁ : eval₂ (evalRingHom x) y g = Polynomial.evalEval x y g
rw₂ rw₃ : Polynomial.evalEval x y g = Polynomial.evalEval x y g
⊢ (evalEval h : (a : AdjoinRoot p) → R) ((mk p : (a : R[X][Y]) → AdjoinRoot p) g : AdjoinRoot p) =
    Polynomial.evalEval x y g

Tactic:
rw [evalEval, lift_mk, eval₂_evalRingHom]

Premises used: AdjoinRoot.evalEval, AdjoinRoot.lift_mk, Polynomial.eval₂_evalRingHom
-- Module: Mathlib.Algebra.Polynomial.CancelLeads
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
⊢ -p.cancelLeads q = q.cancelLeads p

Tactic:
neg_sub _ _

Premises used: neg_sub, Polynomial.cancelLeads
-- Module: Mathlib.Algebra.Polynomial.CancelLeads
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
pos : ∀ (hp : p = 0), (p.cancelLeads q).natDegree < q.natDegree
neg : ∀ (hp : ¬p = 0), (p.cancelLeads q).natDegree < q.natDegree
⊢ (p.cancelLeads q).natDegree < q.natDegree

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.CancelLeads
Goal:
R : Type u_1
inst : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : p = 0
⊢ 0 < q.natDegree

Tactic:
hq