-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
private lemma jacobiMatrix_comp_₁₁_det :
    (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det = 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
inst✝³ : DecidableEq (Q.comp P).rels
inst✝² : Fintype (Q.comp P).rels
inst✝¹ : DecidableEq Q.rels
inst✝ : Fintype Q.rels
⊢ ((aeval (Q.comp P).val).mapMatrix (Q.comp P).jacobiMatrix.toBlocks₁₁).det =
    ((algebraMap Q.Ring T).mapMatrix Q.jacobiMatrix).det

Tactic:
congr

Result:
case e_M
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
inst✝³ : DecidableEq (Q.comp P).rels
inst✝² : Fintype (Q.comp P).rels
inst✝¹ : DecidableEq Q.rels
inst✝ : Fintype Q.rels
⊢ (aeval (Q.comp P).val).mapMatrix (Q.comp P).jacobiMatrix.toBlocks₁₁ = (algebraMap Q.Ring T).mapMatrix Q.jacobiMatrix

Proof state:
case e_M.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
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝³ : DecidableEq (Q.comp P).rels
inst✝² : Fintype (Q.comp P).rels
inst✝¹ : DecidableEq Q.rels
inst✝ : Fintype Q.rels
i j : Q.rels
⊢ (aeval (Q.comp P).val).mapMatrix (Q.comp P).jacobiMatrix.toBlocks₁₁ i j =
    (algebraMap Q.Ring T).mapMatrix Q.jacobiMatrix i j

Tactic:
simp only [Matrix.map_apply, RingHom.mapMatrix_apply, ← Q.jacobiMatrix_comp_inl_inl P,
  Q.algebraMap_apply]

Result:
case e_M.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
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝³ : DecidableEq (Q.comp P).rels
inst✝² : Fintype (Q.comp P).rels
inst✝¹ : DecidableEq Q.rels
inst✝ : Fintype Q.rels
i j : Q.rels
⊢ (aeval (Q.comp P).val).mapMatrix (Q.comp P).jacobiMatrix.toBlocks₁₁ i j =
    (aeval Q.val) ((aeval (Sum.elim X (⇑C ∘ P.val))) ((Q.comp P).jacobiMatrix (Sum.inl i) (Sum.inl 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
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝³ : DecidableEq (Q.comp P).rels
inst✝² : Fintype (Q.comp P).rels
inst✝¹ : DecidableEq Q.rels
inst✝ : Fintype Q.rels
⊢ (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det = Q.jacobian

Tactic:
rw [jacobian_eq_jacobiMatrix_det, AlgHom.map_det (aeval (Q.comp P).val), RingHom.map_det]

Result:
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
inst✝³ : DecidableEq (Q.comp P).rels
inst✝² : Fintype (Q.comp P).rels
inst✝¹ : DecidableEq Q.rels
inst✝ : Fintype Q.rels
⊢ ((aeval (Q.comp P).val).mapMatrix (Q.comp P).jacobiMatrix.toBlocks₁₁).det =
    ((algebraMap Q.Ring T).mapMatrix Q.jacobiMatrix).det

Proof state:
case e_M.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
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝³ : DecidableEq (Q.comp P).rels
inst✝² : Fintype (Q.comp P).rels
inst✝¹ : DecidableEq Q.rels
inst✝ : Fintype Q.rels
i j : Q.rels
⊢ (aeval (Q.comp P).val).mapMatrix (Q.comp P).jacobiMatrix.toBlocks₁₁ i j =
    (aeval Q.val) ((aeval (Sum.elim X (⇑C ∘ P.val))) ((Q.comp P).jacobiMatrix (Sum.inl i) (Sum.inl j)))

Tactic:
apply aeval_sumElim

Result:
no goals

Proof state:
case e_M
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
inst✝³ : DecidableEq (Q.comp P).rels
inst✝² : Fintype (Q.comp P).rels
inst✝¹ : DecidableEq Q.rels
inst✝ : Fintype Q.rels
⊢ (aeval (Q.comp P).val).mapMatrix (Q.comp P).jacobiMatrix.toBlocks₁₁ = (algebraMap Q.Ring T).mapMatrix Q.jacobiMatrix

Tactic:
ext i j : 1

Result:
case e_M.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
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝³ : DecidableEq (Q.comp P).rels
inst✝² : Fintype (Q.comp P).rels
inst✝¹ : DecidableEq Q.rels
inst✝ : Fintype Q.rels
i j : Q.rels
⊢ (aeval (Q.comp P).val).mapMatrix (Q.comp P).jacobiMatrix.toBlocks₁₁ i j =
    (algebraMap Q.Ring T).mapMatrix Q.jacobiMatrix i j