-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
private lemma jacobiMatrix_comp_inl_inr (i : Q.rels) (j : P.rels) :
    (Q.comp P).jacobiMatrix (Sum.inl i) (Sum.inr j) = 0

Proof state:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_3
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
i : Q.rels
j : P.rels
⊢ (pderiv ((Q.comp P).map (Sum.inl i))) ((Q.comp P).relation (Sum.inr j)) = 0

Tactic:
refine MvPolynomial.pderiv_eq_zero_of_not_mem_vars (fun hmem ↦ ?_)

Result:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_3
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
i : Q.rels
j : P.rels
hmem : (Q.comp P).map (Sum.inl i) ∈ vars ((Q.comp P).relation (Sum.inr j))
⊢ False

Proof state:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_3
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
i : Q.rels
j : P.rels
⊢ (Q.comp P).jacobiMatrix (Sum.inl i) (Sum.inr j) = 0

Tactic:
classical
rw [jacobiMatrix_apply]
refine MvPolynomial.pderiv_eq_zero_of_not_mem_vars (fun hmem ↦ ?_)
apply MvPolynomial.vars_rename at hmem
simp at hmem

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_3
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
i : Q.rels
j : P.rels
hmem : (Q.comp P).map (Sum.inl i) ∈ Finset.image Sum.inr (vars (P.relation j))
⊢ False

Tactic:
simp at hmem

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_3
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
i : Q.rels
j : P.rels
hmem : (Q.comp P).map (Sum.inl i) ∈ vars ((Q.comp P).relation (Sum.inr j))
⊢ False

Tactic:
apply MvPolynomial.vars_rename at hmem

Result:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_3
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
i : Q.rels
j : P.rels
hmem : (Q.comp P).map (Sum.inl i) ∈ Finset.image Sum.inr (vars (P.relation j))
⊢ False

Proof state:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_3
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
i : Q.rels
j : P.rels
⊢ (Q.comp P).jacobiMatrix (Sum.inl i) (Sum.inr j) = 0

Tactic:
rw [jacobiMatrix_apply]

Result:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_3
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
i : Q.rels
j : P.rels
⊢ (pderiv ((Q.comp P).map (Sum.inl i))) ((Q.comp P).relation (Sum.inr j)) = 0