awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
p q : R[X][Y]
⊢ evalEval x y (p * q) = evalEval x y p * evalEval x y q

Tactic:
simp only [evalEval, eval_mul]

Premises used: Polynomial.eval_mul, Polynomial.evalEval
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
s : Finset ι
x y : R
p : ι → R[X][Y]
⊢ evalEval x y (∏ j ∈ s, p j) = ∏ j ∈ s, evalEval x y (p j)

Tactic:
simp only [evalEval, eval_prod]

Premises used: Polynomial.eval_prod, Polynomial.evalEval
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
l : List R[X][Y]
simp :
  (List.map (Function.comp (β := R[X]) (eval x) (eval ((C : (a : R) → R[X]) y))) l).prod =
    (List.map (evalEval x y) l).prod
⊢ evalEval x y l.prod = (List.map (evalEval x y) l).prod

Tactic:
simp only [evalEval, eval_list_prod, List.map_map]

Premises used: List.map_map, Polynomial.eval_list_prod, Polynomial.evalEval
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
l : List R[X][Y]
⊢ (List.map (Function.comp (β := R[X]) (eval x) (eval ((C : (a : R) → R[X]) y))) l).prod =
    (List.map (evalEval x y) l).prod

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
l : Multiset R[X][Y]
⊢ evalEval x y l.prod = (Multiset.map (evalEval x y) l).prod

Tactic:
simp [evalEval, eval_multiset_prod, Multiset.map_map]

Premises used: Polynomial.eval_multiset_prod, Polynomial.evalEval, Multiset.map_map
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
p : R[X][Y]
n : ℕ
⊢ evalEval x y (p ^ n) = evalEval x y p ^ n

Tactic:
simp only [evalEval, eval_pow]

Premises used: Polynomial.eval_pow, Polynomial.evalEval
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
p q : R[X][Y]
⊢ p ∣ q → evalEval x y p ∣ evalEval x y q

Tactic:
eval_dvd ∘ eval_dvd

Premises used: Function.comp, Polynomial.eval_dvd
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq (α := (a : R) → R[X][Y]) (⇑(algebraMap R R[X][Y]) : (a : R) → R[X][Y]) CC

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
⊢ Eq (α := (a : R[X][Y]) → R) (⇑(evalEvalRingHom x y) : (a : R[X][Y]) → R) (evalEval x y)

Tactic:
rfl

Premises used: Polynomial.eval, rfl
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
x : R
h :
  ∀ (x_1 x_2 : R),
    Eq (α := R) ((RingHom.comp (RingHom.comp (evalEvalRingHom x x_1) C) C : (a : R) → R) x_2 : R)
      ((RingHom.comp (RingHom.comp (eval₂RingHom (evalRingHom x) x_1) C) C : (a : R) → R) x_2 : R)
h₁ :
  ∀ (x_1 : R),
    Eq (α := R) ((RingHom.comp (evalEvalRingHom x x_1) C : (a : R[X]) → R) X : R)
      ((RingHom.comp (eval₂RingHom (evalRingHom x) x_1) C : (a : R[X]) → R) X : R)
h₂ :
  ∀ (x_1 : R),
    Eq (α := R) ((evalEvalRingHom x x_1 : (a : R[X][Y]) → R) Y : R)
      ((eval₂RingHom (evalRingHom x) x_1 : (a : R[X][Y]) → R) Y : R)
