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 : Finite σ
inst_8 : Finite σ'
val : Fintype σ'
val_1 : Fintype σ
intro :
  HMul.hMul (β := T) Q.jacobian
      ((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) =
    P.jacobian • Q.jacobian
intro₁ : HMul.hMul (β := T) Q.jacobian ((algebraMap S T : (a : S) → T) P.jacobian : T) = P.jacobian • Q.jacobian
intro₂ : HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) P.jacobian : T) Q.jacobian = P.jacobian • Q.jacobian
⊢ HMul.hMul (α := T) (β := 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)
      ((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) =
    P.jacobian • Q.jacobian
have intro₃ : HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) P.jacobian : T) Q.jacobian =
  HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) P.jacobian : T) Q.jacobian
Tactic: rw [jacobiMatrix_comp_₁₁_det, jacobiMatrix_comp_₂₂_det, mul_comm, Algebra.smul_def]
-- 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 : Finite σ
inst_8 : Finite σ'
⊢ jacobian (Q.comp P) = P.jacobian • Q.jacobian
have intro : ∀ (val : Fintype σ'), jacobian (Q.comp P) = P.jacobian • Q.jacobian
Tactic: classical
  cases nonempty_fintype σ'
  cases nonempty_fintype σ
  rw [jacobian_eq_jacobiMatrix_det, ← Matrix.fromBlocks_toBlocks ((Q.comp P).jacobiMatrix),
    jacobiMatrix_comp_₁₂]
  convert_to
    (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det *
    (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det = P.jacobian • Q.jacobian
  · simp only [Generators.algebraMap_apply, ← map_mul]
    congr
    convert!
      Matrix.det_fromBlocks_zero₁₂ (Q.comp P).jacobiMatrix.toBlocks₁₁
        (Q.comp P).jacobiMatrix.toBlocks₂₁ (Q.comp P).jacobiMatrix.toBlocks₂₂
  · rw [jacobiMatrix_comp_₁₁_det, jacobiMatrix_comp_₂₂_det, mul_comm, Algebra.smul_def]
-- 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 : Finite σ
inst_8 : Finite σ'
intro : ∀ (val : Fintype σ'), jacobian (Q.comp P) = P.jacobian • Q.jacobian
⊢ jacobian (Q.comp P) = P.jacobian • Q.jacobian
have intro₁ : ∀ (val : Fintype σ') (val : Fintype σ), jacobian (Q.comp P) = P.jacobian • Q.jacobian
Tactic: classical
  cases nonempty_fintype σ'
  cases nonempty_fintype σ
  rw [jacobian_eq_jacobiMatrix_det, ← Matrix.fromBlocks_toBlocks ((Q.comp P).jacobiMatrix),
    jacobiMatrix_comp_₁₂]
  convert_to
    (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det *
    (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det = P.jacobian • Q.jacobian
  · simp only [Generators.algebraMap_apply, ← map_mul]
    congr
    convert!
      Matrix.det_fromBlocks_zero₁₂ (Q.comp P).jacobiMatrix.toBlocks₁₁
        (Q.comp P).jacobiMatrix.toBlocks₂₁ (Q.comp P).jacobiMatrix.toBlocks₂₂
  · rw [jacobiMatrix_comp_₁₁_det, jacobiMatrix_comp_₂₂_det, mul_comm, Algebra.smul_def]
-- 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 : Finite σ
inst_8 : Finite σ'
intro : ∀ (val : Fintype σ'), jacobian (Q.comp P) = P.jacobian • Q.jacobian
intro₁ : ∀ (val : Fintype σ') (val : Fintype σ), jacobian (Q.comp P) = P.jacobian • Q.jacobian
⊢ jacobian (Q.comp P) = P.jacobian • Q.jacobian
have intro₂ : ∀ (val : Fintype σ') (val_1 : Fintype σ),
  (algebraMap (Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))) T : (a : (Q.comp P).Ring) → T)
      (Matrix.det
        (Matrix.fromBlocks (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) 0 (Matrix.toBlocks₂₁ (jacobiMatrix (Q.comp P)))
          (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P))))) =
    P.jacobian • Q.jacobian
Tactic: classical
  cases nonempty_fintype σ'
  cases nonempty_fintype σ
  rw [jacobian_eq_jacobiMatrix_det, ← Matrix.fromBlocks_toBlocks ((Q.comp P).jacobiMatrix),
    jacobiMatrix_comp_₁₂]
  convert_to
    (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det *
    (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det = P.jacobian • Q.jacobian
  · simp only [Generators.algebraMap_apply, ← map_mul]
    congr
    convert!
      Matrix.det_fromBlocks_zero₁₂ (Q.comp P).jacobiMatrix.toBlocks₁₁
        (Q.comp P).jacobiMatrix.toBlocks₂₁ (Q.comp P).jacobiMatrix.toBlocks₂₂
  · rw [jacobiMatrix_comp_₁₁_det, jacobiMatrix_comp_₂₂_det, mul_comm, Algebra.smul_def]
-- 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 : Finite σ
inst_8 : Finite σ'
intro : ∀ (val : Fintype σ'), jacobian (Q.comp P) = P.jacobian • Q.jacobian
intro₁ : ∀ (val : Fintype σ') (val : Fintype σ), jacobian (Q.comp P) = P.jacobian • Q.jacobian
intro₂ :
  ∀ (val : Fintype σ') (val_1 : Fintype σ),
    (algebraMap (Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))) T : (a : (Q.comp P).Ring) → T)
        (Matrix.det
          (Matrix.fromBlocks (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) 0
            (Matrix.toBlocks₂₁ (jacobiMatrix (Q.comp P))) (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P))))) =
      P.jacobian • Q.jacobian
⊢ jacobian (Q.comp P) = P.jacobian • Q.jacobian
have h : ∀ (val : Fintype σ') (val_1 : Fintype σ),
  (algebraMap (Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))) T : (a : (Q.comp P).Ring) → T)
      (Matrix.det
        (Matrix.fromBlocks (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) 0 (Matrix.toBlocks₂₁ (jacobiMatrix (Q.comp P)))
          (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P))))) =
    HMul.hMul (α := T) (β := 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)
      ((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)
Tactic: classical
  cases nonempty_fintype σ'
  cases nonempty_fintype σ
  rw [jacobian_eq_jacobiMatrix_det, ← Matrix.fromBlocks_toBlocks ((Q.comp P).jacobiMatrix),
    jacobiMatrix_comp_₁₂]
  convert_to
    (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det *
    (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det = P.jacobian • Q.jacobian
  · simp only [Generators.algebraMap_apply, ← map_mul]
    congr
    convert!
      Matrix.det_fromBlocks_zero₁₂ (Q.comp P).jacobiMatrix.toBlocks₁₁
        (Q.comp P).jacobiMatrix.toBlocks₂₁ (Q.comp P).jacobiMatrix.toBlocks₂₂
  · rw [jacobiMatrix_comp_₁₁_det, jacobiMatrix_comp_₂₂_det, mul_comm, Algebra.smul_def]
-- 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
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst_5 : Finite σ
⊢ Eq (α := T ⊗[R] S) (jacobian (baseChange T P)) (1 ⊗ₜ[R] P.jacobian)
have intro : ∀ (val : Fintype σ), Eq (α := T ⊗[R] S) (jacobian (baseChange T P)) (1 ⊗ₜ[R] P.jacobian)
Tactic: cases nonempty_fintype σ
-- 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
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst_5 : Finite σ
val : Fintype σ
⊢ Eq (α := T ⊗[R] S) (jacobian (baseChange T P)) (1 ⊗ₜ[R] P.jacobian)
have intro : Eq (α := T ⊗[R] S)
  ((algebraMap (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P))))
          (T ⊗[R] S) :
        (a : (baseChange T P).Ring) → T ⊗[R] S)
      (Matrix.det (jacobiMatrix (baseChange T P))) :
    T ⊗[R] S)
  (1 ⊗ₜ[R] (algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : T ⊗[R] S)
Tactic: simp_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
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst_5 : Finite σ
val : Fintype σ
⊢ Eq (α := Matrix σ σ (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P)))))
    (jacobiMatrix (baseChange T P))
    ((RingHom.mapMatrix (MvPolynomial.map (algebraMap R T)) :
        (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ (MvPolynomial ι T))
      P.jacobiMatrix)
have a : ∀ (i j : σ),
  Eq (α := Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P))))
    (jacobiMatrix (baseChange T P) i j)
    ((RingHom.mapMatrix (MvPolynomial.map (algebraMap R T)) :
        (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ (MvPolynomial ι T))
      P.jacobiMatrix i j)
Tactic: ext i j : 1
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (hypothesis)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst_5 : Finite σ
val : Fintype σ
⊢ Eq (α := T ⊗[R] S)
    ((algebraMap (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P))))
            (T ⊗[R] S) :
          (a : (baseChange T P).Ring) → T ⊗[R] S)
        (Matrix.det (jacobiMatrix (baseChange T P))) :
      T ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : T ⊗[R] S)
