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
P : PreSubmersivePresentation R S ι σ
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
inst_5 : Finite σ
val : Fintype σ
⊢ (P.ofAlgEquiv e).jacobian = (e : (a : S) → T) P.jacobian
have intro : Eq.{u_1 + 1} (α := T)
  ((algebraMap (P.ofAlgEquiv e).Ring T : (a : (P.ofAlgEquiv e).Ring) → T) (P.ofAlgEquiv e).jacobiMatrix.det : T)
  ((e : (a : S) → T) ((algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : S) : T)
Tactic: rw [jacobian_eq_jacobiMatrix_det, 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
P : PreSubmersivePresentation R S ι σ
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
inst_5 : Finite σ
val : Fintype σ
⊢ Eq.{u_1 + 1} (α := T)
    ((algebraMap (P.ofAlgEquiv e).Ring T : (a : (P.ofAlgEquiv e).Ring) → T) (P.ofAlgEquiv e).jacobiMatrix.det : T)
    ((e : (a : S) → T) ((algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : S) : T)
have intro : Eq.{u_1 + 1} (α := T)
  ((aeval ((⇑(↑e : S →ₐ[R] T) : (a : S) → T) ∘ P.val) : (a : MvPolynomial ι R) → T) P.jacobiMatrix.det : T)
  ((aeval fun (i : ι) ↦ ((↑e : S →ₐ[R] T) : (a : S) → T) (P.val i) : (a : MvPolynomial ι R) → T) P.jacobiMatrix.det : T)
Tactic: simp only [ofAlgEquiv_toPresentation, Presentation.ofAlgEquiv_toGenerators,
    jacobiMatrix_ofAlgEquiv, Generators.algebraMap_apply, Generators.ofAlgEquiv_val,
    ← AlgHom.coe_coe e, MvPolynomial.comp_aeval_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
P : PreSubmersivePresentation R S ι σ
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
inst_5 : Finite σ
⊢ (P.ofAlgEquiv e).jacobian = (e : (a : S) → T) P.jacobian
have intro : ∀ (val : Fintype σ), (P.ofAlgEquiv e).jacobian = (e : (a : S) → T) P.jacobian
Tactic: classical
  cases nonempty_fintype σ
  rw [jacobian_eq_jacobiMatrix_det, jacobian_eq_jacobiMatrix_det]
  simp only [ofAlgEquiv_toPresentation, Presentation.ofAlgEquiv_toGenerators,
    jacobiMatrix_ofAlgEquiv, Generators.algebraMap_apply, Generators.ofAlgEquiv_val,
    ← AlgHom.coe_coe e, MvPolynomial.comp_aeval_apply]
  simp [Function.comp_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
P : PreSubmersivePresentation R S ι σ
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
inst_5 : Finite σ
intro : ∀ (val : Fintype σ), (P.ofAlgEquiv e).jacobian = (e : (a : S) → T) P.jacobian
⊢ (P.ofAlgEquiv e).jacobian = (e : (a : S) → T) P.jacobian
have intro₁ : ∀ (val : Fintype σ),
  Eq.{u_1 + 1} (α := T)
    ((algebraMap (P.ofAlgEquiv e).Ring T : (a : (P.ofAlgEquiv e).Ring) → T) (P.ofAlgEquiv e).jacobiMatrix.det : T)
    ((e : (a : S) → T) ((algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : S) : T)
Tactic: classical
  cases nonempty_fintype σ
  rw [jacobian_eq_jacobiMatrix_det, jacobian_eq_jacobiMatrix_det]
  simp only [ofAlgEquiv_toPresentation, Presentation.ofAlgEquiv_toGenerators,
    jacobiMatrix_ofAlgEquiv, Generators.algebraMap_apply, Generators.ofAlgEquiv_val,
    ← AlgHom.coe_coe e, MvPolynomial.comp_aeval_apply]
  simp [Function.comp_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
P : PreSubmersivePresentation R S ι σ
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
inst_5 : Finite σ
intro : ∀ (val : Fintype σ), (P.ofAlgEquiv e).jacobian = (e : (a : S) → T) P.jacobian
intro₁ :
  ∀ (val : Fintype σ),
    Eq.{u_1 + 1} (α := T)
      ((algebraMap (P.ofAlgEquiv e).Ring T : (a : (P.ofAlgEquiv e).Ring) → T) (P.ofAlgEquiv e).jacobiMatrix.det : T)
      ((e : (a : S) → T) ((algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : S) : T)
⊢ (P.ofAlgEquiv e).jacobian = (e : (a : S) → T) P.jacobian
have intro₂ : ∀ (val : Fintype σ),
  Eq.{u_1 + 1} (α := T)
    ((aeval ((⇑(↑e : S →ₐ[R] T) : (a : S) → T) ∘ P.val) : (a : MvPolynomial ι R) → T) P.jacobiMatrix.det : T)
    ((aeval fun (i : ι) ↦ ((↑e : S →ₐ[R] T) : (a : S) → T) (P.val i) : (a : MvPolynomial ι R) → T) P.jacobiMatrix.det :
      T)
Tactic: classical
  cases nonempty_fintype σ
  rw [jacobian_eq_jacobiMatrix_det, jacobian_eq_jacobiMatrix_det]
  simp only [ofAlgEquiv_toPresentation, Presentation.ofAlgEquiv_toGenerators,
    jacobiMatrix_ofAlgEquiv, Generators.algebraMap_apply, Generators.ofAlgEquiv_val,
    ← AlgHom.coe_coe e, MvPolynomial.comp_aeval_apply]
  simp [Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Eq (α := Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
    ((RingHom.mapMatrix (algebraMap (ofBijectiveAlgebraMap h).Ring S) :
          (a : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} (ofBijectiveAlgebraMap h).Ring) →
            Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
        (ofBijectiveAlgebraMap h).jacobiMatrix :
      Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
    (1 : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
have a : ∀ (i j : PEmpty.{u_1 + 1}),
  Eq.{v + 1} (α := S)
    ((RingHom.mapMatrix (algebraMap (ofBijectiveAlgebraMap h).Ring S) :
          (a : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} (ofBijectiveAlgebraMap h).Ring) →
            Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
        (ofBijectiveAlgebraMap h).jacobiMatrix i j :
      S)
    (1 i j : S)
Tactic: ext (i j : PEmpty)
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ (ofBijectiveAlgebraMap h).jacobian = 1
have this : Eq (α := Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
  ((RingHom.mapMatrix (algebraMap (ofBijectiveAlgebraMap h).Ring S) :
        (a : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} (ofBijectiveAlgebraMap h).Ring) →
          Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
      (ofBijectiveAlgebraMap h).jacobiMatrix :
    Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
  (1 : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
Tactic: have : (algebraMap (ofBijectiveAlgebraMap h).Ring S).mapMatrix
      (ofBijectiveAlgebraMap h).jacobiMatrix = 1 := by
    ext (i j : PEmpty)
    contradiction
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this :
  Eq (α := Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
    ((RingHom.mapMatrix (algebraMap (ofBijectiveAlgebraMap h).Ring S) :
          (a : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} (ofBijectiveAlgebraMap h).Ring) →
            Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
        (ofBijectiveAlgebraMap h).jacobiMatrix :
      Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
    (1 : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
⊢ (ofBijectiveAlgebraMap h).jacobian = 1
have rw : Eq.{v + 1} (α := S)
  ((algebraMap (ofBijectiveAlgebraMap h).Ring S : (a : (ofBijectiveAlgebraMap h).Ring) → S)
      (ofBijectiveAlgebraMap h).jacobiMatrix.det :
    S)
  (1 : S)
Tactic: rw [jacobian_eq_jacobiMatrix_det, RingHom.map_det, this, Matrix.det_one]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this :
  Eq (α := Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
    ((RingHom.mapMatrix (algebraMap (ofBijectiveAlgebraMap h).Ring S) :
          (a : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} (ofBijectiveAlgebraMap h).Ring) →
            Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
        (ofBijectiveAlgebraMap h).jacobiMatrix :
      Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
    (1 : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
rw :
  Eq.{v + 1} (α := S)
    ((algebraMap (ofBijectiveAlgebraMap h).Ring S : (a : (ofBijectiveAlgebraMap h).Ring) → S)
        (ofBijectiveAlgebraMap h).jacobiMatrix.det :
      S)
    (1 : S)
⊢ (ofBijectiveAlgebraMap h).jacobian = 1
have rw₁ : Eq.{v + 1} (α := S)
  (Matrix.det.{v, u_1} (n := PEmpty.{u_1 + 1})
    ((RingHom.mapMatrix (algebraMap (ofBijectiveAlgebraMap h).Ring S) :
        (a : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} (ofBijectiveAlgebraMap h).Ring) →
          Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
      (ofBijectiveAlgebraMap h).jacobiMatrix))
  1
Tactic: rw [jacobian_eq_jacobiMatrix_det, RingHom.map_det, this, Matrix.det_one]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this :
  Eq (α := Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
    ((RingHom.mapMatrix (algebraMap (ofBijectiveAlgebraMap h).Ring S) :
          (a : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} (ofBijectiveAlgebraMap h).Ring) →
            Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
        (ofBijectiveAlgebraMap h).jacobiMatrix :
      Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
    (1 : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
rw :
  Eq.{v + 1} (α := S)
    ((algebraMap (ofBijectiveAlgebraMap h).Ring S : (a : (ofBijectiveAlgebraMap h).Ring) → S)
        (ofBijectiveAlgebraMap h).jacobiMatrix.det :
      S)
    (1 : S)
rw₁ :
  Eq.{v + 1} (α := S)
    (Matrix.det.{v, u_1} (n := PEmpty.{u_1 + 1})
      ((RingHom.mapMatrix (algebraMap (ofBijectiveAlgebraMap h).Ring S) :
          (a : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} (ofBijectiveAlgebraMap h).Ring) →
            Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
        (ofBijectiveAlgebraMap h).jacobiMatrix))
    1
⊢ (ofBijectiveAlgebraMap h).jacobian = 1
have rw₂ : Eq.{v + 1} (α := S) (Matrix.det.{v, u_1} (n := PEmpty.{u_1 + 1}) 1) 1
Tactic: rw [jacobian_eq_jacobiMatrix_det, RingHom.map_det, this, Matrix.det_one]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this :
  Eq (α := Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
    ((RingHom.mapMatrix (algebraMap (ofBijectiveAlgebraMap h).Ring S) :
          (a : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} (ofBijectiveAlgebraMap h).Ring) →
            Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
        (ofBijectiveAlgebraMap h).jacobiMatrix :
      Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
    (1 : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
rw :
  Eq.{v + 1} (α := S)
    ((algebraMap (ofBijectiveAlgebraMap h).Ring S : (a : (ofBijectiveAlgebraMap h).Ring) → S)
        (ofBijectiveAlgebraMap h).jacobiMatrix.det :
      S)
    (1 : S)
rw₁ :
  Eq.{v + 1} (α := S)
    (Matrix.det.{v, u_1} (n := PEmpty.{u_1 + 1})
      ((RingHom.mapMatrix (algebraMap (ofBijectiveAlgebraMap h).Ring S) :
          (a : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} (ofBijectiveAlgebraMap h).Ring) →
            Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
        (ofBijectiveAlgebraMap h).jacobiMatrix))
    1
rw₂ : Eq.{v + 1} (α := S) (Matrix.det.{v, u_1} (n := PEmpty.{u_1 + 1}) 1) 1
⊢ (ofBijectiveAlgebraMap h).jacobian = 1
have rw₃ : Eq.{v + 1} (α := S) 1 1
Tactic: rw [jacobian_eq_jacobiMatrix_det, RingHom.map_det, this, Matrix.det_one]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ (ofBijectiveAlgebraMap h).jacobian = 1
have have : Eq (α := Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
  ((RingHom.mapMatrix (algebraMap (ofBijectiveAlgebraMap h).Ring S) :
        (a : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} (ofBijectiveAlgebraMap h).Ring) →
          Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
      (ofBijectiveAlgebraMap h).jacobiMatrix :
    Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
  (1 : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
Tactic: classical
  have : (algebraMap (ofBijectiveAlgebraMap h).Ring S).mapMatrix
      (ofBijectiveAlgebraMap h).jacobiMatrix = 1 := by
    ext (i j : PEmpty)
    contradiction
  rw [jacobian_eq_jacobiMatrix_det, RingHom.map_det, this, Matrix.det_one]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
have :
  Eq (α := Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
    ((RingHom.mapMatrix (algebraMap (ofBijectiveAlgebraMap h).Ring S) :
          (a : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} (ofBijectiveAlgebraMap h).Ring) →
            Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
        (ofBijectiveAlgebraMap h).jacobiMatrix :
      Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
    (1 : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
⊢ (ofBijectiveAlgebraMap h).jacobian = 1
have have₁ : ∀
  (this :
    Eq (α := Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
      ((RingHom.mapMatrix (algebraMap (ofBijectiveAlgebraMap h).Ring S) :
            (a : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} (ofBijectiveAlgebraMap h).Ring) →
              Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
          (ofBijectiveAlgebraMap h).jacobiMatrix :
        Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)
      (1 : Matrix PEmpty.{u_1 + 1} PEmpty.{u_1 + 1} S)),
  (ofBijectiveAlgebraMap h).jacobian = 1
Tactic: classical
  have : (algebraMap (ofBijectiveAlgebraMap h).Ring S).mapMatrix
      (ofBijectiveAlgebraMap h).jacobiMatrix = 1 := by
    ext (i j : PEmpty)
    contradiction
  rw [jacobian_eq_jacobiMatrix_det, RingHom.map_det, this, Matrix.det_one]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ Eq (α := Matrix Unit Unit (Generators.Ring (Presentation.toGenerators (toPresentation (localizationAway S r)))))
    (jacobiMatrix (localizationAway S r)) (Matrix.diagonal fun (x : Unit) ↦ (C : (a : R) → MvPolynomial Unit R) r)
have h : Eq (α := MvPolynomial Unit R)
  ((pderiv () : (a : MvPolynomial Unit R) → MvPolynomial Unit R)
      (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
          ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
        1) :
    MvPolynomial Unit R)
  ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R)
Tactic: have h : (pderiv ()) (C r * X () - 1) = C r := by simp
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
h :
  Eq (α := MvPolynomial Unit R)
    ((pderiv () : (a : MvPolynomial Unit R) → MvPolynomial Unit R)
        (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1) :
      MvPolynomial Unit R)
    ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R)
⊢ Eq (α := Matrix Unit Unit (Generators.Ring (Presentation.toGenerators (toPresentation (localizationAway S r)))))
    (jacobiMatrix (localizationAway S r)) (Matrix.diagonal fun (x : Unit) ↦ (C : (a : R) → MvPolynomial Unit R) r)
have a : ∀ (i j : Unit),
  Eq (α := Generators.Ring (Presentation.toGenerators (toPresentation (localizationAway S r))))
    (jacobiMatrix (localizationAway S r) i j)
    (Matrix.diagonal (fun (x : Unit) ↦ (C : (a : R) → MvPolynomial Unit R) r) i j)
Tactic: ext (i : Unit) (j : Unit) : 1
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
h :
  Eq (α := MvPolynomial Unit R)
    ((pderiv () : (a : MvPolynomial Unit R) → MvPolynomial Unit R)
        (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1) :
      MvPolynomial Unit R)
    ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R)
i j : Unit
⊢ Eq (α := Generators.Ring (Presentation.toGenerators (toPresentation (localizationAway S r))))
    (jacobiMatrix (localizationAway S r) i j)
    (Matrix.diagonal (fun (x : Unit) ↦ (C : (a : R) → MvPolynomial Unit R) r) i j)
have a : Eq (α := Generators.Ring (Presentation.toGenerators (toPresentation (localizationAway S r))))
  ((pderiv (map (localizationAway S r) i) : (a : MvPolynomial Unit R) → MvPolynomial Unit R)
      (Presentation.relation (toPresentation (localizationAway S r)) j) :
    MvPolynomial Unit R)
  (Matrix.diagonal (fun (x : Unit) ↦ (C : (a : R) → MvPolynomial Unit R) r) i j :
    Generators.Ring (Presentation.toGenerators (toPresentation (localizationAway S r))))
Tactic: rwa [jacobiMatrix_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ jacobian (localizationAway S r) = (algebraMap R S : (a : R) → S) r
have rw : Eq.{v + 1} (α := S)
  ((algebraMap (Generators.Ring (Presentation.toGenerators (toPresentation (localizationAway S r)))) S :
        (a : (localizationAway S r).Ring) → S)
      (Matrix.det (n := Unit) (Matrix.diagonal fun (x : Unit) ↦ (C : (a : R) → MvPolynomial Unit R) r)) :
    S)
  ((algebraMap R S : (a : R) → S) r : S)
Tactic: rw [jacobian_eq_jacobiMatrix_det, localizationAway_jacobiMatrix]
-- 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
ι' : 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 σ'
⊢ Nat.card (ι' ⊕ ι) - Nat.card (σ' ⊕ σ) = Nat.card ι' - Nat.card σ' + (Nat.card ι - Nat.card σ)
have this : Nat.card σ ≤ Nat.card ι
Tactic: have : Nat.card σ ≤ Nat.card ι :=
    card_relations_le_card_vars_of_isFinite P
-- 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
ι' : 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 (σ' ⊕ σ) = Nat.card ι' - Nat.card σ' + (Nat.card ι - Nat.card σ)
have this₁ : Nat.card σ' ≤ Nat.card ι'
Tactic: have : Nat.card σ' ≤ Nat.card ι' :=
    card_relations_le_card_vars_of_isFinite Q
-- 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 ι'
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 σ)
have simp : Nat.card ι' + Nat.card ι - (Nat.card σ' + Nat.card σ) = Nat.card ι' - Nat.card σ' + (Nat.card ι - Nat.card σ)
Tactic: simp only [Nat.card_sum]
-- 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: rw [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 σ'
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))))
have refine : ∀ (hmem : map (Q.comp P) (Sum.inl i) ∈ vars (Presentation.relation (toPresentation (Q.comp P)) (Sum.inr j))), False
Tactic: refine MvPolynomial.pderiv_eq_zero_of_notMem_vars (fun hmem ↦ ?_)
-- 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
ι' : 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))
⊢ False
have hmem₁ : 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
Cleared hypotheses: hmem