⊢ Eq (α := (y : R) → R[X][Y] →+* R) (evalEvalRingHom x) (eval₂RingHom (evalRingHom x))

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
x x_1 x_2 : R
⊢ Eq (α := R) ((RingHom.comp (RingHom.comp (evalEvalRingHom x x_1) C) C : (a : R) → R) x_2 : R)
    ((RingHom.comp (RingHom.comp (eval₂RingHom (evalRingHom x) x_1) C) C : (a : R) → R) x_2 : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
x x_1 : R
⊢ Eq (α := R) ((RingHom.comp (evalEvalRingHom x x_1) C : (a : R[X]) → R) X : R)
    ((RingHom.comp (eval₂RingHom (evalRingHom x) x_1) C : (a : R[X]) → R) X : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
x x_1 : R
⊢ Eq (α := R) ((evalEvalRingHom x x_1 : (a : R[X][Y]) → R) Y : R)
    ((eval₂RingHom (evalRingHom x) x_1 : (a : R[X][Y]) → R) Y : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
x : R
h : ∀ (x_1 : R), Eq (α := (p : R[X][Y]) → R) (eval₂ (evalRingHom x) x_1) (evalEval x x_1)
⊢ Eq (α := (x : R) → (p : R[X][Y]) → R) (eval₂ (evalRingHom x)) (evalEval x)

Tactic:
ext1
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
x x_1 : R
h : Eq (α := (p : R[X][Y]) → R) (eval₂ (evalRingHom x) x_1) (⇑(evalEvalRingHom x x_1) : (a : R[X][Y]) → R)
h₁ : Eq (α := (p : R[X][Y]) → R) (eval₂ (evalRingHom x) x_1) (⇑(eval₂RingHom (evalRingHom x) x_1) : (a : R[X][Y]) → R)
h₂ h₃ : Eq (α := (p : R[X][Y]) → R) (eval₂ (evalRingHom x) x_1) (eval₂ (evalRingHom x) x_1)
⊢ Eq (α := (p : R[X][Y]) → R) (eval₂ (evalRingHom x) x_1) (evalEval x x_1)

Tactic:
rw [← coe_evalEvalRingHom, evalEvalRingHom_eq, coe_eval₂RingHom]

Premises used: Polynomial.evalEvalRingHom_eq, Polynomial.coe_eval₂RingHom, Polynomial.coe_evalEvalRingHom
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
p : R[X][Y]
rw : eval₂ (evalRingHom x) y p = evalEval x y p
rw₁ rw₂ : evalEval x y p = evalEval x y p
⊢ eval y (map (evalRingHom x) p) = evalEval x y p

Tactic:
rw [eval_map, eval₂_evalRingHom]

Premises used: Polynomial.eval_map, Polynomial.eval₂_evalRingHom
-- Module: Mathlib.Algebra.Polynomial.Bivariate
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]
rw : eval₂ (mapRingHom f) (map f q) p = map f (eval q p)
rw₁ : eval₂ (mapRingHom f) ((mapRingHom f : (a : R[X]) → S[X]) q) p = (mapRingHom f : (a : R[X]) → S[X]) (eval q p)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := S[X]) ((mapRingHom f : (a : R[X]) → S[X]) (eval q p) : S[X])
    ((mapRingHom f : (a : R[X]) → S[X]) (eval q p) : S[X])
⊢ eval (map f q) (map (mapRingHom f) p) = map f (eval q p)

Tactic:
rw [eval_map, ← coe_mapRingHom, eval₂_hom]

Premises used: Polynomial.eval_map, Polynomial.eval₂_hom, Polynomial.coe_mapRingHom
-- Module: Mathlib.Algebra.Polynomial.Bivariate
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))
rw₂ 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)
⊢ 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)

Tactic:
rw [map_mapRingHom_eval_map, eval_map, eval₂_hom]

Premises used: Polynomial.eval_map, Polynomial.eval₂_hom, Polynomial.map_mapRingHom_eval_map
-- Module: Mathlib.Algebra.Polynomial.Bivariate
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)
rw₂ 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)
⊢ 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)

Tactic:
rw [evalEval, ← map_mapRingHom_eval_map_eval, map_C]

