awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type w
ι' : Type u_1
P_1 : Generators R S ι
S' : Type u_2
inst_3 : CommRing S'
inst_4 : Algebra R S'
T : Type w
inst_5 : CommRing T
inst_6 : Algebra R T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
inst_9 : Algebra S' T
inst_10 : IsScalarTower R S' T
inst_11 : FinitePresentation R S
inst_12 : Projective S Ω[S⁄R]
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this_1 : FiniteType R P.toExtension.Ring
this : Module.Finite.{v, u} S P.toExtension.Cotangent
rw : Module.FinitePresentation S ↥P.toExtension.toKaehler.ker
⊢ Module.FinitePresentation S ↥P.toExtension.cotangentComplex.range

Tactic:
rw [← LinearMap.exact_iff.mp P.toExtension.exact_cotangentComplex_toKaehler]

Premises used: Iff.mp, LinearMap.exact_iff, Algebra.Extension.exact_cotangentComplex_toKaehler
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type w
ι' : Type u_1
P_1 : Generators R S ι
S' : Type u_2
inst_3 : CommRing S'
inst_4 : Algebra R S'
T : Type w
inst_5 : CommRing T
inst_6 : Algebra R T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
inst_9 : Algebra S' T
inst_10 : IsScalarTower R S' T
inst_11 : FinitePresentation R S
inst_12 : Projective S Ω[S⁄R]
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this_1 : FiniteType R P.toExtension.Ring
this : Module.Finite.{v, u} S P.toExtension.Cotangent
⊢ Module.FinitePresentation S ↥P.toExtension.toKaehler.ker

Tactic:
Module.finitePresentation_of_projective_of_exact
      _ _ (Subtype.val_injective) P.toExtension.toKaehler_surjective
      (LinearMap.exact_subtype_ker_map _)

Premises used: Set.Mem, Module.finitePresentation_of_projective_of_exact, Algebra.Extension.toKaehler_surjective, LinearMap.exact_subtype_ker_map
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type w
ι' : Type u_1
P_1 : Generators R S ι
S' : Type u_2
inst_3 : CommRing S'
inst_4 : Algebra R S'
T : Type w
inst_5 : CommRing T
inst_6 : Algebra R T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
inst_9 : Algebra S' T
inst_10 : IsScalarTower R S' T
inst_11 : FinitePresentation R S
inst_12 : Projective S Ω[S⁄R]
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this_1 : FiniteType R P.toExtension.Ring
this : Module.Finite.{v, u} S P.toExtension.Cotangent
⊢ Module.FinitePresentation S ↥P.toExtension.toKaehler.ker

Tactic:
exact Module.finitePresentation_of_projective_of_exact
      _ _ (Subtype.val_injective) P.toExtension.toKaehler_surjective
      (LinearMap.exact_subtype_ker_map _)

Premises used: Module.finitePresentation_of_projective_of_exact, Algebra.Extension.toKaehler_surjective, LinearMap.exact_subtype_ker_map
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type w
ι' : Type u_1
P_1 : Generators R S ι
S' : Type u_2
inst_3 : CommRing S'
inst_4 : Algebra R S'
T : Type w
inst_5 : CommRing T
inst_6 : Algebra R T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
inst_9 : Algebra S' T
inst_10 : IsScalarTower R S' T
inst_11 : FinitePresentation R S
inst_12 : Projective S Ω[S⁄R]
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this_1 : FiniteType R P.toExtension.Ring
this : Module.Finite.{v, u} S P.toExtension.Cotangent
⊢ Module.FinitePresentation S ↥P.toExtension.cotangentComplex.range

