-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
private lemma jacobiMatrix_comp_₂₂_det :
    (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det = algebraMap S T P.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✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
⊢ ((aeval (Q.comp P).val).mapMatrix (Q.comp P).jacobiMatrix.toBlocks₂₂).det =
    ((algebraMap S T).mapMatrix ((algebraMap P.Ring S).mapMatrix P.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✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
⊢ (aeval (Q.comp P).val).mapMatrix (Q.comp P).jacobiMatrix.toBlocks₂₂ =
    (algebraMap S T).mapMatrix ((algebraMap P.Ring S).mapMatrix P.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✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
i j : P.rels
⊢ (aeval (Q.comp P).val) ((Q.comp P).jacobiMatrix (Sum.inr i) (Sum.inr j)) =
    eval₂ ((algebraMap S T).comp (algebraMap R S)) (fun i => (algebraMap S T) (P.val i)) (P.jacobiMatrix i j)

Tactic:
rw [jacobiMatrix_comp_inr_inr, ← IsScalarTower.algebraMap_eq]

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✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
i j : P.rels
⊢ (aeval (Q.comp P).val) ((rename Sum.inr) (P.jacobiMatrix i j)) =
    eval₂ (algebraMap R T) (fun i => (algebraMap S T) (P.val i)) (P.jacobiMatrix i j)

Proof state:
case e_M.a.h_X
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✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
i✝ j : P.rels
p : MvPolynomial P.vars R
i : P.vars
hp :
  eval₂ (algebraMap R T) (Q.comp P).val ((rename Sum.inr) p) =
    eval₂ (algebraMap R T) (fun i => (algebraMap S T) (P.val i)) p
⊢ eval₂ (algebraMap R T) (fun i => (algebraMap S T) (P.val i)) p *
      Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) (Sum.inr i) =
    eval₂ (algebraMap R T) (fun i => (algebraMap S T) (P.val i)) p * (algebraMap S T) (P.val i)

Tactic:
simp

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
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✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
⊢ (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det = (algebraMap S T) P.jacobian

Tactic:
rw [jacobian_eq_jacobiMatrix_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✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
⊢ (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det =
    (algebraMap S T) ((algebraMap P.Ring S) P.jacobiMatrix.det)

Proof state:
case e_M.a.h_C
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✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
i j : P.rels
a : R
⊢ eval₂ (algebraMap R T) (Q.comp P).val (C a) = (algebraMap R T) a

Tactic:
erw [MvPolynomial.eval₂_C]

Result:
no goals