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
P : PreSubmersivePresentation R S ι σ
inst_3 : Finite σ
hli :
  LinearIndependent S (M := (i : σ) → S) fun (j i : σ) ↦
    (aeval P.val : (a : MvPolynomial ι R) → S)
      ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R)
hsp :
  Eq (α := Submodule S ((i : σ) → S))
    (Submodule.span S
      (Set.range fun (j i : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R)))
    ⊤
⊢ Eq (α := Submodule S ((i : σ) → S))
    (Submodule.span S
      (Set.range fun (j i : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R)))
    ⊤

Tactic:
hsp
-- 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
P : PreSubmersivePresentation R S ι σ
inst_3 : Finite σ
hli :
  LinearIndependent S (M := (i : σ) → S) fun (j i : σ) ↦
    (aeval P.val : (a : MvPolynomial ι R) → S)
      ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R)
hsp :
  Eq (α := Submodule S ((i : σ) → S))
    (Submodule.span S
      (Set.range fun (j i : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R)))
    ⊤
h :
  ∀ (x x_1 : σ),
    Eq.{v + 1} (α := S)
      (Function.comp (β := σ → S) (⇑P.aevalDifferential : (a : σ → S) → σ → S) (⇑(Pi.basisFun S σ) : (a : σ) → σ → S) x
          x_1 :
        S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map x_1) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation x) : MvPolynomial ι R) :
        S)
⊢ Eq (α := Submodule S (σ → S))
    (Submodule.span S
      (Set.range (ι := σ)
        (Function.comp (β := σ → S) (⇑P.aevalDifferential : (a : σ → S) → σ → S)
          (⇑(Pi.basisFun S σ) : (a : σ) → σ → S))))
    ⊤

Tactic:
convert! hsp
-- 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
P : PreSubmersivePresentation R S ι σ
inst_3 : Finite σ
hli :
  LinearIndependent S (M := (i : σ) → S) fun (j i : σ) ↦
    (aeval P.val : (a : MvPolynomial ι R) → S)
      ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R)
hsp :
  Eq (α := Submodule S ((i : σ) → S))
    (Submodule.span S
      (Set.range fun (j i : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R)))
    ⊤
⊢ Function.Bijective (α := σ → S) (β := σ → S) (⇑P.aevalDifferential : (a : σ → S) → σ → S)

Tactic:
exact LinearMap.bijective_of_linearIndependent_of_span_eq_top (Pi.basisFun _ _).span_eq
    (by convert! hli; simp) (by convert! hsp; simp)

Premises used: LinearMap.bijective_of_linearIndependent_of_span_eq_top
-- 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
P : PreSubmersivePresentation R S ι σ
inst_3 : Finite σ
hli :
  LinearIndependent S (M := (i : σ) → S) fun (j i : σ) ↦
    (aeval P.val : (a : MvPolynomial ι R) → S)
      ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R)
hsp :
  Eq (α := Submodule S ((i : σ) → S))
    (Submodule.span S
      (Set.range fun (j i : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R)))
    ⊤
rw rw₁ rw₂ : Function.Bijective (α := σ → S) (β := σ → S) (⇑P.aevalDifferential : (a : σ → S) → σ → S)
⊢ IsUnit P.jacobian

Tactic:
classical
  rw [isUnit_jacobian_iff_aevalDifferential_bijective]
  exact LinearMap.bijective_of_linearIndependent_of_span_eq_top (Pi.basisFun _ _).span_eq
    (by convert! hli; simp) (by convert! hsp; simp)

Premises used: Algebra.PreSubmersivePresentation.isUnit_jacobian_iff_aevalDifferential_bijective, LinearMap.bijective_of_linearIndependent_of_span_eq_top
-- 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
P : PreSubmersivePresentation R S ι σ
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
inst_5 : Fintype σ
inst_6 : DecidableEq σ
⊢ (P.ofAlgEquiv e).jacobiMatrix = P.jacobiMatrix

Tactic:
rfl

Premises used: Algebra.PreSubmersivePresentation.ofAlgEquiv, Algebra.PreSubmersivePresentation.jacobiMatrix, rfl
-- 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
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

Tactic:
cases nonempty_fintype σ

Premises used: nonempty_fintype
-- 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
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 σ
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)
⊢ (P.ofAlgEquiv e).jacobian = (e : (a : S) → T) P.jacobian

