awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Finite ι
inst_8 : Finite ι'
inst_9 : Finite σ
inst_10 : Finite σ'
this : Nat.card σ ≤ Nat.card ι
⊢ Nat.card σ' ≤ Nat.card ι'

Tactic:
have : Nat.card σ' ≤ Nat.card ι' :=
    card_relations_le_card_vars_of_isFinite Q
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Finite ι
inst_8 : Finite ι'
inst_9 : Finite σ
inst_10 : Finite σ'
this_1 : Nat.card σ ≤ Nat.card ι
this : Nat.card σ' ≤ Nat.card ι'
simp : Nat.card ι' + Nat.card ι - (Nat.card σ' + Nat.card σ) = Nat.card ι' - Nat.card σ' + (Nat.card ι - Nat.card σ)
⊢ Nat.card (ι' ⊕ ι) - Nat.card (σ' ⊕ σ) = Nat.card ι' - Nat.card σ' + (Nat.card ι - Nat.card σ)

Tactic:
simp only [Nat.card_sum]

Premises used: Nat.card_sum
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Finite ι
inst_8 : Finite ι'
inst_9 : Finite σ
inst_10 : Finite σ'
this_1 : Nat.card σ ≤ Nat.card ι
this : Nat.card σ' ≤ Nat.card ι'
⊢ Nat.card ι' + Nat.card ι - (Nat.card σ' + Nat.card σ) = Nat.card ι' - Nat.card σ' + (Nat.card ι - Nat.card σ)