Tactic:
have : Module.FinitePresentation S (LinearMap.range P.toExtension.cotangentComplex) := by
    rw [← LinearMap.exact_iff.mp P.toExtension.exact_cotangentComplex_toKaehler]
    exact Module.finitePresentation_of_projective_of_exact
      _ _ (Subtype.val_injective) P.toExtension.toKaehler_surjective
      (LinearMap.exact_subtype_ker_map _)
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type w
ι' : Type u_1
P_1 : Generators R S ι
S' : Type u_2
inst_3 : CommRing S'
inst_4 : Algebra R S'
T : Type w
inst_5 : CommRing T
inst_6 : Algebra R T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
inst_9 : Algebra S' T
inst_10 : IsScalarTower R S' T
inst_11 : FinitePresentation R S
inst_12 : Projective S Ω[S⁄R]
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this_1 : FiniteType R P.toExtension.Ring
this_2 : Module.Finite.{v, u} S P.toExtension.Cotangent
this : Module.FinitePresentation S ↥P.toExtension.cotangentComplex.range
⊢ (LinearMap.ker (M₂ := ↥P.toExtension.cotangentComplex.range) P.toExtension.cotangentComplex.rangeRestrict).FG

Tactic:
Module.FinitePresentation.fg_ker (N := LinearMap.range P.toExtension.cotangentComplex)
    _ P.toExtension.cotangentComplex.surjective_rangeRestrict

Premises used: Module.FinitePresentation.fg_ker, Set.Mem, Algebra.Extension.cotangentComplex, Algebra.Generators.toExtension, LinearMap.surjective_rangeRestrict, Algebra.Presentation.toGenerators
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type w
ι' : Type u_1
P_1 : Generators R S ι
S' : Type u_2
inst_3 : CommRing S'
inst_4 : Algebra R S'
T : Type w
inst_5 : CommRing T
inst_6 : Algebra R T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
inst_9 : Algebra S' T
inst_10 : IsScalarTower R S' T
inst_11 : FinitePresentation R S
inst_12 : Projective S Ω[S⁄R]
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this_1 : FiniteType R P.toExtension.Ring
this_2 : Module.Finite.{v, u} S P.toExtension.Cotangent
this : Module.FinitePresentation S ↥P.toExtension.cotangentComplex.range
⊢ (LinearMap.ker (M₂ := ↥P.toExtension.cotangentComplex.range) P.toExtension.cotangentComplex.rangeRestrict).FG

Tactic:
exact Module.FinitePresentation.fg_ker (N := LinearMap.range P.toExtension.cotangentComplex)
    _ P.toExtension.cotangentComplex.surjective_rangeRestrict

Premises used: Module.FinitePresentation.fg_ker
-- 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
simp_rw :
  ∀ (y : σ),
    (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
          D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))
        y ∈
      (↑(RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val)) : Set P.toExtension.Ring)
⊢ ∀ (a : MvPolynomial ι R),
    Membership.mem (γ := 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))))
        a →
      Eq.{u_2 + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) a : S) (0 : S)

Tactic:
simp_rw [← RingHom.mem_ker, ← SetLike.le_def, Ideal.span_le, Set.range_subset_iff]

Premises used: Ideal.span_le, RingHom.mem_ker, SetLike.le_def, 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
σ_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 : σ
⊢ (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
        D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))
      i ∈
    (↑(RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val)) : Set P.toExtension.Ring)

Tactic:
simpa only [Generators.toExtension_Ring, Generators.toExtension_commRing, Function.comp_apply,
    SetLike.mem_coe, RingHom.mem_ker, ← P.algebraMap_apply] using (D.f _).property

Premises used: Algebra.Generators.algebraMap_apply, RingHom.mem_ker, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.f, SetLike.mem_coe, Function.comp_apply, Algebra.Generators.toExtension_Ring, Subtype.property, 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
σ_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
inst_3 : Nontrivial S
⊢ Nontrivial D.T

Tactic:
RingHom.domain_nontrivial (algebraMap D.T S)

Premises used: Algebra.algebraMap, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.T, RingHom.domain_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
σ_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
⊢ IsScalarTower P.Ring D.T S

Tactic:
⟨fun x y z ↦ ?_⟩

Premises used: IsScalarTower.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
σ_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
refine : ∀ (x : P.Ring) (y : D.T) (z : S), (x • y) • z = x • y • z
⊢ IsScalarTower P.Ring D.T S