Premises used: Polynomial.evalEval, Polynomial.map_C, Polynomial.map_mapRingHom_eval_map_eval
-- Module: Mathlib.Algebra.Polynomial.Bivariate
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)
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)
⊢ eval₂RingHom (eval₂RingHom f x) y = RingHom.comp (evalEvalRingHom x y) (mapRingHom (mapRingHom f))

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x y : S
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:
simp
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x y : S
⊢ 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:
simp
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x y : S
⊢ 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:
simp
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x y : S
p : R[X][Y]
⊢ eval₂ (eval₂RingHom f x) y p = evalEval x y (map (mapRingHom f) p)

Tactic:
congr($(eval₂RingHom_eval₂RingHom f x y) p)

Premises used: congrArg, Polynomial.eval₂RingHom_eval₂RingHom, id, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Bivariate
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)
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)
⊢ 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])

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
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:
simp
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
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:
simp
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
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:
simp
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X][Y]
⊢ eval ((C : (a : R[X]) → R[X][Y]) X)
      (eval₂ (mapRingHom (algebraMap R R[X][Y])) ((C : (a : R[X][Y]) → R[X][X][Y]) Y) p) =
    p

Tactic:
congr($eval_C_X_comp_eval₂_map_C_X p)

Premises used: congrArg, id, Polynomial.eval_C_X_comp_eval₂_map_C_X, DFunLike.coe
-- 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
f : A × 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))
      ((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))
        f) =
    f

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
f : R[X][Y] →ₐ[R] A
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)
⊢ 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

Tactic:
ext
-- 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
f : R[X][Y] →ₐ[R] A
⊢ 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:
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
f : R[X][Y] →ₐ[R] A
⊢ Eq.{u_2 + 1} (α := A)
    (((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) :
          (a : R[X][Y]) → A)
        Y :
      A)
    ((f : (a : R[X][Y]) → A) 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
xy : A × A
⊢ Eq (α := R[X][Y] →ₐ[R] A) ((aevalAevalEquiv R A : (a : A × A) → R[X][Y] →ₐ[R] A) xy : R[X][Y] →ₐ[R] A)
    (aevalAeval xy.1 xy.2 : R[X][Y] →ₐ[R] A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
A : Type u_2
inst : CommSemiring A
x y : A
h : ∀ (x_1 : A[X][Y]), (aevalAeval x y : (a : A[X][Y]) → A) x_1 = evalEval x y x_1
⊢ Eq (α := (a : A[X][Y]) → A) (⇑(aevalAeval x y) : (a : A[X][Y]) → A) (evalEval x y)

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
A : Type u_2
inst : CommSemiring A
x y : A
x_1 : A[X][Y]
⊢ (aevalAeval x y : (a : A[X][Y]) → A) x_1 = evalEval x y x_1

Tactic:
simp [aeval, aevalEquiv]

Premises used: Polynomial.aevalEquiv, Polynomial.aeval
-- 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]
⊢ Eq.{u_2 + 1} (α := A) ((aevalAeval x y : (a : R[X][Y]) → A) ((C : (a : R[X]) → R[X][Y]) p : R[X][Y]) : A)
    ((aeval x : (a : R[X]) → A) p : 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
rw : (aeval x : (a : R[X]) → A) X = x
rw₁ rw₂ : x = x
⊢ (aevalAeval x y : (a : R[X][Y]) → A) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) = x

Tactic:
rw [aevalAeval_C, aeval_X]

Premises used: Polynomial.aevalAeval_C, Polynomial.aeval_X
-- 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
⊢ (aevalAeval x y : (a : R[X][Y]) → A) Y = y

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
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])
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])
⊢ R[X][Y] ≃ₐ[R] R[X][Y]

Tactic:
apply AlgEquiv.ofAlgHom (aevalAeval (Y : R[X][Y]) (C X)) (aevalAeval (Y : R[X][Y]) (C X))

Premises used: Polynomial.C, Polynomial.aevalAeval, AlgEquiv.ofAlgHom, Polynomial.X, DFunLike.coe
-- 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
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
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:
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
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:
simp