-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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 : PreSubmersivePresentation R S ι σ
inst_5 : Finite σ
intro : ∀ (val : Fintype σ), Eq (α := T ⊗[R] S) (jacobian (baseChange T P)) (1 ⊗ₜ[R] P.jacobian)
intro₁ :
  ∀ (val : Fintype σ),
    Eq (α := T ⊗[R] S)
      ((algebraMap (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P))))
              (T ⊗[R] S) :
            (a : (baseChange T P).Ring) → T ⊗[R] S)
          (Matrix.det (jacobiMatrix (baseChange T P))) :
        T ⊗[R] S)
      (1 ⊗ₜ[R] (algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : T ⊗[R] S)
intro₂ :
  ∀ (val : Fintype σ)
    (h :
      Eq (α :=
        Matrix σ σ (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P)))))
        (jacobiMatrix (baseChange T P))
        ((RingHom.mapMatrix (MvPolynomial.map (algebraMap R T)) :
            (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ (MvPolynomial ι T))
          P.jacobiMatrix)),
    Eq (α := T ⊗[R] S)
      ((algebraMap (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P))))
              (T ⊗[R] S) :
            (a : (baseChange T P).Ring) → T ⊗[R] S)
          (Matrix.det (jacobiMatrix (baseChange T P))) :
        T ⊗[R] S)
      (1 ⊗ₜ[R] (algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : T ⊗[R] S)
intro₃ :
  ∀ (val : Fintype σ)
    (h :
      Eq (α :=
        Matrix σ σ (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P)))))
        (jacobiMatrix (baseChange T P))
        ((RingHom.mapMatrix (MvPolynomial.map (algebraMap R T)) :
            (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ (MvPolynomial ι T))
          P.jacobiMatrix)),
    Eq (α := T ⊗[R] S)
      (((aeval (R := R) (S₁ := T ⊗[R] S)
                (Generators.val (Presentation.toGenerators (toPresentation (baseChange T P)))) :
              MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
            (a : MvPolynomial ι R) → T ⊗[R] S)
          P.jacobiMatrix.det :
        T ⊗[R] S)
      (1 ⊗ₜ[R] (aeval P.val : (a : MvPolynomial ι R) → S) P.jacobiMatrix.det : T ⊗[R] S)
⊢ Eq (α := T ⊗[R] S) (jacobian (baseChange T P)) (1 ⊗ₜ[R] P.jacobian)

Tactic:
classical
  cases nonempty_fintype σ
  simp_rw [jacobian_eq_jacobiMatrix_det]
  have h : (baseChange T P).jacobiMatrix =
      (MvPolynomial.map (algebraMap R T)).mapMatrix P.jacobiMatrix := by
    ext i j : 1
    simp only [baseChange, jacobiMatrix_apply, Presentation.baseChange_relation,
      RingHom.mapMatrix_apply, Matrix.map_apply,
      Presentation.baseChange_toGenerators, MvPolynomial.pderiv_map]
  rw [h, ← RingHom.map_det, Generators.algebraMap_apply, aeval_map_algebraMap, P.algebraMap_apply]
  apply aeval_one_tmul

Premises used: Algebra.Generators.algebraMap_apply, Algebra.PreSubmersivePresentation.toPresentation, nonempty_fintype, MvPolynomial.aeval_map_algebraMap, RingHom.map_det, MvPolynomial.aeval_one_tmul, Algebra.Presentation.toGenerators, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det