Tactic:
refine ⟨fun x y z ↦ ?_⟩
-- 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
x : P.Ring
y : D.T
z : S
obtain :
  ∀ (y : MvPolynomial ι R),
    HSMul.hSMul (β := D.T) x
          ((Ideal.Quotient.mk
                  (Ideal.span
                    (Set.range (ι := σ)
                      (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                        D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
                (a : MvPolynomial ι R) →
                  MvPolynomial ι R ⧸
                    Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
              y :
            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))))) •
        z =
      x •
        HSMul.hSMul (α := D.T)
          ((Ideal.Quotient.mk
                  (Ideal.span
                    (Set.range (ι := σ)
                      (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                        D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
                (a : MvPolynomial ι R) →
                  MvPolynomial ι R ⧸
                    Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
              y :
            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)))))
          z
⊢ (x • y) • z = x • y • z

Tactic:
obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y

Premises used: Ideal.Quotient.mk_surjective, rfl
-- 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
x : P.Ring
y : MvPolynomial ι R
z : P.Ring
⊢ HMul.hMul (β := S)
      (HMul.hMul (α := S) (β := S)
        ((algebraMap D.T S : (a : D.T) → S) ((algebraMap P.Ring D.T : (a : P.Ring) → D.T) x : D.T) : S)
        ((algebraMap D.T S : (a : D.T) → S)
            ((Ideal.Quotient.mk
                    (Ideal.span
                      (Set.range (ι := σ)
                        (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                          D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
                  (a : MvPolynomial ι R) →
                    MvPolynomial ι R ⧸
                      Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
                y :
              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))))) :
          S))
      ((aeval P.val : (a : MvPolynomial ι R) → S) z : S) =
    HMul.hMul (β := S)
      (HMul.hMul (α := S) (β := S) ((aeval P.val : (a : MvPolynomial ι R) → S) x : S)
        ((algebraMap D.T S : (a : D.T) → S)
            ((Ideal.Quotient.mk
                    (Ideal.span
                      (Set.range (ι := σ)
                        (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                          D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
                  (a : MvPolynomial ι R) →
                    MvPolynomial ι R ⧸
                      Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
                y :
              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))))) :
          S))
      ((aeval P.val : (a : MvPolynomial ι R) → S) z : S)

Tactic:
rfl
-- 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
⊢ HSMul.hSMul (β := Ideal P.Ring) (HPow.hPow (β := ℕ) D.g 1) (RingHom.ker (F := P.Ring →+* S) (algebraMap P.Ring S)) ≤
    RingHom.ker (F := P.Ring →+* D.T) (algebraMap P.Ring D.T)

Tactic:
simpa using D.hg

Premises used: _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.hg
-- 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
refine_1 : Function.Surjective (α := D.T) (β := S) (⇑(algebraMap D.T S) : (a : D.T) → S)
refine_2 : Function.Surjective (α := P.Ring) (β := D.T) (⇑(algebraMap P.Ring D.T) : (a : P.Ring) → D.T)
refine_3 : IsUnit.{u_2} (M := S) ((algebraMap P.Ring S : (a : P.Ring) → S) D.g : S)
⊢ IsLocalization.Away D.gbar S

Tactic:
refine .of_surjective_of_isScalarTower (n := 1) ?_ ?_ _ ?_ (by simpa using D.hg)
-- 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
⊢ Function.Surjective (α := D.T) (β := S) (⇑(algebraMap D.T S) : (a : D.T) → S)

Tactic:
.of_comp (g := algebraMap P.Ring D.T) ?_

Premises used: Function.Surjective.of_comp
-- 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
refine_1 :
  Function.Surjective (α := P.Ring) (β := S)
    (Function.comp (β := D.T) (⇑(algebraMap D.T S) : (a : D.T) → S) (⇑(algebraMap P.Ring D.T) : (a : P.Ring) → D.T))
⊢ Function.Surjective (α := D.T) (β := S) (⇑(algebraMap D.T S) : (a : D.T) → S)

Tactic:
refine .of_comp (g := algebraMap P.Ring D.T) ?_
-- 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
⊢ 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
σ_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
h :
  Eq (α := P.Ring → S)
    (Function.comp (β := D.T) (⇑(algebraMap D.T S) : (a : D.T) → S) (⇑(algebraMap P.Ring D.T) : (a : P.Ring) → D.T))
    (⇑(algebraMap P.Ring S) : (a : P.Ring) → S)