have h : Eq (α := Matrix σ σ (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P)))))
  (jacobiMatrix (baseChange T P))
  ((RingHom.mapMatrix (MvPolynomial.map (algebraMap R T)) :
      (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ (MvPolynomial ι T))
    P.jacobiMatrix)
Tactic: have h : (baseChange T P).jacobiMatrix =
      (MvPolynomial.map (algebraMap R T)).mapMatrix P.jacobiMatrix := by
    ext i j : 1
    simp only [baseChange, jacobiMatrix_apply, Presentation.baseChange_relation,
      RingHom.mapMatrix_apply, Matrix.map_apply,
      Presentation.baseChange_toGenerators, MvPolynomial.pderiv_map]
-- 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
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst_5 : Finite σ
val : Fintype σ
h :
  Eq (α := Matrix σ σ (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P)))))
    (jacobiMatrix (baseChange T P))
    ((RingHom.mapMatrix (MvPolynomial.map (algebraMap R T)) :
        (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ (MvPolynomial ι T))
      P.jacobiMatrix)
⊢ Eq (α := T ⊗[R] S)
    ((algebraMap (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P))))
            (T ⊗[R] S) :
          (a : (baseChange T P).Ring) → T ⊗[R] S)
        (Matrix.det (jacobiMatrix (baseChange T P))) :
      T ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : T ⊗[R] S)
