awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
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 (α := 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)))
have 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 ())))
        sorry) :
    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]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
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 (α := 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)))
have 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
Tactic: congr 2
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (hypothesis)
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
⊢ (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
have this : Nontrivial D.T
Tactic: have : Nontrivial D.T := inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
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) 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
have h : (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 sorry x)
              sorry).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 sorry x)
                  sorry).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 sorry x)
                  sorry).σ
              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: rw [pres, presLeft, presRight, Presentation.relation_comp_localizationAway_inl]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
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
⊢ ∃ (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)
have 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) sorry) :
            P'.toExtension.Cotangent)
Tactic: cases subsingleton_or_nontrivial S
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
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)
⊢ ∃ (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)
have 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) sorry) :
            P'.toExtension.Cotangent)
Tactic: cases subsingleton_or_nontrivial S
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (hypothesis)
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 := ⋯ }
⊢ ∃ (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)
have this : Subsingleton P'.toExtension.Cotangent
Tactic: have : Subsingleton P'.toExtension.Cotangent := Module.subsingleton S _
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
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 : 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)
have inr : ∀ (f : (b : P.toExtension.Cotangent) → ↥P.toExtension.ker)
  (hf :
    ∀ (b : P.toExtension.Cotangent),
      (Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) (f b) = b),
  ∃ (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) sorry) :
            P'.toExtension.Cotangent)
Tactic: choose f hf using Extension.Cotangent.mk_surjective (P := P.toExtension)
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
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 : Nontrivial S
f : (b : P.toExtension.Cotangent) → ↥P.toExtension.ker
hf :
  ∀ (b : P.toExtension.Cotangent),
    (Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) (f b) = b
v : (i : σ) → ↥P.ker := fun (i : σ) ↦ f ((b₀ : (a : σ) → P.toExtension.Cotangent) i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.ker) ∘ v))
⊢ P.ker.FG
have rw : Ideal.FG (RingHom.ker (F := MvPolynomial α R →ₐ[R] S) (aeval P.val))
Tactic: rw [P.ker_eq_ker_aeval_val]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
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 : Nontrivial S
f : (b : P.toExtension.Cotangent) → ↥P.toExtension.ker
hf :
  ∀ (b : P.toExtension.Cotangent),
    (Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) (f b) = b
v : (i : σ) → ↥P.ker := fun (i : σ) ↦ f ((b₀ : (a : σ) → P.toExtension.Cotangent) i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.ker) ∘ v))
⊢ Ideal.FG (RingHom.ker (F := MvPolynomial α R →ₐ[R] S) (aeval P.val))
have hf₁ : Function.Surjective (α := P.Ring) (β := S) (⇑(aeval P.val) : (a : P.Ring) → S)
Tactic: apply FinitePresentation.ker_fG_of_surjective
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
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 : Nontrivial S
f : (b : P.toExtension.Cotangent) → ↥P.toExtension.ker
hf :
  ∀ (b : P.toExtension.Cotangent),
    (Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) (f b) = b
v : (i : σ) → ↥P.ker := fun (i : σ) ↦ f ((b₀ : (a : σ) → P.toExtension.Cotangent) i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.ker) ∘ v))
⊢ Function.Surjective (α := P.Ring) (β := S) (⇑(aeval P.val) : (a : P.Ring) → S)
have h : Eq (α := P.Ring → S) (⇑(aeval P.val) : (a : P.Ring) → S) (⇑(algebraMap P.Ring S) : (a : P.Ring) → S)
Tactic: convert! P.algebraMap_surjective
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (hypothesis)
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 : Nontrivial S
f : (b : P.toExtension.Cotangent) → ↥P.toExtension.ker
hf :
  ∀ (b : P.toExtension.Cotangent),
    (Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) (f b) = b
v : (i : σ) → ↥P.ker := fun (i : σ) ↦ f ((b₀ : (a : σ) → P.toExtension.Cotangent) i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.ker) ∘ v))
⊢ ∃ (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)
have hJfg : P.ker.FG
Tactic: have hJfg : P.ker.FG := by
    rw [P.ker_eq_ker_aeval_val]
    apply FinitePresentation.ker_fG_of_surjective
    convert! P.algebraMap_surjective
    simp [P.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (hypothesis)
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 : Nontrivial S
f : (b : P.toExtension.Cotangent) → ↥P.toExtension.ker
hf :
  ∀ (b : P.toExtension.Cotangent),
    (Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) (f b) = b
v : (i : σ) → ↥P.ker := fun (i : σ) ↦ f ((b₀ : (a : σ) → P.toExtension.Cotangent) i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.ker) ∘ v))
hJfg : P.ker.FG
⊢ ∃ (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)
have hJ : J ≤ P.ker
Tactic: have hJ : J ≤ P.ker := by simp [J, Ideal.span_le, Set.range_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
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 : Nontrivial S
f : (b : P.toExtension.Cotangent) → ↥P.toExtension.ker
hf :
  ∀ (b : P.toExtension.Cotangent),
    (Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) (f b) = b
v : (i : σ) → ↥P.ker := fun (i : σ) ↦ f ((b₀ : (a : σ) → P.toExtension.Cotangent) i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.ker) ∘ v))
hJfg : P.ker.FG
hJ_1 : J ≤ P.ker
hJ : P.ker ≤ J ⊔ P.ker • P.ker
⊢ ∃ (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)
have obtain : ∀ (g : P.Ring) (hgmem : g - 1 ∈ P.ker) (hg : g • P.ker ≤ J),
  ∃ (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) sorry) :
            P'.toExtension.Cotangent)
Tactic: obtain ⟨g, hgmem, hg⟩ := Submodule.exists_sub_one_mem_and_smul_le_of_fg_of_le_sup hJfg le_rfl hJ
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
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 : Nontrivial S
f : (b : P.toExtension.Cotangent) → ↥P.toExtension.ker
hf :
  ∀ (b : P.toExtension.Cotangent),
    (Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) (f b) = b
v : (i : σ) → ↥P.ker := fun (i : σ) ↦ f ((b₀ : (a : σ) → P.toExtension.Cotangent) i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.ker) ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ ∃ (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)
have inr : P.ker ≤ J ⊔ P.ker • P.ker
Tactic: suffices hJ : P.ker ≤ J ⊔ P.ker • P.ker by
    obtain ⟨g, hgmem, hg⟩ := Submodule.exists_sub_one_mem_and_smul_le_of_fg_of_le_sup hJfg le_rfl hJ
    let D : Aux P b₀ := { f := f, hf := hf, g := g, hgmem := hgmem, hg := hg }
    exact ⟨D.pres, D.basis, D.pres_val_comp_inr, D.basis_apply⟩