-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
/-- The jacobian of the composition of presentations is the product of the jacobians. -/
@[simp]
lemma comp_jacobian_eq_jacobian_smul_jacobian : (Q.comp P).jacobian = P.jacobian • Q.jacobian

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
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
⊢ (Q.comp P).jacobian = P.jacobian • Q.jacobian

Tactic:
cases nonempty_fintype Q.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
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
val✝ : Fintype Q.rels
⊢ (Q.comp P).jacobian = P.jacobian • Q.jacobian

Proof state:
case intro.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
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
val✝¹ : Fintype Q.rels
val✝ : Fintype P.rels
this : Fintype (Q.comp P).rels := inferInstanceAs (Fintype (Q.rels ⊕ P.rels))
⊢ (algebraMap (Q.comp P).Ring T)
      (Matrix.fromBlocks (Q.comp P).jacobiMatrix.toBlocks₁₁ 0 (Q.comp P).jacobiMatrix.toBlocks₂₁
          (Q.comp P).jacobiMatrix.toBlocks₂₂).det =
    P.jacobian • Q.jacobian

Tactic:
convert_to
  (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det *
  (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det = P.jacobian • Q.jacobian

Result:
case h.e'_2
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
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
val✝¹ : Fintype Q.rels
val✝ : Fintype P.rels
this : Fintype (Q.comp P).rels := inferInstanceAs (Fintype (Q.rels ⊕ P.rels))
⊢ (algebraMap (Q.comp P).Ring T)
      (Matrix.fromBlocks (Q.comp P).jacobiMatrix.toBlocks₁₁ 0 (Q.comp P).jacobiMatrix.toBlocks₂₁
          (Q.comp P).jacobiMatrix.toBlocks₂₂).det =
    (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det *
      (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det

case intro.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
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
val✝¹ : Fintype Q.rels
val✝ : Fintype P.rels
this : Fintype (Q.comp P).rels := inferInstanceAs (Fintype (Q.rels ⊕ P.rels))
⊢ (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det *
      (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det =
    P.jacobian • Q.jacobian

Proof state:
case intro.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
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
val✝¹ : Fintype Q.rels
val✝ : Fintype P.rels
this : Fintype (Q.comp P).rels := inferInstanceAs (Fintype (Q.rels ⊕ P.rels))
⊢ (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det *
      (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det =
    P.jacobian • Q.jacobian

Tactic:
rw [jacobiMatrix_comp_₁₁_det, jacobiMatrix_comp_₂₂_det, mul_comm, Algebra.smul_def]

Result:
no goals

Proof state:
case h.e'_2.h.e_6.h
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
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
val✝¹ : Fintype Q.rels
val✝ : Fintype P.rels
this : Fintype (Q.comp P).rels := inferInstanceAs (Fintype (Q.rels ⊕ P.rels))
⊢ (Matrix.fromBlocks (Q.comp P).jacobiMatrix.toBlocks₁₁ 0 (Q.comp P).jacobiMatrix.toBlocks₂₁
        (Q.comp P).jacobiMatrix.toBlocks₂₂).det =
    (Q.comp P).jacobiMatrix.toBlocks₁₁.det * (Q.comp P).jacobiMatrix.toBlocks₂₂.det

Tactic:
convert Matrix.det_fromBlocks_zero₁₂ (Q.comp P).jacobiMatrix.toBlocks₁₁
  (Q.comp P).jacobiMatrix.toBlocks₂₁ (Q.comp P).jacobiMatrix.toBlocks₂₂

Result:
no goals

Proof state:
case intro.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
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
val✝¹ : Fintype Q.rels
val✝ : Fintype P.rels
⊢ (Q.comp P).jacobian = P.jacobian • Q.jacobian

Tactic:
letI : Fintype (Q.comp P).rels := inferInstanceAs <| Fintype (Q.rels ⊕ P.rels)

Result:
case intro.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
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
val✝¹ : Fintype Q.rels
val✝ : Fintype P.rels
this : Fintype (Q.comp P).rels := inferInstanceAs (Fintype (Q.rels ⊕ P.rels))
⊢ (Q.comp P).jacobian = P.jacobian • Q.jacobian

Proof state:
case h.e'_2
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
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
val✝¹ : Fintype Q.rels
val✝ : Fintype P.rels
this : Fintype (Q.comp P).rels := inferInstanceAs (Fintype (Q.rels ⊕ P.rels))
⊢ (algebraMap (Q.comp P).Ring T)
      (Matrix.fromBlocks (Q.comp P).jacobiMatrix.toBlocks₁₁ 0 (Q.comp P).jacobiMatrix.toBlocks₂₁
          (Q.comp P).jacobiMatrix.toBlocks₂₂).det =
    (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det *
      (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det

Tactic:
simp only [Generators.algebraMap_apply, ← map_mul]

Result:
case h.e'_2
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
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
val✝¹ : Fintype Q.rels
val✝ : Fintype P.rels
this : Fintype (Q.comp P).rels := inferInstanceAs (Fintype (Q.rels ⊕ P.rels))
⊢ (aeval (Q.comp P).val)
      (Matrix.fromBlocks (Q.comp P).jacobiMatrix.toBlocks₁₁ 0 (Q.comp P).jacobiMatrix.toBlocks₂₁
          (Q.comp P).jacobiMatrix.toBlocks₂₂).det =
    (aeval (Q.comp P).val) ((Q.comp P).jacobiMatrix.toBlocks₁₁.det * (Q.comp P).jacobiMatrix.toBlocks₂₂.det)

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
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
val✝ : Fintype Q.rels
⊢ (Q.comp P).jacobian = P.jacobian • Q.jacobian

Tactic:
cases nonempty_fintype P.rels

Result:
case intro.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
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
val✝¹ : Fintype Q.rels
val✝ : Fintype P.rels
⊢ (Q.comp P).jacobian = P.jacobian • Q.jacobian