-- 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_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)

Tactic:
erw [Generators.comp_val]

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 *
      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)

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✝¹ : 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)

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

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
⊢ eval₂ (algebraMap R T) (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)

Tactic:
generalize P.jacobiMatrix i j = p

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

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).mapMatrix (Q.comp P).jacobiMatrix.toBlocks₂₂ i j =
    (algebraMap S T).mapMatrix ((algebraMap P.Ring S).mapMatrix P.jacobiMatrix) i j

Tactic:
simp only [Matrix.toBlocks₂₂, AlgHom.mapMatrix_apply, Matrix.map_apply, Matrix.of_apply,
  RingHom.mapMatrix_apply, Generators.algebraMap_apply, map_aeval, coe_eval₂Hom]

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) ((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)

Proof state:
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)

Tactic:
simp [hp, hq]

Result:
no goals

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

Tactic:
simp only [aeval, AlgHom.coe_mk, coe_eval₂Hom]

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
⊢ eval₂ (algebraMap R T) (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)