-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T_1 : Type ?u.65480
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
P : Generators R S ι
a : T
b : S
X : P.Ring := P.σ b
y : P.Ring
C :
  ∀ (a : R),
    Eq (α := T ⊗[R] S)
      (((aeval (R := R) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
            (a : MvPolynomial ι R) → T ⊗[R] S)
          ((MvPolynomial.C : (a : R) → MvPolynomial ι R) a) :
        T ⊗[R] S)
      (1 ⊗ₜ[R]
          (aeval fun (x : ι) ↦ P.val x : (a : MvPolynomial ι R) → S)
            ((MvPolynomial.C : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R) :
        T ⊗[R] S)
add :
  ∀ (p q : MvPolynomial ι R)
    (hp :
      Eq (α := T ⊗[R] S)
        (((aeval (R := R) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
              (a : MvPolynomial ι R) → T ⊗[R] S)
            p :
          T ⊗[R] S)
        (1 ⊗ₜ[R] (aeval fun (x : ι) ↦ P.val x : (a : MvPolynomial ι R) → S) p : T ⊗[R] S))
    (hq :
      Eq (α := T ⊗[R] S)
        (((aeval (R := R) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
              (a : MvPolynomial ι R) → T ⊗[R] S)
            q :
          T ⊗[R] S)
        (1 ⊗ₜ[R] (aeval fun (x : ι) ↦ P.val x : (a : MvPolynomial ι R) → S) q : T ⊗[R] S)),
    Eq (α := T ⊗[R] S)
      (((aeval (R := R) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
            (a : MvPolynomial ι R) → T ⊗[R] S)
          (p + q) :
        T ⊗[R] S)
      (1 ⊗ₜ[R] (aeval fun (x : ι) ↦ P.val x : (a : MvPolynomial ι R) → S) (p + q) : T ⊗[R] S)
mul_X :
  ∀ (p : MvPolynomial ι R) (i : ι)
    (hp :
      Eq (α := T ⊗[R] S)
        (((aeval (R := R) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
              (a : MvPolynomial ι R) → T ⊗[R] S)
            p :
          T ⊗[R] S)
        (1 ⊗ₜ[R] (aeval fun (x : ι) ↦ P.val x : (a : MvPolynomial ι R) → S) p : T ⊗[R] S)),
    Eq (α := T ⊗[R] S)
      (((aeval (R := R) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
            (a : MvPolynomial ι R) → T ⊗[R] S)
          (p * MvPolynomial.X i) :
        T ⊗[R] S)
      (1 ⊗ₜ[R] (aeval fun (x : ι) ↦ P.val x : (a : MvPolynomial ι R) → S) (p * MvPolynomial.X i) : T ⊗[R] S)
⊢ Eq (α := T ⊗[R] S)
    (((aeval (R := R) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        y :
      T ⊗[R] S)
    (1 ⊗ₜ[R] (aeval fun (x : ι) ↦ P.val x : (a : MvPolynomial ι R) → S) y : T ⊗[R] S)

Tactic:
induction y using MvPolynomial.induction_on with
      | C a =>
        rw [aeval_C, aeval_C, TensorProduct.algebraMap_apply, algebraMap_eq_smul_one, smul_tmul,
          algebraMap_eq_smul_one]
      | add p q hp hq => simp [map_add, tmul_add, hp, hq]
      | mul_X p i hp => simp [hp]

Premises used: TensorProduct.smul_tmul, Algebra.TensorProduct.algebraMap_apply, map_add, MvPolynomial.induction_on, Algebra.algebraMap_eq_smul_one, MvPolynomial.aeval_C, TensorProduct.tmul_add, MvPolynomial.C