awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst_4 : CommRing R₀
inst_5 : Algebra R₀ R
inst_6 : Algebra R₀ S
inst_7 : IsScalarTower R₀ R S
inst_8 : P.HasCoeffs R₀
inst_9 : FaithfulSMul R₀ R
inst_10 : Fintype σ
a :
  Eq (α := MvPolynomial ι R)
    ((MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι R)
        (∑ i : σ,
          HMul.hMul (α := MvPolynomial ι R₀) (P.jacobianRelationsOfHasCoeffs R₀ i)
            (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation) R₀
              i)) :
      MvPolynomial ι R)
    ((MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι R)
        (HMul.hMul (α := MvPolynomial ι R₀) (P.jacobianOfHasCoeffs R₀) (P.invJacobianOfHasCoeffs R₀) - 1) :
      MvPolynomial ι R)
⊢ ∑ i : σ,
      HMul.hMul (α := MvPolynomial ι R₀) (P.jacobianRelationsOfHasCoeffs R₀ i)
        (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation) R₀ i) =
    HMul.hMul (α := MvPolynomial ι R₀) (P.jacobianOfHasCoeffs R₀) (P.invJacobianOfHasCoeffs R₀) - 1

Tactic:
classical
  apply MvPolynomial.map_injective _ (FaithfulSMul.algebraMap_injective R₀ R)
  simp [P.map_relationOfHasCoeffs, jacobianRelations_spec]

Premises used: Algebra.Presentation.map_relationOfHasCoeffs, Algebra.SubmersivePresentation.jacobianRelations_spec, MvPolynomial.map_injective, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Presentation R S ι σ
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst_4 : CommRing R₀
inst_5 : Algebra R₀ R
inst_6 : Algebra R₀ S
inst_7 : IsScalarTower R₀ R S
inst_8 : P.HasCoeffs R₀
inst_9 : FaithfulSMul R₀ R
this : Fintype σ := Fintype.ofFinite σ
⊢ Eq (α :=
    HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
      (Ideal.span
        (Set.range (ι := σ)
          (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation) R₀))))
    ((Ideal.Quotient.mk
            (Ideal.span
              (Set.range (ι := σ)
                (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                  R₀))) :
          (a : MvPolynomial ι R₀) → MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))
        (∑ i : σ,
          HMul.hMul (α := MvPolynomial ι R₀) (P.jacobianRelationsOfHasCoeffs R₀ i)
            (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation) R₀
              i)) :
      HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
        (Ideal.span
          (Set.range (ι := σ)
            (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation) R₀))))
    ((Ideal.Quotient.mk
            (Ideal.span
              (Set.range (ι := σ)
                (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                  R₀))) :
          (a : MvPolynomial ι R₀) → MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))
        (HMul.hMul (α := MvPolynomial ι R₀) (P.jacobianOfHasCoeffs R₀) (P.invJacobianOfHasCoeffs R₀) - 1) :
      HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
        (Ideal.span
          (Set.range (ι := σ)
            (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation) R₀))))

Tactic:
have := congr((Ideal.Quotient.mk _ : _ →+* P.ModelOfHasCoeffs R₀)
      $(P.sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs R₀))
-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Presentation R S ι σ
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst_4 : CommRing R₀
inst_5 : Algebra R₀ R
inst_6 : Algebra R₀ S
inst_7 : IsScalarTower R₀ R S
inst_8 : P.HasCoeffs R₀
inst_9 : FaithfulSMul R₀ R
this_1 : Fintype σ := Fintype.ofFinite σ
this :
  HMul.hMul (α :=
      HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
        (Ideal.span
          (Set.range (ι := σ)
            (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation) R₀))))
      (β :=
      HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
        (Ideal.span
          (Set.range (ι := σ)
            (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation) R₀))))
      ((Ideal.Quotient.mk
              (Ideal.span
                (Set.range (ι := σ)
                  (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                    R₀))) :
            (a : MvPolynomial ι R₀) → MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))
          (P.jacobianOfHasCoeffs R₀) :
        HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
          (Ideal.span
            (Set.range (ι := σ)
              (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                R₀))))
      ((Ideal.Quotient.mk
              (Ideal.span
                (Set.range (ι := σ)
                  (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                    R₀))) :
            (a : MvPolynomial ι R₀) → MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))
          (P.invJacobianOfHasCoeffs R₀) :
        HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
          (Ideal.span
            (Set.range (ι := σ)
              (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                R₀)))) =
    1
