awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
i : σ
⊢ Eq (α := S ⊗[D.T] D.presLeft.toExtension.Cotangent)
    ((((AlgebraTensorModule.curry (D.tensorCotangentInv ∘ₗ D.tensorCotangentHom) :
                S →ₗ[S]
                  LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent
                    (S ⊗[D.T] D.presLeft.toExtension.Cotangent)) :
              (a : S) → D.presLeft.toExtension.Cotangent →ₗ[D.T] S ⊗[D.T] D.presLeft.toExtension.Cotangent)
            1 :
          (a : D.presLeft.toExtension.Cotangent) → S ⊗[D.T] D.presLeft.toExtension.Cotangent)
        ((Extension.Cotangent.mk : (a : ↥D.presLeft.toExtension.ker) → D.presLeft.toExtension.Cotangent) (D.kerGen i)) :
      S ⊗[D.T] D.presLeft.toExtension.Cotangent)
    ((((AlgebraTensorModule.curry LinearMap.id :
                S →ₗ[S]
                  LinearMap (R := D.T) (RingHom.id D.T) D.presLeft.toExtension.Cotangent
                    (S ⊗[D.T] D.presLeft.toExtension.Cotangent)) :
              (a : S) → D.presLeft.toExtension.Cotangent →ₗ[D.T] S ⊗[D.T] D.presLeft.toExtension.Cotangent)
            1 :
          (a : D.presLeft.toExtension.Cotangent) → S ⊗[D.T] D.presLeft.toExtension.Cotangent)
        ((Extension.Cotangent.mk : (a : ↥D.presLeft.toExtension.ker) → D.presLeft.toExtension.Cotangent) (D.kerGen i)) :
      S ⊗[D.T] D.presLeft.toExtension.Cotangent)

Tactic:
simp [-toExtension_commRing, -toExtension_Ring, -toExtension_algebra₂, tensorCotangentHom_tmul,
      kerGen, D.hf]

Premises used: Algebra.Generators.toExtension_algebra₂, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.hf, Algebra.Generators.toExtension_Ring, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.tensorCotangentHom_tmul, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.kerGen, Algebra.Generators.toExtension_commRing
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
i : σ
⊢ Eq (α := S ⊗[D.T] D.presLeft.toExtension.Cotangent)
    ((D.tensorCotangentEquiv.symm : (a : P.toExtension.Cotangent) → S ⊗[D.T] D.presLeft.toExtension.Cotangent)
        ((b : (a : σ) → P.toExtension.Cotangent) i) :
      S ⊗[D.T] D.presLeft.toExtension.Cotangent)
    (1 ⊗ₜ[D.T]
        (Extension.Cotangent.mk : (a : ↥D.presLeft.toExtension.ker) → D.presLeft.toExtension.Cotangent) (D.kerGen i) :
      S ⊗[D.T] D.presLeft.toExtension.Cotangent)

Tactic:
D.tensorCotangentInv_apply i

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.tensorCotangentInv_apply, Finset.sum
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst_3 : Nontrivial S
simp_rw :
  Eq (α := Extension.Cotangent (toExtension (localizationAway S D.gbar)))
    ((Extension.Cotangent.mk :
          (a : ↥(localizationAway S D.gbar).toExtension.ker) → (localizationAway S D.gbar).toExtension.Cotangent)
        (Subtype.mk (p := fun (x : Extension.Ring (toExtension (localizationAway S D.gbar))) ↦
          Membership.mem (γ := Ideal (Extension.Ring (toExtension (localizationAway S D.gbar))))
            (Extension.ker (toExtension (localizationAway S D.gbar))) x)
          ((Hom.toAlgHom (ofComp (localizationAway S D.gbar) D.presLeft.toGenerators) :
              (a : ((localizationAway S D.gbar).comp D.presLeft.toGenerators).Ring) → (localizationAway S D.gbar).Ring)
            (D.pres.relation (Sum.inl ())))
          ⋯) :
      Extension.Cotangent (toExtension (localizationAway S D.gbar)))
    (cMulXSubOneCotangent S D.gbar : Extension.Cotangent (toExtension (localizationAway S D.gbar)))