have intro : Eq (α := T ⊗[R] S)
  (((aeval (R := R) (S₁ := T ⊗[R] S) (Generators.val (Presentation.toGenerators (toPresentation (baseChange T P)))) :
          MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
        (a : MvPolynomial ι R) → T ⊗[R] S)
      P.jacobiMatrix.det :
    T ⊗[R] S)
  (1 ⊗ₜ[R] (aeval P.val : (a : MvPolynomial ι R) → S) P.jacobiMatrix.det : T ⊗[R] S)
Tactic: rw [h, ← RingHom.map_det, Generators.algebraMap_apply, aeval_map_algebraMap, P.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
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst_5 : Finite σ
⊢ Eq (α := T ⊗[R] S) (jacobian (baseChange T P)) (1 ⊗ₜ[R] P.jacobian)
have intro : ∀ (val : Fintype σ), Eq (α := T ⊗[R] S) (jacobian (baseChange T P)) (1 ⊗ₜ[R] P.jacobian)
Tactic: classical
  cases nonempty_fintype σ
  simp_rw [jacobian_eq_jacobiMatrix_det]
  have h : (baseChange T P).jacobiMatrix =
      (MvPolynomial.map (algebraMap R T)).mapMatrix P.jacobiMatrix := by
    ext i j : 1
    simp only [baseChange, jacobiMatrix_apply, Presentation.baseChange_relation,
      RingHom.mapMatrix_apply, Matrix.map_apply,
      Presentation.baseChange_toGenerators, MvPolynomial.pderiv_map]
  rw [h, ← RingHom.map_det, Generators.algebraMap_apply, aeval_map_algebraMap, P.algebraMap_apply]
  apply aeval_one_tmul
-- 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
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst_5 : Finite σ
intro : ∀ (val : Fintype σ), Eq (α := T ⊗[R] S) (jacobian (baseChange T P)) (1 ⊗ₜ[R] P.jacobian)
⊢ Eq (α := T ⊗[R] S) (jacobian (baseChange T P)) (1 ⊗ₜ[R] P.jacobian)
have intro₁ : ∀ (val : Fintype σ),
  Eq (α := T ⊗[R] S)
    ((algebraMap (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P))))
            (T ⊗[R] S) :
          (a : (baseChange T P).Ring) → T ⊗[R] S)
        (Matrix.det (jacobiMatrix (baseChange T P))) :
      T ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : T ⊗[R] S)
