-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
@[simp]
lemma baseChange_jacobian : (P.baseChange T).jacobian = 1 ⊗ₜ P.jacobian

Proof state:
case a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : PreSubmersivePresentation R S
val✝ : Fintype P.rels
this : Fintype (baseChange T P).rels := inferInstanceAs (Fintype P.rels)
i j : (baseChange T P).rels
⊢ (baseChange T P).jacobiMatrix i j = (MvPolynomial.map (algebraMap R T)).mapMatrix P.jacobiMatrix i j

Tactic:
simp only [baseChange, jacobiMatrix_apply, Presentation.baseChange_relation,
  RingHom.mapMatrix_apply, Matrix.map_apply]

Result:
case a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : PreSubmersivePresentation R S
val✝ : Fintype P.rels
this : Fintype (baseChange T P).rels := inferInstanceAs (Fintype P.rels)
i j : (baseChange T P).rels
⊢ (pderiv (P.map i)) ((MvPolynomial.map (algebraMap R T)) (P.relation j)) =
    (MvPolynomial.map (algebraMap R T)) ((pderiv (P.map i)) (P.relation j))

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : PreSubmersivePresentation R S
⊢ (baseChange T P).jacobian = 1 ⊗ₜ[R] P.jacobian

Tactic:
classical
cases nonempty_fintype P.rels
letI : Fintype (P.baseChange T).rels := inferInstanceAs <| Fintype P.rels
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]
  erw [MvPolynomial.pderiv_map]
  rfl
rw [h]
erw [← RingHom.map_det, aeval_map_algebraMap]
rw [P.algebraMap_apply]
apply aeval_one_tmul

Result:
no goals

Proof state:
case a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : PreSubmersivePresentation R S
val✝ : Fintype P.rels
this : Fintype (baseChange T P).rels := inferInstanceAs (Fintype P.rels)
i j : (baseChange T P).rels
⊢ (MvPolynomial.map (algebraMap R T)) ((pderiv (P.map i)) (P.relation j)) =
    (MvPolynomial.map (algebraMap R T)) ((pderiv (P.map i)) (P.relation j))

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : PreSubmersivePresentation R S
⊢ (baseChange T P).jacobian = 1 ⊗ₜ[R] P.jacobian

Tactic:
cases nonempty_fintype P.rels

Result:
case intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : PreSubmersivePresentation R S
val✝ : Fintype P.rels
⊢ (baseChange T P).jacobian = 1 ⊗ₜ[R] P.jacobian

Proof state:
case intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : PreSubmersivePresentation R S
val✝ : Fintype P.rels
⊢ (baseChange T P).jacobian = 1 ⊗ₜ[R] P.jacobian

Tactic:
letI : Fintype (P.baseChange T).rels := inferInstanceAs <| Fintype P.rels

Result:
case intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : PreSubmersivePresentation R S
val✝ : Fintype P.rels
this : Fintype (baseChange T P).rels := inferInstanceAs (Fintype P.rels)
⊢ (baseChange T P).jacobian = 1 ⊗ₜ[R] P.jacobian