⊢ Eq (α := Extension.Cotangent (toExtension (localizationAway S D.gbar)))
    ((Extension.Cotangent.map (Hom.toExtensionHom (ofComp (localizationAway S D.gbar) D.presLeft.toGenerators)) :
          (a : ((localizationAway S D.gbar).comp D.presLeft.toGenerators).toExtension.Cotangent) →
            (localizationAway S D.gbar).toExtension.Cotangent)
        ((Extension.Cotangent.mk :
            (a : ↥((localizationAway S D.gbar).comp D.presLeft.toGenerators).toExtension.ker) →
              ((localizationAway S D.gbar).comp D.presLeft.toGenerators).toExtension.Cotangent)
          (Subtype.mk (p :=
            fun (x : Extension.Ring (toExtension (comp (localizationAway S D.gbar) D.presLeft.toGenerators))) ↦
            Membership.mem (γ :=
              Ideal (Extension.Ring (toExtension (comp (localizationAway S D.gbar) D.presLeft.toGenerators))))
              (Extension.ker (toExtension (comp (localizationAway S D.gbar) D.presLeft.toGenerators))) x)
            (D.pres.relation (Sum.inl ())) ⋯)) :
      Extension.Cotangent (toExtension (localizationAway S D.gbar)))
    (cMulXSubOneCotangent S D.gbar : Extension.Cotangent (toExtension (localizationAway S D.gbar)))

Tactic:
simp_rw [Extension.Cotangent.map_mk, Generators.Hom.toExtensionHom_toAlgHom_apply]

Premises used: Algebra.Generators.Hom.toExtensionHom_toAlgHom_apply, Algebra.Extension.Cotangent.map_mk
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst_3 : Nontrivial S
h :
  (Hom.toAlgHom (ofComp (localizationAway S D.gbar) D.presLeft.toGenerators) :
        (a : ((localizationAway S D.gbar).comp D.presLeft.toGenerators).Ring) → (localizationAway S D.gbar).Ring)
      (D.pres.relation (Sum.inl ())) =
    HMul.hMul (α := MvPolynomial Unit D.T) (β := MvPolynomial Unit D.T)
        ((C : (a : D.T) → MvPolynomial Unit D.T) D.gbar : MvPolynomial Unit D.T) (X ()) -
      1
⊢ Eq (α := Extension.Cotangent (toExtension (localizationAway S D.gbar)))
    ((Extension.Cotangent.mk :
          (a : ↥(localizationAway S D.gbar).toExtension.ker) → (localizationAway S D.gbar).toExtension.Cotangent)
        (Subtype.mk (p := fun (x : Extension.Ring (toExtension (localizationAway S D.gbar))) ↦
          Membership.mem (γ := Ideal (Extension.Ring (toExtension (localizationAway S D.gbar))))
            (Extension.ker (toExtension (localizationAway S D.gbar))) x)
          ((Hom.toAlgHom (ofComp (localizationAway S D.gbar) D.presLeft.toGenerators) :
              (a : ((localizationAway S D.gbar).comp D.presLeft.toGenerators).Ring) → (localizationAway S D.gbar).Ring)
            (D.pres.relation (Sum.inl ())))
          ⋯) :
      Extension.Cotangent (toExtension (localizationAway S D.gbar)))
    (cMulXSubOneCotangent S D.gbar : Extension.Cotangent (toExtension (localizationAway S D.gbar)))

Tactic:
congr 2
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst_3 : Nontrivial S
⊢ Nontrivial D.T

