awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
h₂ :
  ∀ (n m : ℕ),
    Eq.{u_1 + 1} (α := R)
      (coeff
        (coeff
          ((AlgHom.comp
                (AlgHom.comp (aevalAeval Y ((C : (a : R[X]) → R[X][Y]) X))
                  (aevalAeval Y ((C : (a : R[X]) → R[X][Y]) X)))
                CAlgHom :
              (a : R[X]) → R[X][Y])
            X)
          n)
        m)
      (coeff (coeff ((AlgHom.comp (AlgHom.id R R[X][Y]) CAlgHom : (a : R[X]) → R[X][Y]) X) n) m)
h₃ :
  ∀ (n m : ℕ),
    Eq.{u_1 + 1} (α := R)
      (coeff
        (coeff
          ((AlgHom.comp (aevalAeval Y ((C : (a : R[X]) → R[X][Y]) X)) (aevalAeval Y ((C : (a : R[X]) → R[X][Y]) X)) :
              (a : R[X][Y]) → R[X][Y])
            Y)
          n)
        m)
      (coeff (coeff ((AlgHom.id R R[X][Y] : (a : R[X][Y]) → R[X][Y]) Y) n) m)
⊢ Eq (α := R[X][Y] →ₐ[R] R[X][Y])
    (AlgHom.comp (aevalAeval Y ((C : (a : R[X]) → R[X][Y]) X)) (aevalAeval Y ((C : (a : R[X]) → R[X][Y]) X)))
    (AlgHom.id R R[X][Y])

Tactic:
ext n m
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := R[X][Y] ≃ₐ[R] R[X][Y]) (AlgEquiv.symm swap) swap

Tactic:
rfl

Premises used: AlgEquiv.symm, AlgEquiv.ofAlgHom, Polynomial.Bivariate.swap, Equiv.symm, rfl
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X][Y]
⊢ Eq (α := R[X][Y]) ((swap : (a : R[X][Y]) → R[X][Y]) p : R[X][Y])
    ((aevalAeval Y ((C : (a : R[X]) → R[X][Y]) X) : (a : R[X][Y]) → R[X][Y]) p : R[X][Y])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := R[X][Y]) ((swap : (a : R[X][Y]) → R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X) : R[X][Y]) (Y : R[X][Y])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := R[X][Y]) ((swap : (a : R[X][Y]) → R[X][Y]) Y : R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y])

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

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
⊢ (swap : (a : R[X][Y]) → R[X][Y]) ((C : (a : R[X]) → R[X][Y]) f) = map C f

Tactic:
simpa [← algebraMap_eq] using aeval_X_left_eq_map f

Premises used: Polynomial.aeval_X_left_eq_map, Polynomial.algebraMap_eq
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X][Y]
⊢ (swap : (a : R[X][Y]) → R[X][Y]) ((swap : (a : R[X][Y]) → R[X][Y]) p) = p

Tactic:
AlgEquiv.symm_apply_apply swap p

Premises used: AlgEquiv.symm_apply_apply, Polynomial.Bivariate.swap
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
h : 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])
h_1 : 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:
aesop
-- Module: Mathlib.Algebra.Polynomial.Bivariate
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])
monomial :
  ∀ (n : ℕ) (a : R),
    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])
⊢ 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])

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]

Premises used: Polynomial.map_monomial, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.monomial, Polynomial.Bivariate.swap_Y, map_pow, Polynomial.Bivariate.swap_C_C, map_mul, Polynomial.C_mul, Polynomial.C_pow
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
f : R[X]
⊢ (swap : (a : R[X][Y]) → R[X][Y]) ((monomial n : (a : R[X]) → R[X][Y]) f) =
    HMul.hMul (β := R[X][Y]) (map C f) ((C : (a : R[X]) → R[X][Y]) (HPow.hPow (α := R[X]) X n) : R[X][Y])

Tactic:
simp [← C_mul_X_pow_eq_monomial, aeval_X_left_eq_map]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.aeval_X_left_eq_map
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
n m : ℕ
r : R
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
⊢ 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])

Tactic:
simp [← 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 : ℕ
r : R
⊢ 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:
ac_rfl
-- Module: Mathlib.Algebra.Polynomial.Bivariate
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 q : R[X][Y]
h :
  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)
h_1 :
  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:
aesop
-- Module: Mathlib.Algebra.Polynomial.Bivariate
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 :
  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)
⊢ Eq.{u_2 + 1} (α := A)
    ((aevalAeval x y : (a : R[X][Y]) → A)
        ((swap : (a : R[X][Y]) → R[X][Y]) ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) a) : R[X][Y]) :
      A)
    ((aevalAeval y x : (a : R[X][Y]) → A) ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) a : R[X][Y]) : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Bivariate
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)
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)
⊢ 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:
induction a using Polynomial.induction_on'
-- Module: Mathlib.Algebra.Polynomial.Bivariate
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 : ℕ
p q : R[X]
h :
  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)
h_1 :
  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:
aesop (add norm add_mul)

Premises used: add_mul
-- Module: Mathlib.Algebra.Polynomial.Bivariate
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 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]) ((monomial n_1 : (a : R) → R[X]) a))) *
      x ^ n =
    HMul.hMul (α := A) ((aeval y : (a : R[X]) → A) ((monomial n_1 : (a : R) → R[X]) a : R[X]) : A) (x ^ n)

Tactic:
aesop (add norm add_mul)

Premises used: add_mul
-- Module: Mathlib.Algebra.Polynomial.Bivariate
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)
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]) ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) a) : R[X][Y]) :
        A)
      ((aevalAeval y x : (a : R[X][Y]) → A) ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) a : R[X][Y]) : 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)

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)

Premises used: add_mul, Polynomial.monomial
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
x : A
p q : R[X][Y]
h :
  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])
h_1 :
  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:
aesop
-- Module: Mathlib.Algebra.Polynomial.Bivariate
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 :
  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
⊢ 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])
        ((Polynomial.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]) ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) a)) :
      A[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Bivariate
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
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
⊢ 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:
induction a using Polynomial.induction_on'
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
x : A
n : ℕ
p q : R[X]
h :
  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
h_1 :
  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:
aesop (add norm [add_mul, C_mul_X_pow_eq_monomial])

Premises used: add_mul, Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
x : A
n n_1 : ℕ
a : R
⊢ map (algebraMap R A) ((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]) ((monomial n_1 : (a : R) → R[X]) a)) *
      HPow.hPow (α := A[X]) ((C : (a : A) → A[X]) x : A[X]) n

Tactic:
aesop (add norm [add_mul, C_mul_X_pow_eq_monomial])

Premises used: add_mul, Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Bivariate
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])
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])
          ((Polynomial.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]) ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) a)) :
        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])

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])

Premises used: add_mul, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.monomial
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
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)))
⊢ 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))

Tactic:
ext i
-- Module: Mathlib.Algebra.Polynomial.Bivariate
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, ⋯⟩))))
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, ⋯⟩))))
    (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, ⋯⟩))))
⊢ 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:
fin_cases i
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
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 ((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, ⋯⟩))))

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
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 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩))))
    (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, ⋯⟩))))

Tactic:
simp