-- 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:
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 ((rename Sum.inr) (C a)) =
    eval₂ (algebraMap R T) (fun i => (algebraMap S T) (P.val i)) (C a)

Tactic:
simp only [algHom_C, algebraMap_eq, eval₂_C]

Result:
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

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) ((algebraMap P.Ring S) P.jacobiMatrix.det)

Tactic:
rw [AlgHom.map_det (aeval (Q.comp P).val), RingHom.map_det, 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✝¹ : 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

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
p : P.Ring
⊢ 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

Tactic:
induction' p using MvPolynomial.induction_on with a p q hp hq p i hp

Result:
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 ((rename Sum.inr) (C a)) =
    eval₂ (algebraMap R T) (fun i => (algebraMap S T) (P.val i)) (C a)

case e_M.a.h_add
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 q : MvPolynomial P.vars R
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
hq :
  eval₂ (algebraMap R T) (Q.comp P).val ((rename Sum.inr) q) =
    eval₂ (algebraMap R T) (fun i => (algebraMap S T) (P.val i)) q
⊢ eval₂ (algebraMap R T) (Q.comp P).val ((rename Sum.inr) (p + q)) =
    eval₂ (algebraMap R T) (fun i => (algebraMap S T) (P.val i)) (p + q)

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) (Q.comp P).val ((rename Sum.inr) (p * X i)) =
    eval₂ (algebraMap R T) (fun i => (algebraMap S T) (P.val i)) (p * X i)

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) (Q.comp P).val ((rename Sum.inr) (p * X i)) =
    eval₂ (algebraMap R T) (fun i => (algebraMap S T) (P.val i)) (p * X i)

Tactic:
simp only [map_mul, rename_X, eval₂_mul, hp, eval₂_X]

Result:
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 * (Q.comp P).val (Sum.inr i) =
    eval₂ (algebraMap R T) (fun i => (algebraMap S T) (P.val i)) p * (algebraMap S T) (P.val i)