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
n : ℕ
a : R
monomial :
  Eq (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y]) ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a)) :
      R[X][Y])
    ((C : (a : R[X]) → R[X][Y]) ((Polynomial.monomial n : (a : R) → R[X]) a) : R[X][Y])
monomial₁ :
  Eq (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y])
        (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a) : R[X][Y])
          (HPow.hPow (α := R[X][Y]) Y n)) :
      R[X][Y])
    ((C : (a : R[X]) → R[X][Y]) ((Polynomial.monomial n : (a : R) → R[X]) a) : R[X][Y])
monomial₂ :
  Eq (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y])
        (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a) : R[X][Y])
          (HPow.hPow (α := R[X][Y]) Y n)) :
      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 n)) :
      R[X][Y])
monomial₃ :
  HMul.hMul (α := R[X][Y]) (β := R[X][Y])
      ((swap : (a : R[X][Y]) → R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a)) : R[X][Y])
      ((swap : (a : R[X][Y]) → R[X][Y]) (HPow.hPow (α := R[X][Y]) Y n) : 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 n))
⊢ Eq.{u_1 + 1} (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y]) (map C ((Polynomial.monomial n : (a : R) → R[X]) a)) : R[X][Y])
    ((C : (a : R[X]) → R[X][Y]) ((Polynomial.monomial n : (a : R) → R[X]) a) : R[X][Y])
have monomial₄ : HMul.hMul (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a)) : R[X][Y])
    (HPow.hPow (α := R[X][Y]) ((swap : (a : R[X][Y]) → R[X][Y]) Y : R[X][Y]) n) =
  (C : (a : R[X]) → R[X][Y]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
Tactic: rw [map_monomial, ← C_mul_X_pow_eq_monomial, ← C_mul_X_pow_eq_monomial,
    map_mul, map_pow, swap_Y, C_mul, C_pow, Bivariate.swap_C_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
a : R
monomial :
  Eq (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y]) ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a)) :
      R[X][Y])
    ((C : (a : R[X]) → R[X][Y]) ((Polynomial.monomial n : (a : R) → R[X]) a) : R[X][Y])
monomial₁ :
  Eq (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y])
        (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a) : R[X][Y])
          (HPow.hPow (α := R[X][Y]) Y n)) :
      R[X][Y])
    ((C : (a : R[X]) → R[X][Y]) ((Polynomial.monomial n : (a : R) → R[X]) a) : R[X][Y])
monomial₂ :
  Eq (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y])
        (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a) : R[X][Y])
          (HPow.hPow (α := R[X][Y]) Y n)) :
      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 n)) :
      R[X][Y])
monomial₃ :
  HMul.hMul (α := R[X][Y]) (β := R[X][Y])
      ((swap : (a : R[X][Y]) → R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a)) : R[X][Y])
      ((swap : (a : R[X][Y]) → R[X][Y]) (HPow.hPow (α := R[X][Y]) Y n) : 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 n))
monomial₄ :
  HMul.hMul (α := R[X][Y])
      ((swap : (a : R[X][Y]) → R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a)) : R[X][Y])
      (HPow.hPow (α := R[X][Y]) ((swap : (a : R[X][Y]) → R[X][Y]) Y : R[X][Y]) n) =
    (C : (a : R[X]) → R[X][Y]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ Eq.{u_1 + 1} (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y]) (map C ((Polynomial.monomial n : (a : R) → R[X]) a)) : R[X][Y])
    ((C : (a : R[X]) → R[X][Y]) ((Polynomial.monomial n : (a : R) → R[X]) a) : R[X][Y])
have monomial₅ : HMul.hMul (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a)) : R[X][Y])
    (HPow.hPow (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) n) =
  (C : (a : R[X]) → R[X][Y]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
Tactic: rw [map_monomial, ← C_mul_X_pow_eq_monomial, ← C_mul_X_pow_eq_monomial,
    map_mul, map_pow, swap_Y, C_mul, C_pow, Bivariate.swap_C_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
a : R
monomial :
  Eq (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y]) ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a)) :
      R[X][Y])
    ((C : (a : R[X]) → R[X][Y]) ((Polynomial.monomial n : (a : R) → R[X]) a) : R[X][Y])
