-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsStandardSmoothOfRelativeDimension n R S
this_1 : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w : _root_.Finite σ
w_1 : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e_1 : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  Equiv.trans ((Equiv.ofInjective P.map ⋯).sumCongr (Equiv.symm (Finite.equivFinOfCardEq ⋯)))
    (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  AlgEquiv.trans (AlgEquiv.symm (MvPolynomial.sumAlgEquiv R σ (Fin n))) (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e : MvPolynomial σ (MvPolynomial (Fin n) R) →ₐ[R] P.Ring).comp
    (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst_1 : Algebra.{u, v} (MvPolynomial (Fin n) R) S := toAlgebra (comp (algebraMap P.Ring S) φ.toRingHom)
scalarTowerInst : IsScalarTower.{u, u, v} (MvPolynomial (Fin n) R) P.Ring S := ⋯
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  Eq (α := RingHom.{u, v} (MvPolynomial σ (MvPolynomial (Fin n) R)) S)
    (AlgHom.toRingHom
      (MvPolynomial.aeval fun (x : σ) ↦
        (algebraMap P.Ring S : (a : P.Ring) → S)
          ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring)))
    (comp (algebraMap P.Ring S) e.toRingEquiv.toRingHom)
P' : Algebra.PreSubmersivePresentation.{0, 0, u, v} (MvPolynomial (Fin n) R) S σ σ :=
  let __Generators : Algebra.Generators.{0, u, v} (MvPolynomial (Fin n) R) S σ :=
    Algebra.Generators.ofSurjective
      (fun (x : σ) ↦
        (algebraMap P.Ring S : (a : P.Ring) → S)
          ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring))
      ⋯;
  { toGenerators := __Generators,
    relation := (⇑e.symm : (a : P.Ring) → MvPolynomial σ (MvPolynomial (Fin n) R)) ∘ P.relation,
    span_range_relation_eq_ker := ⋯, map := _root_.id, map_inj := ⋯ }
i j : σ
suffices :
  Eq (α := P.Ring)
    ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring)
        ((MvPolynomial.pderiv i :
            (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → MvPolynomial σ (MvPolynomial (Fin n) R))
          ((e.symm : (a : P.Ring) → MvPolynomial σ (MvPolynomial (Fin n) R)) (P.relation j))) :
      P.Ring)
    ((MvPolynomial.pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R)
⊢ Eq.{v + 1} (α := S)
    ((algebraMap P.Ring S : (a : P.Ring) → S)
        ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring)
            ((MvPolynomial.pderiv i :
                (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → MvPolynomial σ (MvPolynomial (Fin n) R))
              ((e.symm : (a : P.Ring) → MvPolynomial σ (MvPolynomial (Fin n) R)) (P.relation j))) :
          P.Ring) :
      S)
    ((mapMatrix (algebraMap P.Ring S) : (a : Matrix σ σ P.Ring) → Matrix σ σ S) P.jacobiMatrix i j : S)

Tactic:
suffices e ((e.symm (P.relation j)).pderiv i) = (P.relation j).pderiv (P.map i) by
        simp [Algebra.PreSubmersivePresentation.jacobiMatrix_apply, this]