-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
H :
  Eq (α := Ideal (T ⊗[R] P.Ring))
    (RingHom.ker (F := T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S)
      (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S))
    (Ideal.map (F := P.Ring →ₐ[R] T ⊗[R] P.Ring) TensorProduct.includeRight
      (RingHom.ker (F := P.Ring →ₐ[R] S) (IsScalarTower.toAlgHom R P.Ring S)))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
C :
  ∀ (a : T),
    Eq (α := T ⊗[R] S)
      (((TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S) :
            (a : T ⊗[R] MvPolynomial ι R) → T ⊗[R] S)
          ((e.symm : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R)
            ((MvPolynomial.C : (a : T) → MvPolynomial ι T) a)) :
        T ⊗[R] S)
      (((aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
              MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
            (a : MvPolynomial ι T) → T ⊗[R] S)
          ((MvPolynomial.C : (a : T) → MvPolynomial ι T) a) :
        T ⊗[R] S)
add :
  ∀ (p q : MvPolynomial ι T)
    (hp :
      Eq (α := T ⊗[R] S)
        (((TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S) :
              (a : T ⊗[R] MvPolynomial ι R) → T ⊗[R] S)
            ((e.symm : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R) p) :
          T ⊗[R] S)
        (((aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
                MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
              (a : MvPolynomial ι T) → T ⊗[R] S)
            p :
          T ⊗[R] S))
    (hq :
      Eq (α := T ⊗[R] S)
        (((TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S) :
              (a : T ⊗[R] MvPolynomial ι R) → T ⊗[R] S)
            ((e.symm : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R) q) :
          T ⊗[R] S)
        (((aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
                MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
              (a : MvPolynomial ι T) → T ⊗[R] S)
            q :
          T ⊗[R] S)),
    Eq (α := T ⊗[R] S)
      (((TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S) :
            (a : T ⊗[R] MvPolynomial ι R) → T ⊗[R] S)
          ((e.symm : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R) (p + q)) :
        T ⊗[R] S)
      (((aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
              MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
            (a : MvPolynomial ι T) → T ⊗[R] S)
          (p + q) :
        T ⊗[R] S)
mul_X :
  ∀ (p : MvPolynomial ι T) (i : ι)
    (hp :
      Eq (α := T ⊗[R] S)
        (((TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S) :
              (a : T ⊗[R] MvPolynomial ι R) → T ⊗[R] S)
            ((e.symm : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R) p) :
          T ⊗[R] S)
        (((aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
                MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
              (a : MvPolynomial ι T) → T ⊗[R] S)
            p :
          T ⊗[R] S)),
    Eq (α := T ⊗[R] S)
      (((TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S) :
            (a : T ⊗[R] MvPolynomial ι R) → T ⊗[R] S)
          ((e.symm : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R) (p * X i)) :
        T ⊗[R] S)
      (((aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
              MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
            (a : MvPolynomial ι T) → T ⊗[R] S)
          (p * X i) :
        T ⊗[R] S)
⊢ Eq (α := T ⊗[R] S)
    (((TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S) :
          (a : T ⊗[R] MvPolynomial ι R) → T ⊗[R] S)
        ((e.symm : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R) x) :
      T ⊗[R] S)
    (((aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        x :
      T ⊗[R] S)

Tactic:
induction x using MvPolynomial.induction_on with
      | C a =>
        simp only [algHom_C, TensorProduct.algebraMap_apply,
          algebraMap_self, RingHom.id_apply, e]
        rw [← MvPolynomial.algebraMap_eq, AlgEquiv.commutes]
        simp only [TensorProduct.algebraMap_apply, algebraMap_self, RingHom.id_apply,
          TensorProduct.map_tmul, AlgHom.coe_id, id_eq, map_one]
      | add p q hp hq => simp only [map_add, hp, hq]
      | mul_X p i hp => simp [hp, e]

Premises used: Algebra.TensorProduct.algebraMap_apply, RingHom.id_apply, Algebra.algebraMap_self, AlgHom.coe_id, Algebra.TensorProduct.map_tmul, AlgEquiv.commutes, map_add, MvPolynomial.induction_on, MvPolynomial.algHom_C, map_one, MvPolynomial.algebraMap_eq, MvPolynomial.C, id_eq