awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X][Y]
q : R[X]
r : R
rw :
  Eq.{u_2 + 1} (α := S) (eval ((f : (a : R) → S) r) (map f (eval q p)) : S) ((f : (a : R) → S) (eval r (eval q p)) : S)
⊢ Eq.{u_2 + 1} (α := S) (eval ((f : (a : R) → S) r) (eval (map f q) (map (mapRingHom f) p)) : S)
    ((f : (a : R) → S) (eval r (eval q p)) : S)
have rw₁ : eval₂ f ((f : (a : R) → S) r) (eval q p) = (f : (a : R) → S) (eval r (eval q p))
Tactic: rw [map_mapRingHom_eval_map, eval_map, eval₂_hom]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X][Y]
q : R[X]
r : R
rw :
  Eq.{u_2 + 1} (α := S) (eval ((f : (a : R) → S) r) (map f (eval q p)) : S) ((f : (a : R) → S) (eval r (eval q p)) : S)
rw₁ : eval₂ f ((f : (a : R) → S) r) (eval q p) = (f : (a : R) → S) (eval r (eval q p))
⊢ Eq.{u_2 + 1} (α := S) (eval ((f : (a : R) → S) r) (eval (map f q) (map (mapRingHom f) p)) : S)
    ((f : (a : R) → S) (eval r (eval q p)) : S)
have rw₂ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (eval r (eval q p)) : S) ((f : (a : R) → S) (eval r (eval q p)) : S)
Tactic: rw [map_mapRingHom_eval_map, eval_map, eval₂_hom]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X][Y]
x y : R
⊢ Eq.{u_2 + 1} (α := S) (evalEval ((f : (a : R) → S) x) ((f : (a : R) → S) y) (map (mapRingHom f) p) : S)
    ((f : (a : R) → S) (evalEval x y p) : S)
have rw : Eq.{u_2 + 1} (α := S)
  (eval ((f : (a : R) → S) x) (eval ((C : (a : S) → S[X]) ((f : (a : R) → S) y)) (map (mapRingHom f) p)) : S)
  ((f : (a : R) → S) (evalEval x y p) : S)
Tactic: rw [evalEval, ← map_mapRingHom_eval_map_eval, map_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X][Y]
x y : R
rw :
  Eq.{u_2 + 1} (α := S)
    (eval ((f : (a : R) → S) x) (eval ((C : (a : S) → S[X]) ((f : (a : R) → S) y)) (map (mapRingHom f) p)) : S)
    ((f : (a : R) → S) (evalEval x y p) : S)
⊢ Eq.{u_2 + 1} (α := S) (evalEval ((f : (a : R) → S) x) ((f : (a : R) → S) y) (map (mapRingHom f) p) : S)
    ((f : (a : R) → S) (evalEval x y p) : S)
have rw₁ : Eq.{u_2 + 1} (α := S)
  (eval ((f : (a : R) → S) x) (eval ((C : (a : S) → S[X]) ((f : (a : R) → S) y)) (map (mapRingHom f) p)) : S)
  (eval ((f : (a : R) → S) x) (eval (map f ((C : (a : R) → R[X]) y)) (map (mapRingHom f) p)) : S)
Tactic: rw [evalEval, ← map_mapRingHom_eval_map_eval, map_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X][Y]
x y : R
rw :
  Eq.{u_2 + 1} (α := S)
    (eval ((f : (a : R) → S) x) (eval ((C : (a : S) → S[X]) ((f : (a : R) → S) y)) (map (mapRingHom f) p)) : S)
    ((f : (a : R) → S) (evalEval x y p) : S)
rw₁ :
  Eq.{u_2 + 1} (α := S)
    (eval ((f : (a : R) → S) x) (eval ((C : (a : S) → S[X]) ((f : (a : R) → S) y)) (map (mapRingHom f) p)) : S)
    (eval ((f : (a : R) → S) x) (eval (map f ((C : (a : R) → R[X]) y)) (map (mapRingHom f) p)) : S)
⊢ Eq.{u_2 + 1} (α := S) (evalEval ((f : (a : R) → S) x) ((f : (a : R) → S) y) (map (mapRingHom f) p) : S)
    ((f : (a : R) → S) (evalEval x y p) : S)
have rw₂ : Eq.{u_2 + 1} (α := S)
  (eval ((f : (a : R) → S) x) (eval ((C : (a : S) → S[X]) ((f : (a : R) → S) y)) (map (mapRingHom f) p)) : S)
  (eval ((f : (a : R) → S) x) (eval ((C : (a : S) → S[X]) ((f : (a : R) → S) y)) (map (mapRingHom f) p)) : S)