monomial₁ :
  Eq (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y])
        (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a) : R[X][Y])
          (HPow.hPow (α := R[X][Y]) Y n)) :
      R[X][Y])
    ((C : (a : R[X]) → R[X][Y]) ((Polynomial.monomial n : (a : R) → R[X]) a) : R[X][Y])
monomial₂ :
  Eq (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y])
        (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a) : R[X][Y])
          (HPow.hPow (α := R[X][Y]) Y n)) :
      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 n)) :
      R[X][Y])
monomial₃ :
  HMul.hMul (α := R[X][Y]) (β := R[X][Y])
      ((swap : (a : R[X][Y]) → R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a)) : R[X][Y])
      ((swap : (a : R[X][Y]) → R[X][Y]) (HPow.hPow (α := R[X][Y]) Y n) : 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 n))
monomial₄ :
  HMul.hMul (α := R[X][Y])
      ((swap : (a : R[X][Y]) → R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a)) : R[X][Y])
      (HPow.hPow (α := R[X][Y]) ((swap : (a : R[X][Y]) → R[X][Y]) Y : R[X][Y]) n) =
    (C : (a : R[X]) → R[X][Y]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
monomial₅ :
  HMul.hMul (α := R[X][Y])
      ((swap : (a : R[X][Y]) → R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a)) : R[X][Y])
      (HPow.hPow (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) n) =
    (C : (a : R[X]) → R[X][Y]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ Eq.{u_1 + 1} (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y]) (map C ((Polynomial.monomial n : (a : R) → R[X]) a)) : R[X][Y])
    ((C : (a : R[X]) → R[X][Y]) ((Polynomial.monomial n : (a : R) → R[X]) a) : R[X][Y])
have monomial₆ : HMul.hMul (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a)) : R[X][Y])
    (HPow.hPow (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) n) =
  HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a) : R[X][Y])
    ((C : (a : R[X]) → R[X][Y]) (HPow.hPow (α := R[X]) X n) : R[X][Y])
Tactic: rw [map_monomial, ← C_mul_X_pow_eq_monomial, ← C_mul_X_pow_eq_monomial,
    map_mul, map_pow, swap_Y, C_mul, C_pow, Bivariate.swap_C_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
⊢ Eq (α := R[X][Y]) ((swap : (a : R[X][Y]) → R[X][Y]) (map C f) : R[X][Y]) ((C : (a : R[X]) → R[X][Y]) f : R[X][Y])
have add : ∀ (p q : R[X]),
  Eq (α := R[X][Y]) ((swap : (a : R[X][Y]) → R[X][Y]) (map C p) : R[X][Y]) ((C : (a : R[X]) → R[X][Y]) p : R[X][Y]) →
    Eq (α := R[X][Y]) ((swap : (a : R[X][Y]) → R[X][Y]) (map C q) : R[X][Y]) ((C : (a : R[X]) → R[X][Y]) q : R[X][Y]) →
      Eq (α := R[X][Y]) ((swap : (a : R[X][Y]) → R[X][Y]) (map C (p + q)) : R[X][Y])
        ((C : (a : R[X]) → R[X][Y]) (p + q) : R[X][Y])
Tactic: induction f using Polynomial.induction_on' with
  | add => aesop
  | monomial n a => rw [map_monomial, ← C_mul_X_pow_eq_monomial, ← C_mul_X_pow_eq_monomial,
    map_mul, map_pow, swap_Y, C_mul, C_pow, Bivariate.swap_C_C]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
add :
  ∀ (p q : R[X]),
    Eq (α := R[X][Y]) ((swap : (a : R[X][Y]) → R[X][Y]) (map C p) : R[X][Y]) ((C : (a : R[X]) → R[X][Y]) p : R[X][Y]) →
      Eq (α := R[X][Y]) ((swap : (a : R[X][Y]) → R[X][Y]) (map C q) : R[X][Y])
          ((C : (a : R[X]) → R[X][Y]) q : R[X][Y]) →
        Eq (α := R[X][Y]) ((swap : (a : R[X][Y]) → R[X][Y]) (map C (p + q)) : R[X][Y])
          ((C : (a : R[X]) → R[X][Y]) (p + q) : R[X][Y])
⊢ Eq (α := R[X][Y]) ((swap : (a : R[X][Y]) → R[X][Y]) (map C f) : R[X][Y]) ((C : (a : R[X]) → R[X][Y]) f : R[X][Y])
have monomial : ∀ (n : ℕ) (a : R),
  Eq.{u_1 + 1} (α := R[X][Y]) ((swap : (a : R[X][Y]) → R[X][Y]) (map C ((monomial n : (a : R) → R[X]) a)) : R[X][Y])
    ((C : (a : R[X]) → R[X][Y]) ((monomial n : (a : R) → R[X]) a) : R[X][Y])
Tactic: induction f using Polynomial.induction_on' with
  | add => aesop
  | monomial n a => rw [map_monomial, ← C_mul_X_pow_eq_monomial, ← C_mul_X_pow_eq_monomial,
    map_mul, map_pow, swap_Y, C_mul, C_pow, Bivariate.swap_C_C]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n m : ℕ
r : R
⊢ Eq (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y]) ((monomial n : (a : R[X]) → R[X][Y]) ((monomial m : (a : R) → R[X]) r)) : R[X][Y])
    ((monomial m : (a : R[X]) → R[X][Y]) ((monomial n : (a : R) → R[X]) r) : R[X][Y])