⊢ Function.Surjective (α := P.Ring) (β := S)
    (Function.comp (β := D.T) (⇑(algebraMap D.T S) : (a : D.T) → S) (⇑(algebraMap P.Ring D.T) : (a : P.Ring) → D.T))

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
σ_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
h :
  ∀ (x : P.Ring),
    Eq.{u_2 + 1} (α := S)
      (Function.comp (β := D.T) (⇑(algebraMap D.T S) : (a : D.T) → S) (⇑(algebraMap P.Ring D.T) : (a : P.Ring) → D.T)
          x :
        S)
      ((algebraMap P.Ring S : (a : P.Ring) → S) x : S)
⊢ Eq (α := P.Ring → S)
    (Function.comp (β := D.T) (⇑(algebraMap D.T S) : (a : D.T) → S) (⇑(algebraMap P.Ring D.T) : (a : P.Ring) → D.T))
    (⇑(algebraMap P.Ring S) : (a : P.Ring) → S)

Tactic:
ext x
-- 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
x : P.Ring
⊢ Eq.{u_2 + 1} (α := S)
    (Function.comp (β := D.T) (⇑(algebraMap D.T S) : (a : D.T) → S) (⇑(algebraMap P.Ring D.T) : (a : P.Ring) → D.T) x :
      S)
    ((algebraMap P.Ring S : (a : P.Ring) → S) x : S)

Tactic:
(IsScalarTower.algebraMap_apply _ D.T S x).symm

Premises used: _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.T, Eq.symm, IsScalarTower.algebraMap_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
σ_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
x : P.Ring
⊢ Eq.{u_2 + 1} (α := S)
    (Function.comp (β := D.T) (⇑(algebraMap D.T S) : (a : D.T) → S) (⇑(algebraMap P.Ring D.T) : (a : P.Ring) → D.T) x :
      S)
    ((algebraMap P.Ring S : (a : P.Ring) → S) x : S)

Tactic:
exact (IsScalarTower.algebraMap_apply _ D.T S x).symm

Premises used: _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.T, Eq.symm, IsScalarTower.algebraMap_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
σ_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
⊢ Function.Surjective (α := P.Ring) (β := D.T) (⇑(algebraMap P.Ring D.T) : (a : P.Ring) → D.T)

Tactic:
simp [T, Ideal.Quotient.mk_surjective]

Premises used: _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.T, Ideal.Quotient.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
σ_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
h : Eq.{u_2 + 1} (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) D.g : S) (1 : S)
⊢ IsUnit.{u_2} (M := S) ((algebraMap P.Ring S : (a : P.Ring) → S) D.g : S)

Tactic:
simp [h]
-- 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
refine_3 : Eq.{u_2 + 1} (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) D.g : S) (1 : S)
⊢ IsUnit.{u_2} (M := S) ((algebraMap P.Ring S : (a : P.Ring) → S) D.g : S)

Tactic:
suffices h : (algebraMap P.Ring S) D.g = 1 by simp [h]
-- 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
refine_3 : Membership.mem (γ := Ideal P.Ring) (RingHom.ker (F := P.Ring →+* S) (algebraMap P.Ring S)) (D.g - 1)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) D.g : S) (1 : S)

Tactic:
rw [← map_one (algebraMap P.Ring S), ← sub_eq_zero, ← map_sub, ← RingHom.mem_ker]

Premises used: Algebra.Generators.Ring, map_sub, Algebra.algebraMap, sub_eq_zero, RingHom.mem_ker, map_one
-- 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
⊢ Membership.mem (γ := Ideal P.Ring) (RingHom.ker (F := P.Ring →+* S) (algebraMap P.Ring S)) (D.g - 1)

Tactic:
D.hgmem

Premises used: Set.Mem, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.hgmem, AddMonoidAlgebra
-- 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
⊢ Membership.mem (γ := Ideal P.Ring) (RingHom.ker (F := P.Ring →+* S) (algebraMap P.Ring S)) (D.g - 1)

Tactic:
exact D.hgmem

Premises used: _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.hgmem