Tactic:
have : Nontrivial D.T := inferInstance
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst_3 : Nontrivial S
this :
  Nontrivial
    (HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal P.Ring)
      (Ideal.span
        (Set.range (ι := σ)
          (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.toExtension.ker) ∘
            D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
⊢ (Hom.toAlgHom
          (ofComp (localizationAway S D.gbar)
            (Presentation.naive
                (fun
                    (x :
                      HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
                        (Ideal.span
                          (Set.range (ι := σ)
                            (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                              D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))) ↦
                  if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x)
                ⋯).toGenerators) :
        (a :
            ((localizationAway S D.gbar).comp
                (Presentation.naive
                    (fun
                        (x :
                          MvPolynomial ι R ⧸
                            Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) ↦
                      if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x)
                    ⋯).toGenerators).Ring) →
          (localizationAway S D.gbar).Ring)
      (HMul.hMul (α := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R) (β := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
          ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R)
              ((Presentation.naive
                    (fun
                        (x :
                          HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
                            (Ideal.span
                              (Set.range (ι := σ)
                                (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                                  D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))) ↦
                      if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x)
                    ⋯).σ
                D.gbar) :
            MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
          (X (Sum.inl ())) -
        1) =
    HMul.hMul (α := MvPolynomial Unit D.T) (β := MvPolynomial Unit D.T)
        ((C : (a : D.T) → MvPolynomial Unit D.T) D.gbar : MvPolynomial Unit D.T) (X ()) -
      1

Tactic:
Generators.toAlgHom_ofComp_localizationAway _ _

Premises used: Algebra.Generators.toAlgHom_ofComp_localizationAway, AddMonoidAlgebra.singleZeroRingHom, AddMonoidAlgebra, Finsupp.single
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst_3 : Nontrivial S
this :
  Nontrivial
    (HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal P.Ring)
      (Ideal.span
        (Set.range (ι := σ)
          (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.toExtension.ker) ∘
            D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
⊢ (Hom.toAlgHom
          (ofComp (localizationAway S D.gbar)
            (Presentation.naive
                (fun
                    (x :
                      HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
                        (Ideal.span
                          (Set.range (ι := σ)
                            (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                              D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))) ↦
                  if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x)
                ⋯).toGenerators) :
        (a :
            ((localizationAway S D.gbar).comp
                (Presentation.naive
                    (fun
                        (x :
                          MvPolynomial ι R ⧸
                            Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) ↦
                      if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x)
                    ⋯).toGenerators).Ring) →
          (localizationAway S D.gbar).Ring)
      (HMul.hMul (α := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R) (β := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
          ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R)
              ((Presentation.naive
                    (fun
                        (x :
                          HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
                            (Ideal.span
                              (Set.range (ι := σ)
                                (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                                  D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))) ↦
                      if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x)
                    ⋯).σ
                D.gbar) :
            MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
          (X (Sum.inl ())) -
        1) =
    HMul.hMul (α := MvPolynomial Unit D.T) (β := MvPolynomial Unit D.T)
        ((C : (a : D.T) → MvPolynomial Unit D.T) D.gbar : MvPolynomial Unit D.T) (X ()) -
      1

Tactic:
exact Generators.toAlgHom_ofComp_localizationAway _ _

Premises used: Algebra.Generators.toAlgHom_ofComp_localizationAway
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst_3 : Nontrivial S
this :
  Nontrivial
    (HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal P.Ring)
      (Ideal.span
        (Set.range (ι := σ)
          (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.toExtension.ker) ∘
            D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
⊢ (if
        Eq (α :=
          HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
            (Ideal.span
              (Set.range (ι := σ)
                (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                  D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
          (-1) 0 then
      0
    else
      if
          Eq (α :=
            HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
              (Ideal.span
                (Set.range (ι := σ)
                  (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                    D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
            (-1) (-1) then
        -1
      else Function.surjInv ⋯ (-1)) =
    -1

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst_3 : Nontrivial S
this :
  Nontrivial
    (HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal P.Ring)
      (Ideal.span
        (Set.range (ι := σ)
          (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.toExtension.ker) ∘
            D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
⊢ (if
        Eq (α :=
          HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
            (Ideal.span
              (Set.range (ι := σ)
                (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                  D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
          0 0 then
      0
    else
      if
          Eq (α :=
            HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
              (Ideal.span
                (Set.range (ι := σ)
                  (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                    D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
            0 (-1) then
        -1
      else Function.surjInv ⋯ 0) =
    0

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst_3 : Nontrivial S
x : D.presRight.toExtension.Cotangent
y : S ⊗[D.T] D.presLeft.toExtension.Cotangent
⊢ Eq (α := D.pres.toExtension.Cotangent)
    ((D.cotangentEquivProd.symm :
          (a : D.presRight.toExtension.Cotangent × S ⊗[D.T] D.presLeft.toExtension.Cotangent) →
            D.pres.toExtension.Cotangent)
        (x, y) :
      D.pres.toExtension.Cotangent)
    (((cotangentCompLocalizationAwayEquiv D.gbar D.presLeft.toGenerators ⋯).symm :
          (a : S ⊗[D.T] D.presLeft.toExtension.Cotangent × (localizationAway S D.gbar).toExtension.Cotangent) →
            ((localizationAway S D.gbar).comp D.presLeft.toGenerators).toExtension.Cotangent)
        (y, x) :
      Extension.Cotangent (toExtension (comp (localizationAway S D.gbar) D.presLeft.toGenerators)))

Tactic:
rfl

Premises used: Set.Mem, Ideal.Cotangent, Quotient, rfl, Algebra.Extension.Cotangent
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst_3 : Nontrivial S
⊢ Eq (α := D.pres.toExtension.Cotangent)
    ((D.basis : (a : Unit ⊕ σ) → D.pres.toExtension.Cotangent) (Sum.inl ()) : D.pres.toExtension.Cotangent)
    ((D.cotangentEquivProd.symm :
          (a : D.presRight.toExtension.Cotangent × S ⊗[D.T] D.presLeft.toExtension.Cotangent) →
            D.pres.toExtension.Cotangent)
        (cMulXSubOneCotangent S D.gbar, 0) :
      D.pres.toExtension.Cotangent)

Tactic:
simpa [basis] using Generators.basisCotangentAway_apply _ _

Premises used: _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.basis, Algebra.Generators.basisCotangentAway_apply
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst_3 : Nontrivial S
i : σ
⊢ Eq (α := D.pres.toExtension.Cotangent)
    ((D.basis : (a : Unit ⊕ σ) → D.pres.toExtension.Cotangent) (Sum.inr i) : D.pres.toExtension.Cotangent)
    ((D.cotangentEquivProd.symm :
          (a : D.presRight.toExtension.Cotangent × S ⊗[D.T] D.presLeft.toExtension.Cotangent) →
            D.pres.toExtension.Cotangent)
        (0, (D.basisLeft : (a : σ) → S ⊗[D.T] D.presLeft.toExtension.Cotangent) i) :
      D.pres.toExtension.Cotangent)

Tactic:
simp [basis]

Premises used: _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.basis
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ D.pres.val ∘ Sum.inr = P.val

Tactic:
funext (aeval_X _)

Premises used: MvPolynomial.aeval_X, funext
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst_4 : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
inl :
  Subsingleton S →
    ∃ (P' : Presentation.{u_5, u_4, u_1, u_2} R S (Unit ⊕ α) (Unit ⊕ σ)) (b :
      Module.Basis (Unit ⊕ σ) S P'.toExtension.Cotangent),
      P'.val ∘ Sum.inr = P.val ∧
        ∀ (r : Unit ⊕ σ),
          Eq (α := P'.toExtension.Cotangent)
            ((b : (a : Unit ⊕ σ) → P'.toExtension.Cotangent) r : P'.toExtension.Cotangent)
            ((Extension.Cotangent.mk : (a : ↥P'.toExtension.ker) → P'.toExtension.Cotangent)
                (Subtype.mk (p := fun (x : P'.toExtension.Ring) ↦ x ∈ P'.toExtension.ker) (P'.relation r) ⋯) :
              P'.toExtension.Cotangent)
inr :
  Nontrivial S →
    ∃ (P' : Presentation.{u_5, u_4, u_1, u_2} R S (Unit ⊕ α) (Unit ⊕ σ)) (b :
      Module.Basis (Unit ⊕ σ) S P'.toExtension.Cotangent),
      P'.val ∘ Sum.inr = P.val ∧
        ∀ (r : Unit ⊕ σ),
          Eq (α := P'.toExtension.Cotangent)
            ((b : (a : Unit ⊕ σ) → P'.toExtension.Cotangent) r : P'.toExtension.Cotangent)
            ((Extension.Cotangent.mk : (a : ↥P'.toExtension.ker) → P'.toExtension.Cotangent)
                (Subtype.mk (p := fun (x : P'.toExtension.Ring) ↦ x ∈ P'.toExtension.ker) (P'.relation r) ⋯) :
              P'.toExtension.Cotangent)
⊢ ∃ (P' : Presentation.{u_5, u_4, u_1, u_2} R S (Unit ⊕ α) (Unit ⊕ σ)) (b :
    Module.Basis (Unit ⊕ σ) S P'.toExtension.Cotangent),
    P'.val ∘ Sum.inr = P.val ∧
      ∀ (r : Unit ⊕ σ),
        Eq (α := P'.toExtension.Cotangent)
          ((b : (a : Unit ⊕ σ) → P'.toExtension.Cotangent) r : P'.toExtension.Cotangent)
          ((Extension.Cotangent.mk : (a : ↥P'.toExtension.ker) → P'.toExtension.Cotangent)
              (Subtype.mk (p := fun (x : P'.toExtension.Ring) ↦ x ∈ P'.toExtension.ker) (P'.relation r) ⋯) :
            P'.toExtension.Cotangent)

Tactic:
cases subsingleton_or_nontrivial S

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst_4 : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h : Subsingleton S
⊢ Eq (α :=
    Ideal (Generators.Ring.{u_4, u_1, u_2} (R := R) (S := S) (ι := Unit ⊕ α) (ofSurjective (fun (i : Unit ⊕ α) ↦ 0) ⋯)))
    (Ideal.span (Set.range fun (x : Unit ⊕ σ) ↦ 1)) (ker (ofSurjective (fun (i : Unit ⊕ α) ↦ 0) ⋯))

Tactic:
simpa using (RingHom.ker_eq_top_of_subsingleton _).symm

Premises used: RingHom.ker_eq_top_of_subsingleton, Eq.symm
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst_4 : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h : Subsingleton S
P' : Presentation.{u_5, u_4, u_1, u_2} R S (Unit ⊕ α) (Unit ⊕ σ) :=
  let __Generators : Generators.{u_4, u_1, u_2} R S (Unit ⊕ α) := ofSurjective (fun (i : Unit ⊕ α) ↦ 0) ⋯;
  { toGenerators := __Generators, relation := fun (x : Unit ⊕ σ) ↦ 1, span_range_relation_eq_ker := ⋯ }
⊢ Subsingleton P'.toExtension.Cotangent

Tactic:
have : Subsingleton P'.toExtension.Cotangent := Module.subsingleton S _
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst_4 : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h : Subsingleton S
P' : Presentation.{u_5, u_4, u_1, u_2} R S (Unit ⊕ α) (Unit ⊕ σ) :=
  let __Generators : Generators.{u_4, u_1, u_2} R S (Unit ⊕ α) := ofSurjective (fun (i : Unit ⊕ α) ↦ 0) ⋯;
  { toGenerators := __Generators, relation := fun (x : Unit ⊕ σ) ↦ 1, span_range_relation_eq_ker := ⋯ }
this : Subsingleton P'.toExtension.Cotangent
⊢ P'.val ∘ Sum.inr = P.val

Tactic:
subsingleton
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst_4 : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h : Subsingleton S
P' : Presentation.{u_5, u_4, u_1, u_2} R S (Unit ⊕ α) (Unit ⊕ σ) :=
  let __Generators : Generators.{u_4, u_1, u_2} R S (Unit ⊕ α) := ofSurjective (fun (i : Unit ⊕ α) ↦ 0) ⋯;
  { toGenerators := __Generators, relation := fun (x : Unit ⊕ σ) ↦ 1, span_range_relation_eq_ker := ⋯ }
this : Subsingleton P'.toExtension.Cotangent
⊢ ∀ (r : Unit ⊕ σ),
    Eq (α := P'.toExtension.Cotangent)
      ((default : (a : Unit ⊕ σ) → P'.toExtension.Cotangent) r : P'.toExtension.Cotangent)
      ((Extension.Cotangent.mk : (a : ↥P'.toExtension.ker) → P'.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : P'.toExtension.Ring) ↦ x ∈ P'.toExtension.ker) (P'.relation r) ⋯) :
        P'.toExtension.Cotangent)

Tactic:
subsingleton