-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Bivariate
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : A
y : B
hx : Transcendental R x
p : R[X][Y]
add :
  ∀ (p q : R[X][Y])
    (hp :
      Eq.{u_3 + 1} (α := B)
        (((aeval ((algebraMap A B : (a : A) → B) x) : (↥R[y])[X] →ₐ[↥R[y]] B) : (a : (↥R[y])[X]) → B)
            (((aeval
                      ((C : (a : ↥R[y]) → (↥R[y])[X])
                        (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra R B) R[y] x) y ⋯)) :
                    AlgHom.{u_1, u_1, u_3} R[X] R[X][Y] (↥R[y])[X]) :
                  (a : R[X][Y]) → (↥R[y])[X])
                p :
              (↥R[y])[X]) :
          B)
        ((aeval y : (a : (↥R[x])[X]) → B)
            ((Transcendental.algEquivAdjoin hx : (a : R[X][Y]) → (↥R[x])[X]) p : (↥R[x])[X]) :
          B))
    (hq :
      Eq.{u_3 + 1} (α := B)
        (((aeval ((algebraMap A B : (a : A) → B) x) : (↥R[y])[X] →ₐ[↥R[y]] B) : (a : (↥R[y])[X]) → B)
            (((aeval
                      ((C : (a : ↥R[y]) → (↥R[y])[X])
                        (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra R B) R[y] x) y ⋯)) :
                    AlgHom.{u_1, u_1, u_3} R[X] R[X][Y] (↥R[y])[X]) :
                  (a : R[X][Y]) → (↥R[y])[X])
                q :
              (↥R[y])[X]) :
          B)
        ((aeval y : (a : (↥R[x])[X]) → B)
            ((Transcendental.algEquivAdjoin hx : (a : R[X][Y]) → (↥R[x])[X]) q : (↥R[x])[X]) :
          B)),
    Eq.{u_3 + 1} (α := B)
      (((aeval ((algebraMap A B : (a : A) → B) x) : (↥R[y])[X] →ₐ[↥R[y]] B) : (a : (↥R[y])[X]) → B)
          (((aeval
                    ((C : (a : ↥R[y]) → (↥R[y])[X])
                      (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra R B) R[y] x) y ⋯)) :
                  AlgHom.{u_1, u_1, u_3} R[X] R[X][Y] (↥R[y])[X]) :
                (a : R[X][Y]) → (↥R[y])[X])
              (p + q) :
            (↥R[y])[X]) :
        B)
      ((aeval y : (a : (↥R[x])[X]) → B)
          ((Transcendental.algEquivAdjoin hx : (a : R[X][Y]) → (↥R[x])[X]) (p + q) : (↥R[x])[X]) :
        B)
monomial :
  ∀ (n : ℕ) (a : R[X]),
    Eq.{u_3 + 1} (α := B)
      (((aeval ((algebraMap A B : (a : A) → B) x) : (↥R[y])[X] →ₐ[↥R[y]] B) : (a : (↥R[y])[X]) → B)
          (((aeval
                    ((C : (a : ↥R[y]) → (↥R[y])[X])
                      (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra R B) R[y] x) y ⋯)) :
                  AlgHom.{u_1, u_1, u_3} R[X] R[X][Y] (↥R[y])[X]) :
                (a : R[X][Y]) → (↥R[y])[X])
              ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) a) :
            (↥R[y])[X]) :
        B)
      ((aeval y : (a : (↥R[x])[X]) → B)
          ((Transcendental.algEquivAdjoin hx : (a : R[X][Y]) → (↥R[x])[X])
              ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) a) :
            (↥R[x])[X]) :
        B)
⊢ Eq.{u_3 + 1} (α := B)
    (((aeval ((algebraMap A B : (a : A) → B) x) : (↥R[y])[X] →ₐ[↥R[y]] B) : (a : (↥R[y])[X]) → B)
        (((aeval
                  ((C : (a : ↥R[y]) → (↥R[y])[X])
                    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra R B) R[y] x) y ⋯)) :
                AlgHom.{u_1, u_1, u_3} R[X] R[X][Y] (↥R[y])[X]) :
              (a : R[X][Y]) → (↥R[y])[X])
            p :
          (↥R[y])[X]) :
      B)
    ((aeval y : (a : (↥R[x])[X]) → B) ((Transcendental.algEquivAdjoin hx : (a : R[X][Y]) → (↥R[x])[X]) p : (↥R[x])[X]) :
      B)

Tactic:
induction p using Polynomial.induction_on' with
  | add p q hp hq => simp_all [map_add]
  | monomial n a =>
    simp_all [aeval_algebraMap_apply, Transcendental.algEquivAdjoin, Subalgebra.algebraMap_def]

Premises used: Polynomial.Bivariate.Transcendental.algEquivAdjoin, Subalgebra.algebraMap_def, map_add, Polynomial.monomial, Polynomial.aeval_algebraMap_apply