awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
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))))
    (jacobiMatrix (Q.comp P) (Sum.inl i) (Sum.inr j)) 0
have 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))))
Tactic: classical
  rw [jacobiMatrix_apply]
  refine MvPolynomial.pderiv_eq_zero_of_notMem_vars (fun hmem ↦ ?_)
  apply MvPolynomial.vars_rename at hmem
  simp at hmem
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
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))))
⊢ Eq (α := Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
    (jacobiMatrix (Q.comp P) (Sum.inl i) (Sum.inr j)) 0
have rw₃ : ∀ (hmem : map (Q.comp P) (Sum.inl i) ∈ vars (Presentation.relation (toPresentation (Q.comp P)) (Sum.inr j))), False
Tactic: classical
  rw [jacobiMatrix_apply]
  refine MvPolynomial.pderiv_eq_zero_of_notMem_vars (fun hmem ↦ ?_)
  apply MvPolynomial.vars_rename at hmem
  simp at hmem
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
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
⊢ Eq (α := Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
    (jacobiMatrix (Q.comp P) (Sum.inl i) (Sum.inr j)) 0
have rw₄ : ∀
  (hmem :
    Membership.mem (γ := Finset (ι' ⊕ ι)) (Finset.image Sum.inr (vars (P.relation j))) (map (Q.comp P) (Sum.inl i))),
  False
Tactic: classical
  rw [jacobiMatrix_apply]
  refine MvPolynomial.pderiv_eq_zero_of_notMem_vars (fun hmem ↦ ?_)
  apply MvPolynomial.vars_rename at hmem
  simp at hmem
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
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 σ'
⊢ Eq (α := Matrix σ' σ (Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))))
    (Matrix.toBlocks₁₂ (jacobiMatrix (Q.comp P))) 0
have a : ∀ (i : σ') (j : σ),
  Eq (α := Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
    (Matrix.toBlocks₁₂ (jacobiMatrix (Q.comp P)) i j) (0 i j)
Tactic: ext i j : 1
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
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 : σ'
⊢ (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
have 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)
Tactic: rw [jacobiMatrix_apply, jacobiMatrix_apply, comp_map, Sum.elim_inl,
    ← Q.comp_aeval_relation_inl P.toPresentation]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
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 σ'
⊢ (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
have 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))
Tactic: rw [jacobian_eq_jacobiMatrix_det, AlgHom.map_det (aeval (Q.comp P).val), RingHom.map_det]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
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 σ'
⊢ 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))
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
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 σ'
⊢ 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)
have 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)
Tactic: ext i j : 1
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
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)
    ((RingHom.mapMatrix (algebraMap Q.Ring T) : (a : Matrix σ' σ' Q.Ring) → Matrix σ' σ' T) Q.jacobiMatrix i j : T)
have 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)
Tactic: simp only [Matrix.map_apply, RingHom.mapMatrix_apply, ← Q.jacobiMatrix_comp_inl_inl P,
    Q.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
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))))
    (jacobiMatrix (Q.comp P) (Sum.inr i) (Sum.inr j))
    ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.jacobiMatrix i j))
have 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)
Tactic: rw [jacobiMatrix_apply, jacobiMatrix_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
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 σ'
⊢ 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)
have 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)
Tactic: rw [jacobian_eq_jacobiMatrix_det]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
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 σ'
⊢ 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)
have rw : Eq.{u_3 + 1} (α := T)
  (Matrix.det.{u_3, t} (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, t} (n := σ)
    ((RingHom.mapMatrix (algebraMap S T) : (a : Matrix σ σ S) → Matrix σ σ T)
      ((RingHom.mapMatrix (algebraMap P.Ring S) : (a : Matrix σ σ P.Ring) → Matrix σ σ S) P.jacobiMatrix)))
Tactic: rw [AlgHom.map_det (aeval (Q.comp P).val), RingHom.map_det, RingHom.map_det]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
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 σ'
⊢ Eq.{u_3 + 1} (α := T)
    (Matrix.det.{u_3, t} (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, t} (n := σ)
      ((RingHom.mapMatrix (algebraMap S T) : (a : Matrix σ σ S) → Matrix σ σ T)
        ((RingHom.mapMatrix (algebraMap P.Ring S) : (a : Matrix σ σ P.Ring) → Matrix σ σ S) P.jacobiMatrix)))
have 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 S T) : (a : Matrix σ σ S) → Matrix σ σ T)
      ((RingHom.mapMatrix (algebraMap P.Ring S) : (a : Matrix σ σ P.Ring) → Matrix σ σ S) P.jacobiMatrix) :
    Matrix σ σ T)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
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 σ'
⊢ 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 S T) : (a : Matrix σ σ S) → Matrix σ σ T)
        ((RingHom.mapMatrix (algebraMap P.Ring S) : (a : Matrix σ σ P.Ring) → Matrix σ σ S) P.jacobiMatrix) :
      Matrix σ σ T)
have 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 S T) : (a : Matrix σ σ S) → Matrix σ σ T)
        ((RingHom.mapMatrix (algebraMap P.Ring S) : (a : Matrix σ σ P.Ring) → Matrix σ σ S) P.jacobiMatrix) i j :
      T)
Tactic: ext i j : 1
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
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)
    ((RingHom.mapMatrix (algebraMap S T) : (a : Matrix σ σ S) → Matrix σ σ T)
        ((RingHom.mapMatrix (algebraMap P.Ring S) : (a : Matrix σ σ P.Ring) → Matrix σ σ S) P.jacobiMatrix) i j :
      T)
have e_M : (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P)))) : (a : MvPolynomial (ι' ⊕ ι) R) → T)
    (jacobiMatrix (Q.comp P) (Sum.inr i) (Sum.inr j) :
      Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))) =
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S))
    (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) (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]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
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 : σ
⊢ (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P)))) : (a : MvPolynomial (ι' ⊕ ι) R) → T)
      (jacobiMatrix (Q.comp P) (Sum.inr i) (Sum.inr j) :
        Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))) =
    eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S))
      (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) (P.jacobiMatrix i j)
have e_M : (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P)))) : (a : MvPolynomial (ι' ⊕ ι) R) → T)
    ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.jacobiMatrix i j) :
      MvPolynomial (ι' ⊕ ι) R) =
  eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) (P.jacobiMatrix i j)
Tactic: rw [jacobiMatrix_comp_inr_inr, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
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 : σ
⊢ eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.jacobiMatrix i j)) =
    eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) (P.jacobiMatrix i j)
have e_M : ∀ (p : P.Ring),
  eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) p) =
    eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) p
Tactic: generalize P.jacobiMatrix i j = p
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
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_1 j : σ
p : MvPolynomial ι R
i : ι
hp :
  eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) p) =
    eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) p
⊢ eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (p * X i)) =
    eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) (p * X i)
have e_M : eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) p *
    eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (X i)) =
  eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) p *
    eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) (X i)
Tactic: simp only [map_mul, eval₂_mul, hp]