Tactic: classical
  cases nonempty_fintype σ
  simp_rw [jacobian_eq_jacobiMatrix_det]
  have h : (baseChange T P).jacobiMatrix =
      (MvPolynomial.map (algebraMap R T)).mapMatrix P.jacobiMatrix := by
    ext i j : 1
    simp only [baseChange, jacobiMatrix_apply, Presentation.baseChange_relation,
      RingHom.mapMatrix_apply, Matrix.map_apply,
      Presentation.baseChange_toGenerators, MvPolynomial.pderiv_map]
  rw [h, ← RingHom.map_det, Generators.algebraMap_apply, aeval_map_algebraMap, P.algebraMap_apply]
  apply aeval_one_tmul
-- 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
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst_5 : Finite σ
intro : ∀ (val : Fintype σ), Eq (α := T ⊗[R] S) (jacobian (baseChange T P)) (1 ⊗ₜ[R] P.jacobian)
intro₁ :
  ∀ (val : Fintype σ),
    Eq (α := T ⊗[R] S)
      ((algebraMap (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P))))
              (T ⊗[R] S) :
            (a : (baseChange T P).Ring) → T ⊗[R] S)
          (Matrix.det (jacobiMatrix (baseChange T P))) :
        T ⊗[R] S)
      (1 ⊗ₜ[R] (algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : T ⊗[R] S)
⊢ Eq (α := T ⊗[R] S) (jacobian (baseChange T P)) (1 ⊗ₜ[R] P.jacobian)
have intro₂ : ∀ (val : Fintype σ)
  (h :
    Eq (α := Matrix σ σ (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P)))))
      (jacobiMatrix (baseChange T P))
      ((RingHom.mapMatrix (MvPolynomial.map (algebraMap R T)) :
          (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ (MvPolynomial ι T))
        P.jacobiMatrix)),
  Eq (α := T ⊗[R] S)
    ((algebraMap (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P))))
            (T ⊗[R] S) :
          (a : (baseChange T P).Ring) → T ⊗[R] S)
        (Matrix.det (jacobiMatrix (baseChange T P))) :
      T ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : T ⊗[R] S)
Tactic: classical
  cases nonempty_fintype σ
  simp_rw [jacobian_eq_jacobiMatrix_det]
  have h : (baseChange T P).jacobiMatrix =
      (MvPolynomial.map (algebraMap R T)).mapMatrix P.jacobiMatrix := by
    ext i j : 1
    simp only [baseChange, jacobiMatrix_apply, Presentation.baseChange_relation,
      RingHom.mapMatrix_apply, Matrix.map_apply,
      Presentation.baseChange_toGenerators, MvPolynomial.pderiv_map]
  rw [h, ← RingHom.map_det, Generators.algebraMap_apply, aeval_map_algebraMap, P.algebraMap_apply]
  apply aeval_one_tmul