Tactic:
lia
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Fintype σ
inst_8 : Fintype σ'
i : σ'
j : σ
rw :
  Eq (α := Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
    ((pderiv (map (Q.comp P) (Sum.inl i)) : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial (ι' ⊕ ι) R)
        (Presentation.relation (toPresentation (Q.comp P)) (Sum.inr j)) :
      MvPolynomial (ι' ⊕ ι) R)
    (0 : Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
⊢ Eq (α := Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
    (jacobiMatrix (Q.comp P) (Sum.inl i) (Sum.inr j)) 0

Tactic:
rw [jacobiMatrix_apply]

Premises used: Algebra.PreSubmersivePresentation.jacobiMatrix_apply
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Fintype σ
inst_8 : Fintype σ'
i : σ'
j : σ
⊢ Eq (α := Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
    ((pderiv (map (Q.comp P) (Sum.inl i)) : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial (ι' ⊕ ι) R)
        (Presentation.relation (toPresentation (Q.comp P)) (Sum.inr j)) :
      MvPolynomial (ι' ⊕ ι) R)
    (0 : Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))

Tactic:
MvPolynomial.pderiv_eq_zero_of_notMem_vars (fun hmem ↦ ?_)

Premises used: MvPolynomial.pderiv_eq_zero_of_notMem_vars
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Fintype σ
inst_8 : Fintype σ'
i : σ'
j : σ
refine :
  ∀ (hmem : map (Q.comp P) (Sum.inl i) ∈ vars (Presentation.relation (toPresentation (Q.comp P)) (Sum.inr j))), False
⊢ Eq (α := Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
    ((pderiv (map (Q.comp P) (Sum.inl i)) : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial (ι' ⊕ ι) R)
        (Presentation.relation (toPresentation (Q.comp P)) (Sum.inr j)) :
      MvPolynomial (ι' ⊕ ι) R)
    (0 : Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))

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

Premises used: MvPolynomial.pderiv_eq_zero_of_notMem_vars
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Fintype σ
inst_8 : Fintype σ'
i : σ'
j : σ
hmem : map (Q.comp P) (Sum.inl i) ∈ vars (Presentation.relation (toPresentation (Q.comp P)) (Sum.inr j))
⊢ Membership.mem (γ := Finset (ι' ⊕ ι)) (Finset.image Sum.inr (vars (P.relation j))) (map (Q.comp P) (Sum.inl i))

Tactic:
apply MvPolynomial.vars_rename at hmem

Premises used: MvPolynomial.vars_rename
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Fintype σ
inst_8 : Fintype σ'
i : σ'
j : σ
hmem : Membership.mem (γ := Finset (ι' ⊕ ι)) (Finset.image Sum.inr (vars (P.relation j))) (map (Q.comp P) (Sum.inl i))
⊢ False

Tactic:
simp at hmem
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Fintype σ
inst_8 : Fintype σ'
i : σ'
j : σ
rw rw₁ rw₂ :
  Eq (α := Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
    ((pderiv (map (Q.comp P) (Sum.inl i)) : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial (ι' ⊕ ι) R)
        (Presentation.relation (toPresentation (Q.comp P)) (Sum.inr j)) :
      MvPolynomial (ι' ⊕ ι) R)
    (0 : Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
rw₃ :
  ∀ (hmem : map (Q.comp P) (Sum.inl i) ∈ vars (Presentation.relation (toPresentation (Q.comp P)) (Sum.inr j))), False
rw₄ :
  ∀
    (hmem :
      Membership.mem (γ := Finset (ι' ⊕ ι)) (Finset.image Sum.inr (vars (P.relation j))) (map (Q.comp P) (Sum.inl i))),
    False
⊢ Eq (α := Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
    (jacobiMatrix (Q.comp P) (Sum.inl i) (Sum.inr j)) 0

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

Premises used: Algebra.PreSubmersivePresentation.jacobiMatrix_apply, MvPolynomial.pderiv_eq_zero_of_notMem_vars, MvPolynomial.vars_rename
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Fintype σ
inst_8 : Fintype σ'
a :
  ∀ (i : σ') (j : σ),
    Eq (α := Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
      (Matrix.toBlocks₁₂ (jacobiMatrix (Q.comp P)) i j) (0 i j)
⊢ Eq (α := Matrix σ' σ (Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))))
    (Matrix.toBlocks₁₂ (jacobiMatrix (Q.comp P))) 0

Tactic:
ext i j : 1
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Fintype σ
inst_8 : Fintype σ'
i : σ'
j : σ
⊢ Eq (α := Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
    (Matrix.toBlocks₁₂ (jacobiMatrix (Q.comp P)) i j) (0 i j)

Tactic:
simp [Matrix.toBlocks₁₂, jacobiMatrix_comp_inl_inr]

Premises used: _private.0.Algebra.PreSubmersivePresentation.jacobiMatrix_comp_inl_inr, Matrix.toBlocks₁₂
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Fintype σ
inst_8 : Fintype σ'
i j : σ'
rw :
  Eq (α := MvPolynomial ι' S)
    ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val)) :
          (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S)
        ((pderiv (Sum.inl (Q.map j)) : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial (ι' ⊕ ι) R)
          (Presentation.relation (toPresentation (Q.comp P)) (Sum.inl i))) :
      MvPolynomial ι' S)
    ((pderiv (Q.map j) : (a : MvPolynomial ι' S) → MvPolynomial ι' S)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val)) :
            (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S)
          (Presentation.relation (Q.comp P.toPresentation) (Sum.inl i))) :
      MvPolynomial ι' S)
⊢ (aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val)) : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S)
      (jacobiMatrix (Q.comp P) (Sum.inl j) (Sum.inl i)) =
    Q.jacobiMatrix j i

Tactic:
rw [jacobiMatrix_apply, jacobiMatrix_apply, comp_map, Sum.elim_inl,
    ← Q.comp_aeval_relation_inl P.toPresentation]

Premises used: Algebra.Presentation.comp_aeval_relation_inl, Algebra.PreSubmersivePresentation.jacobiMatrix_apply, Algebra.PreSubmersivePresentation.toPresentation, Algebra.PreSubmersivePresentation.comp_map, Sum.elim_inl
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Fintype σ
inst_8 : Fintype σ'
i j : σ'
⊢ Eq (α := MvPolynomial ι' S)
    ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val)) :
          (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S)
        ((pderiv (Sum.inl (Q.map j)) : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial (ι' ⊕ ι) R)
          (Presentation.relation (toPresentation (Q.comp P)) (Sum.inl i))) :
      MvPolynomial ι' S)
    ((pderiv (Q.map j) : (a : MvPolynomial ι' S) → MvPolynomial ι' S)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val)) :
            (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S)
          (Presentation.relation (Q.comp P.toPresentation) (Sum.inl i))) :
      MvPolynomial ι' S)

Tactic:
apply aeval_sumElim_pderiv_inl

Premises used: MvPolynomial.aeval_sumElim_pderiv_inl
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Fintype σ
inst_8 : Fintype σ'
rw :
  Eq.{u_3 + 1} (α := T)
    (Matrix.det.{u_3, u_2} (n := σ')
      ((AlgHom.mapMatrix (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))) :
          (a : Matrix σ' σ' (MvPolynomial (ι' ⊕ ι) R)) → Matrix σ' σ' T)
        (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P)))))
    (Matrix.det.{u_3, u_2} (n := σ')
      ((RingHom.mapMatrix (algebraMap Q.Ring T) : (a : Matrix σ' σ' Q.Ring) → Matrix σ' σ' T) Q.jacobiMatrix))
⊢ (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P)))) : (a : MvPolynomial (ι' ⊕ ι) R) → T)
      (Matrix.det (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) :
        Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))) =
    Q.jacobian

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

Premises used: MvPolynomial.aeval, Algebra.PreSubmersivePresentation.toPresentation, AlgHom.map_det, RingHom.map_det, Algebra.PreSubmersivePresentation.comp, Algebra.Generators.val, Algebra.Presentation.toGenerators, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Fintype σ
inst_8 : Fintype σ'
e_M :
  Eq (α := Matrix σ' σ' T)
    ((AlgHom.mapMatrix (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))) :
          (a : Matrix σ' σ' (MvPolynomial (ι' ⊕ ι) R)) → Matrix σ' σ' T)
        (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) :
      Matrix σ' σ' T)
    ((RingHom.mapMatrix (algebraMap Q.Ring T) : (a : Matrix σ' σ' Q.Ring) → Matrix σ' σ' T) Q.jacobiMatrix :
      Matrix σ' σ' T)
⊢ Eq.{u_3 + 1} (α := T)
    (Matrix.det.{u_3, u_2} (n := σ')
      ((AlgHom.mapMatrix (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))) :
          (a : Matrix σ' σ' (MvPolynomial (ι' ⊕ ι) R)) → Matrix σ' σ' T)
        (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P)))))
    (Matrix.det.{u_3, u_2} (n := σ')
      ((RingHom.mapMatrix (algebraMap Q.Ring T) : (a : Matrix σ' σ' Q.Ring) → Matrix σ' σ' T) Q.jacobiMatrix))

Tactic:
congr
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Fintype σ
inst_8 : Fintype σ'
e_M :
  ∀ (i j : σ'),
    Eq.{u_3 + 1} (α := T)
      ((AlgHom.mapMatrix (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))) :
            (a : Matrix σ' σ' (MvPolynomial (ι' ⊕ ι) R)) → Matrix σ' σ' T)
          (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) i j :
        T)
      ((RingHom.mapMatrix (algebraMap Q.Ring T) : (a : Matrix σ' σ' Q.Ring) → Matrix σ' σ' T) Q.jacobiMatrix i j : T)
⊢ Eq (α := Matrix σ' σ' T)
    ((AlgHom.mapMatrix (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))) :
          (a : Matrix σ' σ' (MvPolynomial (ι' ⊕ ι) R)) → Matrix σ' σ' T)
        (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) :
      Matrix σ' σ' T)
    ((RingHom.mapMatrix (algebraMap Q.Ring T) : (a : Matrix σ' σ' Q.Ring) → Matrix σ' σ' T) Q.jacobiMatrix :
      Matrix σ' σ' T)

Tactic:
ext i j : 1
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Fintype σ
inst_8 : Fintype σ'
i j : σ'
e_M :
  Eq.{u_3 + 1} (α := T)
    ((AlgHom.mapMatrix (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))) :
          (a : Matrix σ' σ' (MvPolynomial (ι' ⊕ ι) R)) → Matrix σ' σ' T)
        (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) i j :
      T)
    ((aeval Q.val : (a : MvPolynomial ι' S) → T)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val)) :
              (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S)
            (jacobiMatrix (Q.comp P) (Sum.inl i) (Sum.inl j)) :
          MvPolynomial ι' S) :
      T)
⊢ Eq.{u_3 + 1} (α := T)
    ((AlgHom.mapMatrix (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))) :
          (a : Matrix σ' σ' (MvPolynomial (ι' ⊕ ι) R)) → Matrix σ' σ' T)
        (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) i j :
      T)
    ((RingHom.mapMatrix (algebraMap Q.Ring T) : (a : Matrix σ' σ' Q.Ring) → Matrix σ' σ' T) Q.jacobiMatrix i j : T)

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

Premises used: RingHom.mapMatrix_apply, Algebra.Generators.algebraMap_apply, Matrix.map_apply, Algebra.PreSubmersivePresentation.toPresentation, _private.0.Algebra.PreSubmersivePresentation.jacobiMatrix_comp_inl_inl, Algebra.Presentation.toGenerators
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Fintype σ
inst_8 : Fintype σ'
i j : σ'
⊢ Eq.{u_3 + 1} (α := T)
    ((AlgHom.mapMatrix (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))) :
          (a : Matrix σ' σ' (MvPolynomial (ι' ⊕ ι) R)) → Matrix σ' σ' T)
        (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) i j :
      T)
    ((aeval Q.val : (a : MvPolynomial ι' S) → T)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val)) :
              (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S)
            (jacobiMatrix (Q.comp P) (Sum.inl i) (Sum.inl j)) :
          MvPolynomial ι' S) :
      T)

Tactic:
apply aeval_sumElim

Premises used: MvPolynomial.aeval_sumElim
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Fintype σ
inst_8 : Fintype σ'
i j : σ
rw :
  Eq (α := Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
    ((pderiv (map (Q.comp P) (Sum.inr i)) : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial (ι' ⊕ ι) R)
        (Presentation.relation (toPresentation (Q.comp P)) (Sum.inr j)) :
      MvPolynomial (ι' ⊕ ι) R)
    ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R)
        ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j)) :
      MvPolynomial (ι' ⊕ ι) R)
⊢ Eq (α := Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
    (jacobiMatrix (Q.comp P) (Sum.inr i) (Sum.inr j))
    ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.jacobiMatrix i j))

Tactic:
rw [jacobiMatrix_apply, jacobiMatrix_apply]

Premises used: Algebra.PreSubmersivePresentation.jacobiMatrix_apply
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Fintype σ
inst_8 : Fintype σ'
i j : σ
⊢ Eq (α := Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
    ((pderiv (Sum.inr (P.map i)) : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial (ι' ⊕ ι) R)
        (Presentation.relation (toPresentation (Q.comp P)) (Sum.inr j)) :
      MvPolynomial (ι' ⊕ ι) R)
    ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R)
        ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j)) :
      MvPolynomial (ι' ⊕ ι) R)

Tactic:
apply pderiv_rename Sum.inr_injective

Premises used: Sum.inr_injective, MvPolynomial.pderiv_rename
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Fintype σ
inst_8 : Fintype σ'
rw :
  Eq.{u_3 + 1} (α := T)
    ((aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P)))) :
          (a : MvPolynomial (ι' ⊕ ι) R) → T)
        (Matrix.det (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P))) :
          Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))) :
      T)
    ((algebraMap S T : (a : S) → T) ((algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : S) : T)
⊢ Eq.{u_3 + 1} (α := T)
    ((aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P)))) :
          (a : MvPolynomial (ι' ⊕ ι) R) → T)
        (Matrix.det (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P))) :
          Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))) :
      T)
    ((algebraMap S T : (a : S) → T) P.jacobian : T)

Tactic:
rw [jacobian_eq_jacobiMatrix_det]

Premises used: Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det