⊢ IsUnit (M :=
    Presentation.ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P.toPresentation)
      R₀)
    ((Ideal.Quotient.mk
            (Ideal.span
              (Set.range (ι := σ)
                (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                  R₀))) :
          (a : MvPolynomial ι R₀) → MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))
        (P.jacobianOfHasCoeffs R₀) :
      HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
        (Ideal.span
          (Set.range (ι := σ)
            (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation) R₀))))

Tactic:
IsUnit.of_mul_eq_one _ this

Premises used: IsUnit.of_mul_eq_one
-- 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 ι
⊢ Nat.card σ ≤ Nat.card ι

Tactic:
Nat.card_le_card_of_injective P.map P.map_inj

Premises used: Nat.card_le_card_of_injective, Algebra.PreSubmersivePresentation.map_inj, Algebra.PreSubmersivePresentation.map
-- 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 σ
inst_4 : DecidableEq σ
i j : σ
dsimp :
  Eq.{v + 1} (α := S)
    (((Basis.constr (Pi.basisFun S σ) S : (a : σ → σ → S) → (σ → S) →ₗ[S] σ → 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) :
          (a : σ → S) → σ → S)
        (Pi.single (M := fun (a : σ) ↦ S) i 1) j :
      S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R) :
      S)
⊢ Eq.{v + 1} (α := S) ((P.aevalDifferential : (a : σ → S) → σ → S) (Pi.single (M := fun (a : σ) ↦ S) i 1) j : S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R) :
      S)

Tactic:
dsimp only [aevalDifferential]

Premises used: Algebra.PreSubmersivePresentation.aevalDifferential
-- 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 σ
inst_4 : DecidableEq σ
i j : σ
rw :
  Eq.{v + 1} (α := S)
    (((Basis.constr (Pi.basisFun S σ) S : (a : σ → σ → S) → (σ → S) →ₗ[S] σ → 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) :
          (a : σ → S) → σ → S)
        ((Pi.basisFun S σ : (a : σ) → σ → S) i : σ → S) j :
      S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R) :
      S)
rw₁ rw₂ :
  Eq.{v + 1} (α := S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R) :
      S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R) :
      S)
⊢ Eq.{v + 1} (α := S)
    (((Basis.constr (Pi.basisFun S σ) S : (a : σ → σ → S) → (σ → S) →ₗ[S] σ → 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) :
          (a : σ → S) → σ → S)
        (Pi.single (M := fun (a : σ) ↦ S) i 1) j :
      S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R) :
      S)

Tactic:
rw [← Pi.basisFun_apply, Basis.constr_basis]