have simp : HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) r) : R[X][Y])
      (HPow.hPow (α := R[X][Y]) Y m) *
    HPow.hPow (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) n =
  HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) r) : R[X][Y])
      (HPow.hPow (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) n) *
    HPow.hPow (α := R[X][Y]) Y m
Tactic: simp [← C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
x y : A
n : ℕ
a : R[X]
⊢ Eq.{u_2 + 1} (α := A)
    ((aevalAeval x y : (a : R[X][Y]) → A)
        ((swap : (a : R[X][Y]) → R[X][Y]) ((monomial n : (a : R[X]) → R[X][Y]) a) : R[X][Y]) :
      A)
    ((aevalAeval y x : (a : R[X][Y]) → A) ((monomial n : (a : R[X]) → R[X][Y]) a : R[X][Y]) : A)
have monomial : eval x
      (((aeval ((C : (a : A) → A[X]) y) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X])
        ((aeval Y : (a : R[X]) → R[X][Y]) a)) *
    x ^ n =
  HMul.hMul (α := A) ((aeval y : (a : R[X]) → A) a : A) (x ^ n)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
x y : A
n : ℕ
a : R[X]
⊢ eval x
        (((aeval ((C : (a : A) → A[X]) y) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X])
          ((aeval Y : (a : R[X]) → R[X][Y]) a)) *
      x ^ n =
    HMul.hMul (α := A) ((aeval y : (a : R[X]) → A) a : A) (x ^ n)
have monomial : ∀ (p q : R[X]),
  eval x
          (((aeval ((C : (a : A) → A[X]) y) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X])
            ((aeval Y : (a : R[X]) → R[X][Y]) p)) *
        x ^ n =
      HMul.hMul (α := A) ((aeval y : (a : R[X]) → A) p : A) (x ^ n) →
    eval x
            (((aeval ((C : (a : A) → A[X]) y) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X])
              ((aeval Y : (a : R[X]) → R[X][Y]) q)) *
          x ^ n =
        HMul.hMul (α := A) ((aeval y : (a : R[X]) → A) q : A) (x ^ n) →
      eval x
            (((aeval ((C : (a : A) → A[X]) y) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X])
              ((aeval Y : (a : R[X]) → R[X][Y]) (p + q))) *
          x ^ n =
        HMul.hMul (α := A) ((aeval y : (a : R[X]) → A) (p + q) : A) (x ^ n)
Tactic: induction a using Polynomial.induction_on'
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
x y : A
n : ℕ
a : R[X]
monomial :
  ∀ (p q : R[X]),
    eval x
            (((aeval ((C : (a : A) → A[X]) y) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X])
              ((aeval Y : (a : R[X]) → R[X][Y]) p)) *
          x ^ n =
        HMul.hMul (α := A) ((aeval y : (a : R[X]) → A) p : A) (x ^ n) →
      eval x
              (((aeval ((C : (a : A) → A[X]) y) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X])
                ((aeval Y : (a : R[X]) → R[X][Y]) q)) *
            x ^ n =
          HMul.hMul (α := A) ((aeval y : (a : R[X]) → A) q : A) (x ^ n) →
        eval x
              (((aeval ((C : (a : A) → A[X]) y) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X])
                ((aeval Y : (a : R[X]) → R[X][Y]) (p + q))) *
            x ^ n =
          HMul.hMul (α := A) ((aeval y : (a : R[X]) → A) (p + q) : A) (x ^ n)
⊢ eval x
        (((aeval ((C : (a : A) → A[X]) y) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X])
          ((aeval Y : (a : R[X]) → R[X][Y]) a)) *
      x ^ n =
    HMul.hMul (α := A) ((aeval y : (a : R[X]) → A) a : A) (x ^ n)
have monomial₁ : ∀ (n_1 : ℕ) (a : R),
  eval x
        (((aeval ((C : (a : A) → A[X]) y) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X])
          ((aeval Y : (a : R[X]) → R[X][Y]) ((Polynomial.monomial n_1 : (a : R) → R[X]) a))) *
      x ^ n =
    HMul.hMul (α := A) ((aeval y : (a : R[X]) → A) ((Polynomial.monomial n_1 : (a : R) → R[X]) a : R[X]) : A) (x ^ n)
Tactic: induction a using Polynomial.induction_on'
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
x y : A
p : R[X][Y]
⊢ Eq.{u_2 + 1} (α := A) ((aevalAeval x y : (a : R[X][Y]) → A) ((swap : (a : R[X][Y]) → R[X][Y]) p : R[X][Y]) : A)
    ((aevalAeval y x : (a : R[X][Y]) → A) p : A)
have add : ∀ (p q : R[X][Y]),
  Eq.{u_2 + 1} (α := A) ((aevalAeval x y : (a : R[X][Y]) → A) ((swap : (a : R[X][Y]) → R[X][Y]) p : R[X][Y]) : A)
      ((aevalAeval y x : (a : R[X][Y]) → A) p : A) →
    Eq.{u_2 + 1} (α := A) ((aevalAeval x y : (a : R[X][Y]) → A) ((swap : (a : R[X][Y]) → R[X][Y]) q : R[X][Y]) : A)
        ((aevalAeval y x : (a : R[X][Y]) → A) q : A) →
      Eq.{u_2 + 1} (α := A)
        ((aevalAeval x y : (a : R[X][Y]) → A) ((swap : (a : R[X][Y]) → R[X][Y]) (p + q) : R[X][Y]) : A)
        ((aevalAeval y x : (a : R[X][Y]) → A) (p + q) : A)
Tactic: induction p using Polynomial.induction_on' with
  | add => aesop
  | monomial n a =>
    simp
    induction a using Polynomial.induction_on' <;> aesop (add norm add_mul)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
x y : A
p : R[X][Y]
add :
  ∀ (p q : R[X][Y]),
    Eq.{u_2 + 1} (α := A) ((aevalAeval x y : (a : R[X][Y]) → A) ((swap : (a : R[X][Y]) → R[X][Y]) p : R[X][Y]) : A)
        ((aevalAeval y x : (a : R[X][Y]) → A) p : A) →
      Eq.{u_2 + 1} (α := A) ((aevalAeval x y : (a : R[X][Y]) → A) ((swap : (a : R[X][Y]) → R[X][Y]) q : R[X][Y]) : A)
          ((aevalAeval y x : (a : R[X][Y]) → A) q : A) →
        Eq.{u_2 + 1} (α := A)
          ((aevalAeval x y : (a : R[X][Y]) → A) ((swap : (a : R[X][Y]) → R[X][Y]) (p + q) : R[X][Y]) : A)
          ((aevalAeval y x : (a : R[X][Y]) → A) (p + q) : A)
⊢ Eq.{u_2 + 1} (α := A) ((aevalAeval x y : (a : R[X][Y]) → A) ((swap : (a : R[X][Y]) → R[X][Y]) p : R[X][Y]) : A)
    ((aevalAeval y x : (a : R[X][Y]) → A) p : A)
have monomial : ∀ (n : ℕ) (a : R[X]),
  Eq.{u_2 + 1} (α := A)
    ((aevalAeval x y : (a : R[X][Y]) → A)
        ((swap : (a : R[X][Y]) → R[X][Y]) ((monomial n : (a : R[X]) → R[X][Y]) a) : R[X][Y]) :
      A)
    ((aevalAeval y x : (a : R[X][Y]) → A) ((monomial n : (a : R[X]) → R[X][Y]) a : R[X][Y]) : A)
Tactic: induction p using Polynomial.induction_on' with
  | add => aesop
  | monomial n a =>
    simp
    induction a using Polynomial.induction_on' <;> aesop (add norm add_mul)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
x : A
n : ℕ
a : R[X]
⊢ Eq.{u_2 + 1} (α := A[X])
    (((aeval ((C : (a : A) → A[X]) x) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X])
        ((monomial n : (a : R[X]) → R[X][Y]) a) :
      A[X])
    ((mapAlgHom (aeval x) : (a : R[X][Y]) → A[X])
        ((swap : (a : R[X][Y]) → R[X][Y]) ((monomial n : (a : R[X]) → R[X][Y]) a)) :
      A[X])
have monomial : map (algebraMap R A) a * HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n =
  map (↑(aeval x) : R[X] →+* A) ((aeval Y : (a : R[X]) → R[X][Y]) a) *
    HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
x : A
n : ℕ
a : R[X]
⊢ map (algebraMap R A) a * HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n =
    map (↑(aeval x) : R[X] →+* A) ((aeval Y : (a : R[X]) → R[X][Y]) a) *
      HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n
have monomial : ∀ (p q : R[X]),
  map (algebraMap R A) p * HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n =
      map (↑(aeval x) : R[X] →+* A) ((aeval Y : (a : R[X]) → R[X][Y]) p) *
        HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n →
    map (algebraMap R A) q * HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n =
        map (↑(aeval x) : R[X] →+* A) ((aeval Y : (a : R[X]) → R[X][Y]) q) *
          HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n →
      map (algebraMap R A) (p + q) * HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n =
        map (↑(aeval x) : R[X] →+* A) ((aeval Y : (a : R[X]) → R[X][Y]) (p + q)) *
          HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n
Tactic: induction a using Polynomial.induction_on'
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
x : A
n : ℕ
a : R[X]
monomial :
  ∀ (p q : R[X]),
    map (algebraMap R A) p * HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n =
        map (↑(aeval x) : R[X] →+* A) ((aeval Y : (a : R[X]) → R[X][Y]) p) *
          HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n →
      map (algebraMap R A) q * HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n =
          map (↑(aeval x) : R[X] →+* A) ((aeval Y : (a : R[X]) → R[X][Y]) q) *
            HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n →
        map (algebraMap R A) (p + q) * HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n =
          map (↑(aeval x) : R[X] →+* A) ((aeval Y : (a : R[X]) → R[X][Y]) (p + q)) *
            HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n
⊢ map (algebraMap R A) a * HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n =
    map (↑(aeval x) : R[X] →+* A) ((aeval Y : (a : R[X]) → R[X][Y]) a) *
      HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n
have monomial₁ : ∀ (n_1 : ℕ) (a : R),
  map (algebraMap R A) ((Polynomial.monomial n_1 : (a : R) → R[X]) a) *
      HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n =
    map (↑(aeval x) : R[X] →+* A) ((aeval Y : (a : R[X]) → R[X][Y]) ((Polynomial.monomial n_1 : (a : R) → R[X]) a)) *
      HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n
Tactic: induction a using Polynomial.induction_on'
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
x : A
p : R[X][Y]
⊢ Eq.{u_2 + 1} (α := A[X])
    (((aeval ((C : (a : A) → A[X]) x) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X]) p : A[X])
    ((mapAlgHom (aeval x) : (a : R[X][Y]) → A[X]) ((swap : (a : R[X][Y]) → R[X][Y]) p) : A[X])
have add : ∀ (p q : R[X][Y]),
  Eq.{u_2 + 1} (α := A[X])
      (((aeval ((C : (a : A) → A[X]) x) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X]) p : A[X])
      ((mapAlgHom (aeval x) : (a : R[X][Y]) → A[X]) ((swap : (a : R[X][Y]) → R[X][Y]) p) : A[X]) →
    Eq.{u_2 + 1} (α := A[X])
        (((aeval ((C : (a : A) → A[X]) x) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X]) q : A[X])
        ((mapAlgHom (aeval x) : (a : R[X][Y]) → A[X]) ((swap : (a : R[X][Y]) → R[X][Y]) q) : A[X]) →
      Eq.{u_2 + 1} (α := A[X])
        (((aeval ((C : (a : A) → A[X]) x) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X]) (p + q) :
          A[X])
        ((mapAlgHom (aeval x) : (a : R[X][Y]) → A[X]) ((swap : (a : R[X][Y]) → R[X][Y]) (p + q)) : A[X])
Tactic: induction p using Polynomial.induction_on' with
  | add => aesop
  | monomial n a =>
      simp
      induction a using Polynomial.induction_on'
        <;> aesop (add norm [add_mul, C_mul_X_pow_eq_monomial])
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
x : A
p : R[X][Y]
add :
  ∀ (p q : R[X][Y]),
    Eq.{u_2 + 1} (α := A[X])
        (((aeval ((C : (a : A) → A[X]) x) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X]) p : A[X])
        ((mapAlgHom (aeval x) : (a : R[X][Y]) → A[X]) ((swap : (a : R[X][Y]) → R[X][Y]) p) : A[X]) →
      Eq.{u_2 + 1} (α := A[X])
          (((aeval ((C : (a : A) → A[X]) x) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X]) q :
            A[X])
          ((mapAlgHom (aeval x) : (a : R[X][Y]) → A[X]) ((swap : (a : R[X][Y]) → R[X][Y]) q) : A[X]) →
        Eq.{u_2 + 1} (α := A[X])
          (((aeval ((C : (a : A) → A[X]) x) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X])
              (p + q) :
            A[X])
          ((mapAlgHom (aeval x) : (a : R[X][Y]) → A[X]) ((swap : (a : R[X][Y]) → R[X][Y]) (p + q)) : A[X])
⊢ Eq.{u_2 + 1} (α := A[X])
    (((aeval ((C : (a : A) → A[X]) x) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X]) p : A[X])
    ((mapAlgHom (aeval x) : (a : R[X][Y]) → A[X]) ((swap : (a : R[X][Y]) → R[X][Y]) p) : A[X])
have monomial : ∀ (n : ℕ) (a : R[X]),
  Eq.{u_2 + 1} (α := A[X])
    (((aeval ((C : (a : A) → A[X]) x) : AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] A[X]) : (a : R[X][Y]) → A[X])
        ((monomial n : (a : R[X]) → R[X][Y]) a) :
      A[X])
    ((mapAlgHom (aeval x) : (a : R[X][Y]) → A[X])
        ((swap : (a : R[X][Y]) → R[X][Y]) ((monomial n : (a : R[X]) → R[X][Y]) a)) :
      A[X])
Tactic: induction p using Polynomial.induction_on' with
  | add => aesop
  | monomial n a =>
      simp
      induction a using Polynomial.induction_on'
        <;> aesop (add norm [add_mul, C_mul_X_pow_eq_monomial])
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq (α := MvPolynomial (Fin 2) R →ₐ[R] MvPolynomial (Fin 2) R)
    (AlgHom.comp (aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1))
      (MvPolynomial.aeval ![(C : (a : R[X]) → R[X][Y]) X, Y]))
    (AlgHom.id R (MvPolynomial (Fin 2) R))
have hf : ∀ (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)))
Tactic: ext i