Tactic:
rw [jacobian_eq_jacobiMatrix_det, jacobian_eq_jacobiMatrix_det]

Premises used: 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
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 σ
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)
⊢ 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:
simp only [ofAlgEquiv_toPresentation, Presentation.ofAlgEquiv_toGenerators,
    jacobiMatrix_ofAlgEquiv, Generators.algebraMap_apply, Generators.ofAlgEquiv_val,
    ← AlgHom.coe_coe e, MvPolynomial.comp_aeval_apply]

Premises used: Algebra.PreSubmersivePresentation.jacobiMatrix_ofAlgEquiv, AlgHom.coe_coe, Algebra.Generators.algebraMap_apply, Algebra.PreSubmersivePresentation.ofAlgEquiv_toPresentation, MvPolynomial.comp_aeval_apply, Algebra.Presentation.ofAlgEquiv_toGenerators, Algebra.Generators.ofAlgEquiv_val
-- 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
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)
    ((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 [Function.comp_def]

Premises used: Function.comp_def
-- 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
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)
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)
⊢ (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]

Premises used: Algebra.PreSubmersivePresentation.jacobiMatrix_ofAlgEquiv, AlgHom.coe_coe, Algebra.Generators.algebraMap_apply, nonempty_fintype, Function.comp_def, Algebra.PreSubmersivePresentation.ofAlgEquiv_toPresentation, MvPolynomial.comp_aeval_apply, Algebra.Presentation.ofAlgEquiv_toGenerators, Algebra.Generators.ofAlgEquiv_val, 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
P : PreSubmersivePresentation R S ι σ
h_1 : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
a b : PEmpty.{t + 1}
h : Eq.{w + 1} (α := PEmpty.{w + 1}) a.elim b.elim
⊢ a = b

Tactic:
contradiction
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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)
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)
⊢ 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:
ext (i j : PEmpty)

Premises used: PEmpty
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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)
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:
contradiction
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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)

Tactic:
have : (algebraMap (ofBijectiveAlgebraMap h).Ring S).mapMatrix
      (ofBijectiveAlgebraMap h).jacobiMatrix = 1 := by
    ext (i j : PEmpty)
    contradiction
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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
rw₃ rw₄ : Eq.{v + 1} (α := S) 1 1
⊢ (ofBijectiveAlgebraMap h).jacobian = 1

Tactic:
rw [jacobian_eq_jacobiMatrix_det, RingHom.map_det, this, Matrix.det_one]

Premises used: RingHom.map_det, Matrix.det_one, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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)
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
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)
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
⊢ (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]

Premises used: RingHom.map_det, Matrix.det_one, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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 (α := 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:
simp
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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 (α := 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
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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)
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)
⊢ 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)

Tactic:
ext (i : Unit) (j : Unit) : 1

Premises used: Unit
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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
a a₁ a₂ 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))))
⊢ 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:
rwa [jacobiMatrix_apply]

Premises used: Algebra.PreSubmersivePresentation.jacobiMatrix_apply
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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
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)
⊢ jacobian (localizationAway S r) = (algebraMap R S : (a : R) → S) r

Tactic:
rw [jacobian_eq_jacobiMatrix_det, localizationAway_jacobiMatrix]

Premises used: Algebra.PreSubmersivePresentation.localizationAway_jacobiMatrix, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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.{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:
simp [show Fintype.card (localizationAway r (S := S)).rels = 1 from rfl]
-- 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
P_1 : PreSubmersivePresentation 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 ι σ
⊢ ∀ (a : σ') (b : σ), Sum.inl (Q.map a) ≠ Sum.inr (P.map b)

Tactic:
simp
-- 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 ι σ
⊢ Eq (α := Presentation R T (ι' ⊕ ι) (σ' ⊕ σ)) (toPresentation (Q.comp P)) (Q.comp P.toPresentation)

Tactic:
rfl

Premises used: Algebra.Presentation.comp, rfl
-- 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 ι σ
⊢ Eq (α := Generators R T (ι' ⊕ ι)) (Presentation.toGenerators (toPresentation (Q.comp P))) (Q.comp P.toGenerators)

Tactic:
rfl

Premises used: Algebra.Generators.comp, rfl
-- 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 σ'
⊢ Nat.card σ ≤ Nat.card ι

Tactic:
have : Nat.card σ ≤ Nat.card ι :=
    card_relations_le_card_vars_of_isFinite P