-- 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
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst_5 : Finite σ
intro : ∀ (val : Fintype σ), Eq (α := T ⊗[R] S) (jacobian (baseChange T P)) (1 ⊗ₜ[R] P.jacobian)
intro₁ :
  ∀ (val : Fintype σ),
    Eq (α := T ⊗[R] S)
      ((algebraMap (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P))))
              (T ⊗[R] S) :
            (a : (baseChange T P).Ring) → T ⊗[R] S)
          (Matrix.det (jacobiMatrix (baseChange T P))) :
        T ⊗[R] S)
      (1 ⊗ₜ[R] (algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : T ⊗[R] S)
intro₂ :
  ∀ (val : Fintype σ)
    (h :
      Eq (α :=
        Matrix σ σ (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P)))))
        (jacobiMatrix (baseChange T P))
        ((RingHom.mapMatrix (MvPolynomial.map (algebraMap R T)) :
            (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ (MvPolynomial ι T))
          P.jacobiMatrix)),
    Eq (α := T ⊗[R] S)
      ((algebraMap (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P))))
              (T ⊗[R] S) :
            (a : (baseChange T P).Ring) → T ⊗[R] S)
          (Matrix.det (jacobiMatrix (baseChange T P))) :
        T ⊗[R] S)
      (1 ⊗ₜ[R] (algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : T ⊗[R] S)
⊢ Eq (α := T ⊗[R] S) (jacobian (baseChange T P)) (1 ⊗ₜ[R] P.jacobian)
have intro₃ : ∀ (val : Fintype σ)
  (h :
    Eq (α := Matrix σ σ (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P)))))
      (jacobiMatrix (baseChange T P))
      ((RingHom.mapMatrix (MvPolynomial.map (algebraMap R T)) :
          (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ (MvPolynomial ι T))
        P.jacobiMatrix)),
  Eq (α := T ⊗[R] S)
    (((aeval (R := R) (S₁ := T ⊗[R] S) (Generators.val (Presentation.toGenerators (toPresentation (baseChange T P)))) :
            MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        P.jacobiMatrix.det :
      T ⊗[R] S)
    (1 ⊗ₜ[R] (aeval P.val : (a : MvPolynomial ι R) → S) P.jacobiMatrix.det : T ⊗[R] S)
Tactic: classical
  cases nonempty_fintype σ
  simp_rw [jacobian_eq_jacobiMatrix_det]
  have h : (baseChange T P).jacobiMatrix =
      (MvPolynomial.map (algebraMap R T)).mapMatrix P.jacobiMatrix := by
    ext i j : 1
    simp only [baseChange, jacobiMatrix_apply, Presentation.baseChange_relation,
      RingHom.mapMatrix_apply, Matrix.map_apply,
      Presentation.baseChange_toGenerators, MvPolynomial.pderiv_map]
  rw [h, ← RingHom.map_det, Generators.algebraMap_apply, aeval_map_algebraMap, P.algebraMap_apply]
  apply aeval_one_tmul
-- 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
P_1 P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
⊢ Function.Injective.{u_2 + 1, u_1 + 1} (α := σ') (β := ι') ((⇑e.symm : (a : ι) → ι') ∘ P.map ∘ (⇑f : (a : σ') → σ))
have rw : Function.Injective.{u_2 + 1, t + 1} (α := σ') (β := σ) (⇑f : (a : σ') → σ)
Tactic: rw [Function.Injective.of_comp_iff e.symm.injective, Function.Injective.of_comp_iff P.map_inj]
-- 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
P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
inst_3 : Fintype σ'
inst_4 : DecidableEq σ'
inst_5 : Fintype σ
inst_6 : DecidableEq σ
⊢ (P.reindex e f).jacobiMatrix =
    Matrix.map (α := P.Ring)
      ((Matrix.reindex f.symm f.symm : (a : Matrix σ σ P.Ring) → Matrix σ' σ' P.Ring) P.jacobiMatrix)
      (⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : MvPolynomial ι R) → MvPolynomial ι' R)
have a : ∀ (i j : σ'),
  (P.reindex e f).jacobiMatrix i j =
    Matrix.map (α := P.Ring)
      ((Matrix.reindex f.symm f.symm : (a : Matrix σ σ P.Ring) → Matrix σ' σ' P.Ring) P.jacobiMatrix)
      (⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : MvPolynomial ι R) → MvPolynomial ι' R) 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
P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
inst_3 : Finite σ
inst_4 : Finite σ'
⊢ (P.reindex e f).jacobian = P.jacobian
have intro : ∀ (val : Fintype σ), (P.reindex e f).jacobian = P.jacobian
Tactic: cases nonempty_fintype σ
-- 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
P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
inst_3 : Finite σ
inst_4 : Finite σ'
val : Fintype σ
⊢ (P.reindex e f).jacobian = P.jacobian
have intro : ∀ (val : Fintype σ'), (P.reindex e f).jacobian = P.jacobian
Tactic: cases nonempty_fintype σ'