awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
i : Fin 2
m : Fin 2 →₀ ℕ
⊢ Eq.{u_1 + 1} (α := R)
    (MvPolynomial.coeff m
      ((AlgHom.comp (aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1))
            (MvPolynomial.aeval ![(C : (a : R[X]) → R[X][Y]) X, Y]) :
          (a : MvPolynomial (Fin 2) R) → MvPolynomial (Fin 2) R)
        (MvPolynomial.X i)))
    (MvPolynomial.coeff m
      ((AlgHom.id R (MvPolynomial (Fin 2) R) : (a : MvPolynomial (Fin 2) R) → MvPolynomial (Fin 2) R)
        (MvPolynomial.X i)))
have hf : Eq.{u_1 + 1} (α := R)
  (MvPolynomial.coeff m
    ((AlgHom.comp (aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1))
          (MvPolynomial.aeval ![(C : (a : R[X]) → R[X][Y]) X, Y]) :
        (a : MvPolynomial (Fin 2) R) → MvPolynomial (Fin 2) R)
      (MvPolynomial.X ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩))))
  (MvPolynomial.coeff m
    ((AlgHom.id R (MvPolynomial (Fin 2) R) : (a : MvPolynomial (Fin 2) R) → MvPolynomial (Fin 2) R)
      (MvPolynomial.X ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩))))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
i : Fin 2
m : Fin 2 →₀ ℕ
hf :
  Eq.{u_1 + 1} (α := R)
    (MvPolynomial.coeff m
      ((AlgHom.comp (aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1))
            (MvPolynomial.aeval ![(C : (a : R[X]) → R[X][Y]) X, Y]) :
          (a : MvPolynomial (Fin 2) R) → MvPolynomial (Fin 2) R)
        (MvPolynomial.X ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩))))
    (MvPolynomial.coeff m
      ((AlgHom.id R (MvPolynomial (Fin 2) R) : (a : MvPolynomial (Fin 2) R) → MvPolynomial (Fin 2) R)
        (MvPolynomial.X ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩))))
⊢ Eq.{u_1 + 1} (α := R)
    (MvPolynomial.coeff m
      ((AlgHom.comp (aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1))
            (MvPolynomial.aeval ![(C : (a : R[X]) → R[X][Y]) X, Y]) :
          (a : MvPolynomial (Fin 2) R) → MvPolynomial (Fin 2) R)
        (MvPolynomial.X i)))
    (MvPolynomial.coeff m
      ((AlgHom.id R (MvPolynomial (Fin 2) R) : (a : MvPolynomial (Fin 2) R) → MvPolynomial (Fin 2) R)
        (MvPolynomial.X i)))
have hf₁ : Eq.{u_1 + 1} (α := R)
  (MvPolynomial.coeff m
    ((AlgHom.comp (aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1))
          (MvPolynomial.aeval ![(C : (a : R[X]) → R[X][Y]) X, Y]) :
        (a : MvPolynomial (Fin 2) R) → MvPolynomial (Fin 2) R)
      (MvPolynomial.X ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩))))
  (MvPolynomial.coeff m
    ((AlgHom.id R (MvPolynomial (Fin 2) R) : (a : MvPolynomial (Fin 2) R) → MvPolynomial (Fin 2) R)
      (MvPolynomial.X ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩))))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
⊢ 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])
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
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)
⊢ 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])
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
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)
          ((monomial n : (a : R[X]) → R[X][Y]) ((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])
            ((monomial n : (a : R[X]) → R[X][Y]) ((monomial m : (a : R) → R[X]) a)))) :
      MvPolynomial (Fin 2) R)
have 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)
Tactic: simp_rw [← Polynomial.C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_2
inst : CommRing R
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)
have 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) ((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) →
    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: 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
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_2
inst : CommRing R
p : 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)
have 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)
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
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
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)
          ((monomial n : (a : R[X]) → R[X][Y]) ((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])
          ((monomial n : (a : R[X]) → R[X][Y]) ((monomial m : (a : R) → R[X]) a))) :
      MvPolynomial (Fin 2) R)
have 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)
Tactic: simp_rw [← Polynomial.C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
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) ((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)
have 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) ((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) →
    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: 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]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
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)
⊢ 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)
have 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)
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]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : 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)
have 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)
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]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
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)
⊢ 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)
have 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) ((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)
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]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
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]
⊢ (evalEval h : (a : AdjoinRoot p) → R) ((mk p : (a : R[X][Y]) → AdjoinRoot p) g : AdjoinRoot p) =
    Polynomial.evalEval x y g
have rw : (lift (evalRingHom x) y sorry : (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]