awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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₀
this : Fintype σ := Fintype.ofFinite σ
rw :
  (MvPolynomial.aeval P.val : (a : MvPolynomial ι R) → S)
      ((MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι R) (P.jacobianOfHasCoeffs R₀) :
        MvPolynomial ι R) =
    P.jacobian
rw₁ : (MvPolynomial.aeval P.val : (a : MvPolynomial ι R) → S) P.jacobiMatrix.det = P.jacobian
rw₂ :
  Eq.{u_2 + 1} (α := S) ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R) → S) P.jacobiMatrix.det : S)
    ((algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : S)
⊢ (MvPolynomial.aeval P.val : (a : MvPolynomial ι R₀) → S) (P.jacobianOfHasCoeffs R₀) = P.jacobian
have rw₃ : Eq.{u_2 + 1} (α := S) ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R) → S) P.jacobiMatrix.det : S)
  ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R) → S) P.jacobiMatrix.det : S)
Tactic: rw [← MvPolynomial.aeval_map_algebraMap R, map_jacobianOfHasCoeffs,
    P.jacobian_eq_jacobiMatrix_det, Generators.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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 σ
⊢ ∑ 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
have 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)
Tactic: apply MvPolynomial.map_injective _ (FaithfulSMul.algebraMap_injective R₀ R)
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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 σ
⊢ ∑ 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
have 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)
Tactic: classical
  apply MvPolynomial.map_injective _ (FaithfulSMul.algebraMap_injective R₀ R)
  simp [P.map_relationOfHasCoeffs, jacobianRelations_spec]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (hypothesis)
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 σ
⊢ IsUnit (M :=
    Presentation.ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P.toPresentation)
      R₀)
    (PreSubmersivePresentation.jacobian (P.ofHasCoeffs R₀))
have this₁ : 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₀))
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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₀)
    (PreSubmersivePresentation.jacobian (P.ofHasCoeffs R₀))
have h : Eq (α :=
  Presentation.ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P.toPresentation)
    R₀)
  (PreSubmersivePresentation.jacobian (P.ofHasCoeffs 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₀))
Tactic: convert! IsUnit.of_mul_eq_one _ this
-- 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 ι σ
inst_3 : Finite σ
inst_4 : DecidableEq σ
i j : σ
⊢ 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)
have 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)
Tactic: dsimp only [aevalDifferential]
-- 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 ι σ
inst_3 : Finite σ
inst_4 : DecidableEq σ
i j : σ
⊢ 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)
have 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)
Tactic: rw [← Pi.basisFun_apply, Basis.constr_basis]
-- 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 ι σ
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)
⊢ 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)
have 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)
Tactic: rw [← Pi.basisFun_apply, Basis.constr_basis]
-- 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 ι σ
inst_3 : Fintype σ
inst_4 : DecidableEq σ
⊢ 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)
have 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)
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 ι σ
inst_3 : Fintype σ
inst_4 : DecidableEq σ
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)
have 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)
Tactic: rw [← LinearMap.toMatrix_eq_toMatrix']
-- 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 ι σ
inst_3 : Fintype σ
inst_4 : DecidableEq σ
i j : σ
⊢ 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)
have 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)
Tactic: rw [LinearMap.toMatrix_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 ι σ
inst_3 : Finite σ
⊢ P.jacobian =
    ((LinearMap.det (M := σ → S) (A := S) : ((σ → S) →ₗ[S] σ → S) →* S) : (a : (σ → S) →ₗ[S] σ → S) → S)
      P.aevalDifferential
have intro : ∀ (val : Fintype σ),
  P.jacobian =
    ((LinearMap.det (M := σ → S) (A := S) : ((σ → S) →ₗ[S] σ → S) →* S) : (a : (σ → S) →ₗ[S] σ → S) → S)
      P.aevalDifferential
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 ι σ
inst_3 : Finite σ
⊢ P.jacobian =
    ((LinearMap.det (M := σ → S) (A := S) : ((σ → S) →ₗ[S] σ → S) →* S) : (a : (σ → S) →ₗ[S] σ → S) → S)
      P.aevalDifferential
have intro : ∀ (val : Fintype σ),
  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]
-- 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 ι σ
inst_3 : Finite σ
⊢ IsUnit P.jacobian ↔ Function.Bijective (α := σ → S) (β := σ → S) (⇑P.aevalDifferential : (a : σ → S) → σ → S)
have rw : IsUnit P.aevalDifferential ↔ Function.Bijective (α := σ → S) (β := σ → S) (⇑P.aevalDifferential : (a : σ → S) → σ → S)
Tactic: rw [P.jacobian_eq_det_aevalDifferential, ← LinearMap.isUnit_iff_isUnit_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 ι σ
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)))
    ⊤
⊢ IsUnit P.jacobian
have rw : Function.Bijective (α := σ → S) (β := σ → S) (⇑P.aevalDifferential : (a : σ → S) → σ → S)
Tactic: rw [isUnit_jacobian_iff_aevalDifferential_bijective]
-- 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 ι σ
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 := σ → S)
    (Function.comp (β := σ → S) (⇑P.aevalDifferential : (a : σ → S) → σ → S) (⇑(Pi.basisFun S σ) : (a : σ) → σ → S))
have 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)
Tactic: convert! hli
-- 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 ι σ
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 (σ → S))
    (Submodule.span S
      (Set.range (ι := σ)
        (Function.comp (β := σ → S) (⇑P.aevalDifferential : (a : σ → S) → σ → S)
          (⇑(Pi.basisFun S σ) : (a : σ) → σ → S))))
    ⊤
have 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)
Tactic: convert! hsp
-- 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 ι σ
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)))
    ⊤
⊢ IsUnit P.jacobian
have rw : Function.Bijective (α := σ → S) (β := σ → S) (⇑P.aevalDifferential : (a : σ → S) → σ → S)
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)
-- 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: cases nonempty_fintype σ