Tactic: rw [evalEval, ← map_mapRingHom_eval_map_eval, map_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x y : S
⊢ eval₂RingHom (eval₂RingHom f x) y = RingHom.comp (evalEvalRingHom x y) (mapRingHom (mapRingHom f))
have h₁ : ∀ (x_1 : R),
  Eq.{u_2 + 1} (α := S) ((((eval₂RingHom (eval₂RingHom f x) y).comp C).comp C : (a : R) → S) x_1 : S)
    ((((RingHom.comp (evalEvalRingHom x y) (mapRingHom (mapRingHom f))).comp C).comp C : (a : R) → S) x_1 : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x y : S
h₁ :
  ∀ (x_1 : R),
    Eq.{u_2 + 1} (α := S) ((((eval₂RingHom (eval₂RingHom f x) y).comp C).comp C : (a : R) → S) x_1 : S)
      ((((RingHom.comp (evalEvalRingHom x y) (mapRingHom (mapRingHom f))).comp C).comp C : (a : R) → S) x_1 : S)
⊢ eval₂RingHom (eval₂RingHom f x) y = RingHom.comp (evalEvalRingHom x y) (mapRingHom (mapRingHom f))
have h₂ : Eq.{u_2 + 1} (α := S) (((eval₂RingHom (eval₂RingHom f x) y).comp C : (a : R[X]) → S) X : S)
  (((RingHom.comp (evalEvalRingHom x y) (mapRingHom (mapRingHom f))).comp C : (a : R[X]) → S) X : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x y : S
h₁ :
  ∀ (x_1 : R),
    Eq.{u_2 + 1} (α := S) ((((eval₂RingHom (eval₂RingHom f x) y).comp C).comp C : (a : R) → S) x_1 : S)
      ((((RingHom.comp (evalEvalRingHom x y) (mapRingHom (mapRingHom f))).comp C).comp C : (a : R) → S) x_1 : S)
h₂ :
  Eq.{u_2 + 1} (α := S) (((eval₂RingHom (eval₂RingHom f x) y).comp C : (a : R[X]) → S) X : S)
    (((RingHom.comp (evalEvalRingHom x y) (mapRingHom (mapRingHom f))).comp C : (a : R[X]) → S) X : S)
⊢ eval₂RingHom (eval₂RingHom f x) y = RingHom.comp (evalEvalRingHom x y) (mapRingHom (mapRingHom f))
have h₃ : Eq.{u_2 + 1} (α := S) ((eval₂RingHom (eval₂RingHom f x) y : (a : R[X][Y]) → S) Y : S)
  ((RingHom.comp (evalEvalRingHom x y) (mapRingHom (mapRingHom f)) : (a : R[X][Y]) → S) Y : S)
Tactic: ext
-- 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[X][Y])
    (@RingHom.comp _ R[X][X][Y] _ _ (Semiring.toNonAssocSemiring : NonAssocSemiring R[X][X][Y]) _
        (evalRingHom ((C : (a : R[X]) → R[X][Y]) X) : R[X][X][Y] →+* R[X][Y])
        (eval₂RingHom (mapRingHom (algebraMap R R[X][Y])) ((C : (a : R[X][Y]) → R[X][X][Y]) Y) :
          R[X][Y] →+* R[X][X][Y]) :
      R[X][Y] →+* R[X][Y])
    (RingHom.id R[X][Y] : R[X][Y] →+* R[X][Y])
have h₁ : ∀ (x : R) (n n_1 : ℕ),
  Eq.{u_1 + 1} (α := R)
    (coeff
      (coeff
        (((RingHom.comp
                (RingHom.comp
                  (@RingHom.comp _ R[X][X][Y] _ _ (Semiring.toNonAssocSemiring : NonAssocSemiring R[X][X][Y]) _
                    (evalRingHom ((C : (a : R[X]) → R[X][Y]) X) : R[X][X][Y] →+* R[X][Y])
                    (eval₂RingHom (mapRingHom (algebraMap R R[X][Y])) ((C : (a : R[X][Y]) → R[X][X][Y]) Y) :
                      R[X][Y] →+* R[X][X][Y]))
                  C)
                C :
              R →+* R[X][Y]) :
            (a : R) → R[X][Y])
          x)
        n)
      n_1)
    (coeff (coeff ((RingHom.comp (RingHom.comp (RingHom.id R[X][Y]) C) C : (a : R) → 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
h₁ :
  ∀ (x : R) (n n_1 : ℕ),
    Eq.{u_1 + 1} (α := R)
      (coeff
        (coeff
          (((RingHom.comp
                  (RingHom.comp
                    (@RingHom.comp _ R[X][X][Y] _ _ (Semiring.toNonAssocSemiring : NonAssocSemiring R[X][X][Y]) _
                      (evalRingHom ((C : (a : R[X]) → R[X][Y]) X) : R[X][X][Y] →+* R[X][Y])
                      (eval₂RingHom (mapRingHom (algebraMap R R[X][Y])) ((C : (a : R[X][Y]) → R[X][X][Y]) Y) :
                        R[X][Y] →+* R[X][X][Y]))
                    C)
                  C :
                R →+* R[X][Y]) :
              (a : R) → R[X][Y])
            x)
          n)
        n_1)
      (coeff (coeff ((RingHom.comp (RingHom.comp (RingHom.id R[X][Y]) C) C : (a : R) → R[X][Y]) x) n) n_1)
⊢ Eq.{u_1 + 1} (α := R[X][Y] →+* R[X][Y])
    (@RingHom.comp _ R[X][X][Y] _ _ (Semiring.toNonAssocSemiring : NonAssocSemiring R[X][X][Y]) _
        (evalRingHom ((C : (a : R[X]) → R[X][Y]) X) : R[X][X][Y] →+* R[X][Y])
        (eval₂RingHom (mapRingHom (algebraMap R R[X][Y])) ((C : (a : R[X][Y]) → R[X][X][Y]) Y) :
          R[X][Y] →+* R[X][X][Y]) :
      R[X][Y] →+* R[X][Y])
    (RingHom.id R[X][Y] : R[X][Y] →+* R[X][Y])
have h₂ : ∀ (n n_1 : ℕ),
  Eq.{u_1 + 1} (α := R)
    (coeff
      (coeff
        (((RingHom.comp
                (@RingHom.comp _ R[X][X][Y] _ _ (Semiring.toNonAssocSemiring : NonAssocSemiring R[X][X][Y]) _
                  (evalRingHom ((C : (a : R[X]) → R[X][Y]) X) : R[X][X][Y] →+* R[X][Y])
                  (eval₂RingHom (mapRingHom (algebraMap R R[X][Y])) ((C : (a : R[X][Y]) → R[X][X][Y]) Y) :
                    R[X][Y] →+* R[X][X][Y]))
                C :
              R[X] →+* R[X][Y]) :
            (a : R[X]) → R[X][Y])
          X)
        n)
      n_1)
    (coeff (coeff ((RingHom.comp (RingHom.id R[X][Y]) C : (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
h₁ :
  ∀ (x : R) (n n_1 : ℕ),
    Eq.{u_1 + 1} (α := R)
      (coeff
        (coeff
          (((RingHom.comp
                  (RingHom.comp
                    (@RingHom.comp _ R[X][X][Y] _ _ (Semiring.toNonAssocSemiring : NonAssocSemiring R[X][X][Y]) _
                      (evalRingHom ((C : (a : R[X]) → R[X][Y]) X) : R[X][X][Y] →+* R[X][Y])
                      (eval₂RingHom (mapRingHom (algebraMap R R[X][Y])) ((C : (a : R[X][Y]) → R[X][X][Y]) Y) :
                        R[X][Y] →+* R[X][X][Y]))
                    C)
                  C :
                R →+* R[X][Y]) :
              (a : R) → R[X][Y])
            x)
          n)
        n_1)
      (coeff (coeff ((RingHom.comp (RingHom.comp (RingHom.id R[X][Y]) C) C : (a : R) → R[X][Y]) x) n) n_1)
h₂ :
  ∀ (n n_1 : ℕ),
    Eq.{u_1 + 1} (α := R)
      (coeff
        (coeff
          (((RingHom.comp
                  (@RingHom.comp _ R[X][X][Y] _ _ (Semiring.toNonAssocSemiring : NonAssocSemiring R[X][X][Y]) _
                    (evalRingHom ((C : (a : R[X]) → R[X][Y]) X) : R[X][X][Y] →+* R[X][Y])
                    (eval₂RingHom (mapRingHom (algebraMap R R[X][Y])) ((C : (a : R[X][Y]) → R[X][X][Y]) Y) :
                      R[X][Y] →+* R[X][X][Y]))
                  C :
                R[X] →+* R[X][Y]) :
              (a : R[X]) → R[X][Y])
            X)
          n)
        n_1)
      (coeff (coeff ((RingHom.comp (RingHom.id R[X][Y]) C : (a : R[X]) → R[X][Y]) X) n) n_1)
⊢ Eq.{u_1 + 1} (α := R[X][Y] →+* R[X][Y])
    (@RingHom.comp _ R[X][X][Y] _ _ (Semiring.toNonAssocSemiring : NonAssocSemiring R[X][X][Y]) _
        (evalRingHom ((C : (a : R[X]) → R[X][Y]) X) : R[X][X][Y] →+* R[X][Y])
        (eval₂RingHom (mapRingHom (algebraMap R R[X][Y])) ((C : (a : R[X][Y]) → R[X][X][Y]) Y) :
          R[X][Y] →+* R[X][X][Y]) :
      R[X][Y] →+* R[X][Y])
    (RingHom.id R[X][Y] : R[X][Y] →+* R[X][Y])
have h₃ : ∀ (n n_1 : ℕ),
  Eq.{u_1 + 1} (α := R)
    (coeff
      (coeff
        (((@RingHom.comp _ R[X][X][Y] _ _ (Semiring.toNonAssocSemiring : NonAssocSemiring R[X][X][Y]) _
                (evalRingHom ((C : (a : R[X]) → R[X][Y]) X) : R[X][X][Y] →+* R[X][Y])
                (eval₂RingHom (mapRingHom (algebraMap R R[X][Y])) ((C : (a : R[X][Y]) → R[X][X][Y]) Y) :
                  R[X][Y] →+* R[X][X][Y]) :
              R[X][Y] →+* R[X][Y]) :
            (a : R[X][Y]) → R[X][Y])
          Y)
        n)
      n_1)
    (coeff (coeff ((RingHom.id 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_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
f : R[X][Y] →ₐ[R] A
⊢ AlgHom.comp
      ((fun (xy : A × A) ↦
          (AlgHom.comp (B := A[X]) (AlgHom.restrictScalars R (aeval xy.1))
              (let this := algebra;
              AlgHom.restrictScalars R (S := R[X]) (aeval ((C : (a : A) → A[X]) xy.2))) :
            R[X][Y] →ₐ[R] A))
        ((fun (f : R[X][Y] →ₐ[R] A) ↦
            (((f : (a : R[X][Y]) → A) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]), (f : (a : R[X][Y]) → A) Y) : A × A))
          f))
      CAlgHom =
    f.comp CAlgHom
have hX : Eq.{u_2 + 1} (α := A)
  ((AlgHom.comp
          ((fun (xy : A × A) ↦
              (AlgHom.comp (B := A[X]) (AlgHom.restrictScalars R (aeval xy.1))
                  (let this := algebra;
                  AlgHom.restrictScalars R (S := R[X]) (aeval ((C : (a : A) → A[X]) xy.2))) :
                R[X][Y] →ₐ[R] A))
            ((fun (f : R[X][Y] →ₐ[R] A) ↦
                (((f : (a : R[X][Y]) → A) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]), (f : (a : R[X][Y]) → A) Y) : A × A))
              f))
          CAlgHom :
        (a : R[X]) → A)
      X :
    A)
  ((f.comp CAlgHom : (a : R[X]) → A) X : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
A : Type u_2
inst : CommSemiring A
x y : A
⊢ Eq (α := (a : A[X][Y]) → A) (⇑(aevalAeval x y) : (a : A[X][Y]) → A) (evalEval x y)
have h : ∀ (x_1 : A[X][Y]), (aevalAeval x y : (a : A[X][Y]) → A) x_1 = evalEval x y x_1
Tactic: ext
-- 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
⊢ (aevalAeval x y : (a : R[X][Y]) → A) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) = x
have rw : (aeval x : (a : R[X]) → A) X = x
Tactic: rw [aevalAeval_C, aeval_X]
-- 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
rw : (aeval x : (a : R[X]) → A) X = x
⊢ (aevalAeval x y : (a : R[X][Y]) → A) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) = x
have rw₁ : x = x
Tactic: rw [aevalAeval_C, aeval_X]
-- 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
⊢ R[X][Y] ≃ₐ[R] R[X][Y]
have h₁ : 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: apply AlgEquiv.ofAlgHom (aevalAeval (Y : R[X][Y]) (C X)) (aevalAeval (Y : R[X][Y]) (C X))
-- 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
⊢ 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])
have 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)
Tactic: ext n m
-- 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
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)
⊢ 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])
have 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)
Tactic: ext n m
-- 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
⊢ 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])
have 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)
Tactic: ext n m
-- 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
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)
⊢ 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])
have 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)
Tactic: ext n m
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
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])
have monomial : Eq (α := R[X][Y])
  ((swap : (a : R[X][Y]) → R[X][Y]) ((monomial n : (a : R[X]) → R[X][Y]) ((C : (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: 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])
⊢ 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₁ : 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])
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])
⊢ 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₂ : 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])
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])
⊢ 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]) (β := 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))
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]