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
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' : 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:
exact ⟨P', default, by subsingleton, by 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 : Nontrivial S
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) ⋯) :
              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:
choose f hf using Extension.Cotangent.mk_surjective (P := P.toExtension)

Premises used: Algebra.Extension.Cotangent.mk_surjective
-- 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 : 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))
rw : Ideal.FG (RingHom.ker (F := MvPolynomial α R →ₐ[R] S) (aeval P.val))
⊢ P.ker.FG

Tactic:
rw [P.ker_eq_ker_aeval_val]

Premises used: Algebra.Generators.ker_eq_ker_aeval_val
-- 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 : 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))
hf₁ : Function.Surjective (α := P.Ring) (β := S) (⇑(aeval P.val) : (a : P.Ring) → S)
⊢ Ideal.FG (RingHom.ker (F := MvPolynomial α R →ₐ[R] S) (aeval P.val))

Tactic:
apply FinitePresentation.ker_fG_of_surjective

Premises used: Algebra.FinitePresentation.ker_fG_of_surjective
-- 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 : 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) (⇑(algebraMap P.Ring S) : (a : P.Ring) → S)

Tactic:
P.algebraMap_surjective

Premises used: Algebra.Generators.algebraMap_surjective
-- 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_1 : 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))
h : Eq (α := P.Ring → S) (⇑(aeval P.val) : (a : P.Ring) → S) (⇑(algebraMap P.Ring S) : (a : P.Ring) → S)
⊢ Function.Surjective (α := P.Ring) (β := S) (⇑(aeval P.val) : (a : P.Ring) → S)

Tactic:
convert! P.algebraMap_surjective

Premises used: Algebra.Generators.algebraMap_surjective
-- 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 : 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))
⊢ Eq (α := P.Ring → S) (⇑(aeval P.val) : (a : P.Ring) → S) (⇑(algebraMap P.Ring S) : (a : P.Ring) → S)

Tactic:
simp [P.algebraMap_eq]

Premises used: Algebra.Generators.algebraMap_eq
-- 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 : 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

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]
-- 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 : 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
⊢ J ≤ P.ker

Tactic:
simp [J, Ideal.span_le, Set.range_subset_iff]

Premises used: Ideal.span_le, Set.range_subset_iff
-- 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 : 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
⊢ J ≤ P.ker

Tactic:
have hJ : J ≤ P.ker := by simp [J, Ideal.span_le, Set.range_subset_iff]
-- 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 : 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
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) ⋯) :
              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:
obtain ⟨g, hgmem, hg⟩ := Submodule.exists_sub_one_mem_and_smul_le_of_fg_of_le_sup hJfg le_rfl hJ

Premises used: le_rfl, Submodule.exists_sub_one_mem_and_smul_le_of_fg_of_le_sup
-- 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 : 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
g : P.Ring
hgmem : g - 1 ∈ P.ker
hg : g • P.ker ≤ J
D : Aux P b₀ := { f := f, hf := hf, g := g, hgmem := hgmem, hg := hg }
⊢ ∃ (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:
⟨D.pres, D.basis, D.pres_val_comp_inr, D.basis_apply⟩

Premises used: _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.pres, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.pres_val_comp_inr, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.basis_apply, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.basis, And.intro, Exists.intro
-- 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 : 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
g : P.Ring
hgmem : g - 1 ∈ P.ker
hg : g • P.ker ≤ J
D : Aux P b₀ := { f := f, hf := hf, g := g, hgmem := hgmem, hg := hg }
⊢ ∃ (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:
exact ⟨D.pres, D.basis, D.pres_val_comp_inr, D.basis_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
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
inr : 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)

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⟩
-- 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 : 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.ker ≤ (Submodule.subtype P.ker).range

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
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
⊢ J ≤ (Submodule.subtype P.ker).range

Tactic:
simpa using hJ
-- 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 : 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.ker • P.ker ≤ (Submodule.subtype P.ker).range

Tactic:
simp [Ideal.mul_le_left]

Premises used: Ideal.mul_le_left
-- 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 : 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
inr : ⊤ ≤ Submodule.comap (Submodule.subtype P.ker) J ⊔ P.ker • Submodule.comap (Submodule.subtype P.ker) P.ker
⊢ P.ker ≤ J ⊔ P.ker • P.ker

Tactic:
rw [← Submodule.comap_le_comap_iff_of_le_range (f := P.ker.subtype) (by simp),
    Submodule.comap_subtype_self,
    Submodule.comap_sup_of_injective P.ker.subtype_injective (by simpa using hJ)
    (by simp [Ideal.mul_le_left]),
    Submodule.comap_smul'' P.ker.subtype_injective (by simp)]

Premises used: Algebra.Generators.ker, Submodule.comap_le_comap_iff_of_le_range, Submodule.comap_subtype_self, Submodule.comap_smul'', Submodule.subtype_injective, Submodule.comap_sup_of_injective
-- 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 : 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
inr :
  ⊤ ≤
    Submodule.comap (Submodule.subtype P.ker)
        (Ideal.span (Set.range (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.ker) ∘ v))) ⊔
      HSMul.hSMul (β := Submodule P.Ring ↥P.ker) P.ker ⊤
⊢ ⊤ ≤ Submodule.comap (Submodule.subtype P.ker) J ⊔ P.ker • Submodule.comap (Submodule.subtype P.ker) P.ker

Tactic:
simp only [Submodule.comap_subtype_self, J]

Premises used: Submodule.comap_subtype_self
-- 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 : 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
inr :
  LE.le (α := Submodule P.Ring ↥P.ker) ⊤ (Submodule.span P.Ring (Set.range v) ⊔ LinearMap.ker Extension.Cotangent.mk)
⊢ ⊤ ≤
    Submodule.comap (Submodule.subtype P.ker)
        (Ideal.span (Set.range (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.ker) ∘ v))) ⊔
      HSMul.hSMul (β := Submodule P.Ring ↥P.ker) P.ker ⊤

Tactic:
rw [← Submodule.coe_subtype, Ideal.span, Set.range_comp, ← Submodule.map_span,
    Submodule.comap_map_eq_of_injective P.ker.subtype_injective,
    ← Extension.Cotangent.ker_mk]

Premises used: Algebra.Generators.ker, Set.range_comp, Submodule.comap_map_eq_of_injective, Submodule.coe_subtype, Ideal.span, Submodule.map_span, Submodule.subtype_injective, Algebra.Extension.Cotangent.ker_mk