Premises used: Pi.basisFun_apply, Module.Basis.constr_basis
-- 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 : Fintype σ
inst_4 : DecidableEq σ
⊢ P.jacobian = (algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det

Tactic:
simp [jacobiMatrix, jacobian]

Premises used: Algebra.PreSubmersivePresentation.jacobian, Algebra.PreSubmersivePresentation.jacobiMatrix
-- 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 : Fintype σ
inst_4 : DecidableEq σ
i j : σ
⊢ P.jacobiMatrix i j = (pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j)

Tactic:
simp [jacobiMatrix, LinearMap.toMatrix, differential, basis]

Premises used: Algebra.PreSubmersivePresentation.basis, Algebra.PreSubmersivePresentation.jacobiMatrix, Algebra.PreSubmersivePresentation.differential, LinearMap.toMatrix
-- 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 : Fintype σ
inst_4 : DecidableEq σ
a :
  ∀ (i j : σ),
    Eq.{v + 1} (α := S) ((LinearMap.toMatrix' : (a : (σ → S) →ₗ[S] σ → S) → Matrix σ σ S) P.aevalDifferential i j : S)
      ((AlgHom.mapMatrix (aeval P.val) : (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ S) P.jacobiMatrix i j : S)
⊢ Eq (α := Matrix σ σ S)
    ((LinearMap.toMatrix' : (a : (σ → S) →ₗ[S] σ → S) → Matrix σ σ S) P.aevalDifferential : Matrix σ σ S)
    ((AlgHom.mapMatrix (aeval P.val) : (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ S) P.jacobiMatrix :
      Matrix σ σ S)

Tactic:
ext i j : 1
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst_3 : Fintype σ
inst_4 : DecidableEq σ
i j : σ
a :
  Eq.{v + 1} (α := S)
    ((LinearMap.toMatrix (Pi.basisFun S σ) (Pi.basisFun S σ) : (a : (σ → S) →ₗ[S] σ → S) → Matrix σ σ S)
        P.aevalDifferential i j :
      S)
    ((AlgHom.mapMatrix (aeval P.val) : (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ S) P.jacobiMatrix i j : S)
⊢ Eq.{v + 1} (α := S) ((LinearMap.toMatrix' : (a : (σ → S) →ₗ[S] σ → S) → Matrix σ σ S) P.aevalDifferential i j : S)
    ((AlgHom.mapMatrix (aeval P.val) : (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ S) P.jacobiMatrix i j : S)

Tactic:
rw [← LinearMap.toMatrix_eq_toMatrix']

Premises used: LinearMap.toMatrix_eq_toMatrix'
-- 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 : Fintype σ
inst_4 : DecidableEq σ
i j : σ
a :
  Eq.{v + 1} (α := S)
    ((((Basis.repr (Pi.basisFun S σ) : (a : σ → S) → σ →₀ S)
              ((P.aevalDifferential : (a : σ → S) → σ → S) ((Pi.basisFun S σ : (a : σ) → σ → S) j : σ → S)) :
            σ →₀ S) :
          (a : σ) → S)
        i :
      S)
    ((AlgHom.mapMatrix (aeval P.val) : (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ S) P.jacobiMatrix i j : S)
⊢ Eq.{v + 1} (α := S)
    ((LinearMap.toMatrix (Pi.basisFun S σ) (Pi.basisFun S σ) : (a : (σ → S) →ₗ[S] σ → S) → Matrix σ σ S)
        P.aevalDifferential i j :
      S)
    ((AlgHom.mapMatrix (aeval P.val) : (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ S) P.jacobiMatrix i j : S)

Tactic:
rw [LinearMap.toMatrix_apply]

Premises used: LinearMap.toMatrix_apply
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst_3 : Fintype σ
inst_4 : DecidableEq σ
i j : σ
⊢ Eq.{v + 1} (α := S)
    ((((Basis.repr (Pi.basisFun S σ) : (a : σ → S) → σ →₀ S)
              ((P.aevalDifferential : (a : σ → S) → σ → S) ((Pi.basisFun S σ : (a : σ) → σ → S) j : σ → S)) :
            σ →₀ S) :
          (a : σ) → S)
        i :
      S)
    ((AlgHom.mapMatrix (aeval P.val) : (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ S) P.jacobiMatrix i j : S)

Tactic:
simp [jacobiMatrix_apply]

Premises used: Algebra.PreSubmersivePresentation.jacobiMatrix_apply
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst_3 : Finite σ
intro :
  ∀ (val : Fintype σ),
    P.jacobian =
      ((LinearMap.det (M := σ → S) (A := S) : ((σ → S) →ₗ[S] σ → S) →* S) : (a : (σ → S) →ₗ[S] σ → S) → S)
        P.aevalDifferential
⊢ P.jacobian =
    ((LinearMap.det (M := σ → S) (A := S) : ((σ → S) →ₗ[S] σ → S) →* S) : (a : (σ → S) →ₗ[S] σ → S) → S)
      P.aevalDifferential

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 ι σ
inst_3 : Finite σ
val : Fintype σ
⊢ P.jacobian =
    ((LinearMap.det (M := σ → S) (A := S) : ((σ → S) →ₗ[S] σ → S) →* S) : (a : (σ → S) →ₗ[S] σ → S) → S)
      P.aevalDifferential

Tactic:
simp [← LinearMap.det_toMatrix', P.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix,
    jacobian_eq_jacobiMatrix_det, RingHom.map_det, P.algebraMap_eq]

Premises used: Algebra.Generators.algebraMap_eq, Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, Algebra.PreSubmersivePresentation.toPresentation, RingHom.map_det, LinearMap.det_toMatrix', Algebra.Presentation.toGenerators, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst_3 : Finite σ
intro :
  ∀ (val : Fintype σ),
    P.jacobian =
      ((LinearMap.det (M := σ → S) (A := S) : ((σ → S) →ₗ[S] σ → S) →* S) : (a : (σ → S) →ₗ[S] σ → S) → S)
        P.aevalDifferential
⊢ P.jacobian =
    ((LinearMap.det (M := σ → S) (A := S) : ((σ → S) →ₗ[S] σ → S) →* S) : (a : (σ → S) →ₗ[S] σ → S) → S)
      P.aevalDifferential

Tactic:
classical
  cases nonempty_fintype σ
  simp [← LinearMap.det_toMatrix', P.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix,
    jacobian_eq_jacobiMatrix_det, RingHom.map_det, P.algebraMap_eq]

Premises used: Algebra.Generators.algebraMap_eq, Algebra.PreSubmersivePresentation.toPresentation, nonempty_fintype, RingHom.map_det, LinearMap.det_toMatrix', Algebra.Presentation.toGenerators, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst_3 : Finite σ
rw :
  IsUnit P.aevalDifferential ↔ Function.Bijective (α := σ → S) (β := σ → S) (⇑P.aevalDifferential : (a : σ → S) → σ → S)
⊢ IsUnit P.jacobian ↔ Function.Bijective (α := σ → S) (β := σ → S) (⇑P.aevalDifferential : (a : σ → S) → σ → S)

Tactic:
rw [P.jacobian_eq_det_aevalDifferential, ← LinearMap.isUnit_iff_isUnit_det]

Premises used: LinearMap.isUnit_iff_isUnit_det, Algebra.PreSubmersivePresentation.jacobian_eq_det_aevalDifferential
-- 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 σ
⊢ IsUnit P.aevalDifferential ↔ Function.Bijective (α := σ → S) (β := σ → S) (⇑P.aevalDifferential : (a : σ → S) → σ → S)

Tactic:
Module.End.isUnit_iff P.aevalDifferential

Premises used: Module.End.isUnit_iff, Algebra.PreSubmersivePresentation.aevalDifferential
-- 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 σ
⊢ IsUnit P.aevalDifferential ↔ Function.Bijective (α := σ → S) (β := σ → S) (⇑P.aevalDifferential : (a : σ → S) → σ → S)

Tactic:
exact Module.End.isUnit_iff P.aevalDifferential

Premises used: Module.End.isUnit_iff, Algebra.PreSubmersivePresentation.aevalDifferential
-- 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 : Function.Bijective (α := σ → S) (β := σ → S) (⇑P.aevalDifferential : (a : σ → S) → σ → S)
⊢ IsUnit P.jacobian

Tactic:
rw [isUnit_jacobian_iff_aevalDifferential_bijective]

Premises used: Algebra.PreSubmersivePresentation.isUnit_jacobian_iff_aevalDifferential_bijective
-- 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)))
    ⊤
⊢ 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)

Tactic:
hli
-- 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)
⊢ LinearIndependent (ι := σ) S (M := σ → S)
    (Function.comp (β := σ → S) (⇑P.aevalDifferential : (a : σ → S) → σ → S) (⇑(Pi.basisFun S σ) : (a : σ) → σ → S))

Tactic:
convert! hli
-- 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)))
    ⊤
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)

Tactic:
simp