-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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)
⊢ 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)
have 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)
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]
Cleared hypotheses: x