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
P_1 : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
P : Extension R S
P₁ : Extension.{u_1, u, v} R S
P₂ : Extension.{u_2, u, v} R S
f₁ : P₁.Hom P₂
f₂ : P₂.Hom P₁
x : P₂.H1Cotangent
⊢ Eq (α := P₂.H1Cotangent)
    (((↑S :
                {S_1 : Type v} →
                  {M : Type u_1} →
                    {M₂ : Type u_2} →
                      [inst : Semiring S] →
                        [inst_24 : Semiring S_1] →
                          [inst_25 : AddCommMonoid M] →
                            [inst_26 : AddCommMonoid M₂] →
                              [inst_27 : Module S M] →
                                [inst_28 : Module S M₂] →
                                  [inst_29 : Module S_1 M] →
                                    [inst_30 : Module S_1 M₂] →
                                      [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              (map f₁) ∘ₗ
            map f₂ :
          (a : P₂.H1Cotangent) → P₂.H1Cotangent)
        x :
      P₂.H1Cotangent)
    ((map f₁ ∘ₗ map f₂ : (a : P₂.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)

Tactic:
rfl
-- 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
P : Generators R S ι
r : S
x : P.Ring
i : ι
⊢ (((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
            (r ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) x) :
          ι →₀ S) :
        (a : ι) → S)
      i =
    HMul.hMul (β := S) r
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv i : (a : MvPolynomial ι R) → MvPolynomial ι R) x : MvPolynomial ι R) :
        S)

Tactic:
simp only [cotangentSpaceBasis, Basis.baseChange_repr_tmul, mvPolynomialBasis_repr_apply,
    Algebra.smul_def, mul_comm r, algebraMap_apply, toExtension]

Premises used: Algebra.Generators.algebraMap_apply, Algebra.Generators.cotangentSpaceBasis, KaehlerDifferential.mvPolynomialBasis_repr_apply, Module.Basis.baseChange_repr_tmul, mul_comm, Algebra.smul_def, Algebra.Generators.toExtension
-- 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
P : Generators R S ι
r : S
x : P.Ring
i : ι
⊢ (((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
            (r ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) x) :
          ι →₀ S) :
        (a : ι) → S)
      i =
    HMul.hMul (β := S) r
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv i : (a : MvPolynomial ι R) → MvPolynomial ι R) x : MvPolynomial ι R) :
        S)

Tactic:
classical
  simp only [cotangentSpaceBasis, Basis.baseChange_repr_tmul, mvPolynomialBasis_repr_apply,
    Algebra.smul_def, mul_comm r, algebraMap_apply, toExtension]

Premises used: Algebra.Generators.algebraMap_apply, Algebra.Generators.cotangentSpaceBasis, KaehlerDifferential.mvPolynomialBasis_repr_apply, Module.Basis.baseChange_repr_tmul, mul_comm, Algebra.smul_def, Algebra.Generators.toExtension
-- 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
P : Generators R S ι
x : P.toExtension.Ring
i : ι
⊢ Eq.{v + 1} (α := S)
    ((((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
              (1 ⊗ₜ[P.toExtension.Ring]
                (D R P.toExtension.Ring : (a : P.toExtension.Ring) → Ω[P.toExtension.Ring⁄R]) x) :
            ι →₀ S) :
          (a : ι) → S)
        i :
      S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv i : (a : MvPolynomial ι R) → MvPolynomial ι R) x : MvPolynomial ι R) :
      S)

Tactic:
simp
-- 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
P : Generators R S ι
i : ι
⊢ Eq (α := P.toExtension.CotangentSpace)
    ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i : P.toExtension.CotangentSpace)
    (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i) : S ⊗[P.Ring] Ω[P.Ring⁄R])

Tactic:
simp [cotangentSpaceBasis, toExtension]

Premises used: Algebra.Generators.cotangentSpaceBasis, Algebra.Generators.toExtension
-- 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
P_1 P : Generators R S ι
⊢ Free S P.toExtension.CotangentSpace

Tactic:
.of_basis P.cotangentSpaceBasis

Premises used: Algebra.Generators.cotangentSpaceBasis, Module.Free.of_basis
-- 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
P : Generators R S ι
σ : Type u_1
u : σ → ι
hu : Function.Injective u
x : ↥P.ker
h :
  ∀ (j : σ),
    Eq.{v + 1} (α := S)
      ((((P.cotangentRestrict hu : (a : P.toExtension.Cotangent) → σ →₀ S)
                ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x) :
              σ →₀ S) :
            (a : σ) → S)
          j :
        S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (u j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
⊢ Eq (α := (a : σ) → S)
    (⇑((P.cotangentRestrict hu : (a : P.toExtension.Cotangent) → σ →₀ S)
            ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x) :
          σ →₀ S) :
      (a : σ) → S)
    fun (j : σ) ↦
    (aeval P.val : (a : MvPolynomial ι R) → S)
      ((pderiv (u j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R)

Tactic:
ext j
-- 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
P : Generators R S ι
σ : Type u_1
u : σ → ι
hu : Function.Injective u
x : ↥P.ker
j : σ
h :
  Eq.{v + 1} (α := S)
    ((((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
              (1 ⊗ₜ[P.toExtension.Ring]
                (D R P.toExtension.Ring : (a : P.toExtension.Ring) → Ω[P.toExtension.Ring⁄R])
                  (↑x : P.toExtension.Ring)) :
            ι →₀ S) :
          (a : ι) → S)
        (u j) :
      S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (u j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
      S)
⊢ Eq.{v + 1} (α := S)
    ((((P.cotangentRestrict hu : (a : P.toExtension.Cotangent) → σ →₀ S)
              ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x) :
            σ →₀ S) :
          (a : σ) → S)
        j :
      S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (u j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
      S)

Tactic:
simp only [cotangentRestrict, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    Finsupp.lcomapDomain_apply, Finsupp.comapDomain_apply, Extension.cotangentComplex_mk]

Premises used: Finsupp.lcomapDomain_apply, Finsupp.comapDomain_apply, LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_coe, Algebra.Extension.cotangentComplex_mk, Algebra.Generators.cotangentRestrict
-- 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
P : Generators R S ι
σ : Type u_1
u : σ → ι
hu : Function.Injective u
x : ↥P.ker
j : σ
⊢ Eq.{v + 1} (α := S)
    ((((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
              (1 ⊗ₜ[P.toExtension.Ring]
                (D R P.toExtension.Ring : (a : P.toExtension.Ring) → Ω[P.toExtension.Ring⁄R])
                  (↑x : P.toExtension.Ring)) :
            ι →₀ S) :
          (a : ι) → S)
        (u j) :
      S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (u j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
      S)

Tactic:
simp only [toExtension_Ring, P.cotangentSpaceBasis_repr_tmul, one_mul]

Premises used: Algebra.Generators.cotangentSpaceBasis_repr_tmul, Algebra.Generators.toExtension_Ring, one_mul
-- 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
P : Generators R S ι
R' : Type u'
S' : Type v'
ι' : Type w'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f : P.Hom P'
i : ι
j : ι'
rw :
  Eq.{v' + 1} (α := S')
    ((((P'.cotangentSpaceBasis.repr : (a : P'.toExtension.CotangentSpace) → ι' →₀ S')
              ((CotangentSpace.map f.toExtensionHom :
                  (a : P.toExtension.CotangentSpace) → P'.toExtension.CotangentSpace)
                (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i))) :
            ι' →₀ S') :
          (a : ι') → S')
        j :
      S')
    ((aeval P'.val : (a : MvPolynomial ι' R') → S')
        ((pderiv j : (a : MvPolynomial ι' R') → MvPolynomial ι' R') (f.val i) : MvPolynomial ι' R') :
      S')
⊢ Eq.{v' + 1} (α := S')
    ((((P'.cotangentSpaceBasis.repr : (a : P'.toExtension.CotangentSpace) → ι' →₀ S')
              ((CotangentSpace.map f.toExtensionHom :
                  (a : P.toExtension.CotangentSpace) → P'.toExtension.CotangentSpace)
                ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i)) :
            ι' →₀ S') :
          (a : ι') → S')
        j :
      S')
    ((aeval P'.val : (a : MvPolynomial ι' R') → S')
        ((pderiv j : (a : MvPolynomial ι' R') → MvPolynomial ι' R') (f.val i) : MvPolynomial ι' R') :
      S')

Tactic:
rw [cotangentSpaceBasis_apply]

Premises used: Algebra.Generators.cotangentSpaceBasis_apply
-- 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
P : Generators R S ι
R' : Type u'
S' : Type v'
ι' : Type w'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f : P.Hom P'
i : ι
j : ι'
simp :
  Eq.{v' + 1} (α := S')
    ((((P'.cotangentSpaceBasis.repr :
                (a :
                    { Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                        algebra₂ := P'.instRing, isScalarTower := ⋯, σ := P'.σ, algebraMap_σ := ⋯ }.CotangentSpace) →
                  ι' →₀ S')
              ((CotangentSpace.map f.toExtensionHom :
                  (a :
                      { Ring := P.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                          algebra₂ := P.instRing, isScalarTower := ⋯, σ := P.σ, algebraMap_σ := ⋯ }.CotangentSpace) →
                    { Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                        algebra₂ := P'.instRing, isScalarTower := ⋯, σ := P'.σ, algebraMap_σ := ⋯ }.CotangentSpace)
                (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i))) :
            ι' →₀ S') :
          (a : ι') → S')
        j :
      S')
    ((aeval P'.val : (a : MvPolynomial ι' R') → S')
        ((pderiv j : (a : MvPolynomial ι' R') → MvPolynomial ι' R') (f.val i) : MvPolynomial ι' R') :
      S')
⊢ Eq.{v' + 1} (α := S')
    ((((P'.cotangentSpaceBasis.repr : (a : P'.toExtension.CotangentSpace) → ι' →₀ S')
              ((CotangentSpace.map f.toExtensionHom :
                  (a : P.toExtension.CotangentSpace) → P'.toExtension.CotangentSpace)
                (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i))) :
            ι' →₀ S') :
          (a : ι') → S')
        j :
      S')
    ((aeval P'.val : (a : MvPolynomial ι' R') → S')
        ((pderiv j : (a : MvPolynomial ι' R') → MvPolynomial ι' R') (f.val i) : MvPolynomial ι' R') :
      S')

Tactic:
simp only [toExtension]

Premises used: Algebra.Generators.toExtension
-- 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
P : Generators R S ι
i : ι
⊢ HSMul.hSMul (α := S) (β := Ω[S⁄R]) 1
      ((KaehlerDifferential.map R R P.toExtension.Ring S : (a : Ω[P.toExtension.Ring⁄R]) → Ω[S⁄R])
          ((D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i)) :
        Ω[S⁄R]) =
    (D R S : (a : S) → Ω[S⁄R]) (P.val i)

Tactic:
simp
-- 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
P : Generators R S ι
i : ι
rw :
  Eq.{v + 1} (α := Ω[S⁄R])
    ((P.toExtension.toKaehler : (a : P.toExtension.CotangentSpace) → Ω[S⁄R])
        (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i)) :
      Ω[S⁄R])
    ((D R S : (a : S) → Ω[S⁄R]) (P.val i) : Ω[S⁄R])
⊢ Eq.{v + 1} (α := Ω[S⁄R])
    ((P.toExtension.toKaehler : (a : P.toExtension.CotangentSpace) → Ω[S⁄R])
        ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i) :
      Ω[S⁄R])
    ((D R S : (a : S) → Ω[S⁄R]) (P.val i) : Ω[S⁄R])

Tactic:
rw [cotangentSpaceBasis_apply]

Premises used: Algebra.Generators.cotangentSpaceBasis_apply
-- 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
P : Generators R S ι
i : ι
⊢ Eq.{v + 1} (α := Ω[S⁄R])
    ((P.toExtension.toKaehler : (a : P.toExtension.CotangentSpace) → Ω[S⁄R])
        (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i)) :
      Ω[S⁄R])
    ((D R S : (a : S) → Ω[S⁄R]) (P.val i) : Ω[S⁄R])

Tactic:
toKaehler_tmul_D i

Premises used: AddMonoidAlgebra.singleZeroRingHom, Algebra.Generators.toKaehler_tmul_D, AddMonoidAlgebra, Finsupp.single
-- 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
P : Generators R S ι
i : ι
⊢ Eq.{v + 1} (α := Ω[S⁄R])
    ((P.toExtension.toKaehler : (a : P.toExtension.CotangentSpace) → Ω[S⁄R])
        (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i)) :
      Ω[S⁄R])
    ((D R S : (a : S) → Ω[S⁄R]) (P.val i) : Ω[S⁄R])

Tactic:
exact toKaehler_tmul_D i

Premises used: Algebra.Generators.toKaehler_tmul_D
-- 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
inst_3 : FinitePresentation R S
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
⊢ FiniteType R
    (Generators.Ring (ι := Fin (Presentation.ofFinitePresentationVars R S))
      (Presentation.toGenerators (Presentation.ofFinitePresentation R S)))

Tactic:
infer_instance
-- 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
inst_3 : FinitePresentation R S
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
⊢ FiniteType R P.toExtension.Ring

Tactic:
have : Algebra.FiniteType R P.toExtension.Ring := by simp [P]; infer_instance
-- 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
inst_3 : FinitePresentation R S
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this : FiniteType R P.toExtension.Ring
⊢ Module.FinitePresentation S Ω[S⁄R]

Tactic:
Module.finitePresentation_of_surjective _ P.toExtension.toKaehler_surjective ?_

Premises used: Module.finitePresentation_of_surjective, Algebra.Extension.toKaehler_surjective
-- 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
inst_3 : FinitePresentation R S
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this : FiniteType R P.toExtension.Ring
refine : P.toExtension.toKaehler.ker.FG
⊢ Module.FinitePresentation S Ω[S⁄R]

Tactic:
refine Module.finitePresentation_of_surjective _ P.toExtension.toKaehler_surjective ?_

Premises used: Module.finitePresentation_of_surjective, Algebra.Extension.toKaehler_surjective
-- 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
inst_3 : FinitePresentation R S
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this : FiniteType R P.toExtension.Ring
rw : (Submodule.map P.toExtension.cotangentComplex ⊤).FG
⊢ P.toExtension.toKaehler.ker.FG

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

Premises used: Submodule.map_top, 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
inst_3 : FinitePresentation R S
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this : FiniteType R P.toExtension.Ring
⊢ (Submodule.map P.toExtension.cotangentComplex ⊤).FG

Tactic:
(Extension.Cotangent.finite P.fg_ker).1.map P.toExtension.cotangentComplex

Premises used: Module.Finite.fg_top, Submodule.FG.map, Algebra.Extension.cotangentComplex, Algebra.Generators.toExtension, 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
inst_3 : FinitePresentation R S
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this : FiniteType R P.toExtension.Ring
⊢ (Submodule.map P.toExtension.cotangentComplex ⊤).FG

Tactic:
exact (Extension.Cotangent.finite P.fg_ker).1.map P.toExtension.cotangentComplex

Premises used: Module.Finite.fg_top, Submodule.FG.map, Algebra.Extension.cotangentComplex, Algebra.Generators.toExtension, 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
⊢ FiniteType R
    (Generators.Ring (ι := Fin (Presentation.ofFinitePresentationVars R S))
      (Presentation.toGenerators (Presentation.ofFinitePresentation R S)))

Tactic:
infer_instance
-- 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
⊢ FiniteType R P.toExtension.Ring

Tactic:
have : Algebra.FiniteType R P.toExtension.Ring := by simp [P]; infer_instance
-- 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 : FiniteType R P.toExtension.Ring
suffices : Module.Finite.{v, u} S P.toExtension.H1Cotangent
⊢ Module.Finite S (H1Cotangent R S)

Tactic:
suffices Module.Finite S P.toExtension.H1Cotangent from
    .of_surjective P.equivH1Cotangent.toLinearMap P.equivH1Cotangent.surjective
-- 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 : FiniteType R P.toExtension.Ring
rw : (LinearMap.ker (M₂ := ↥P.toExtension.cotangentComplex.range) P.toExtension.cotangentComplex.rangeRestrict).FG
⊢ Module.Finite.{v, u} S P.toExtension.H1Cotangent

Tactic:
rw [Module.finite_def, Submodule.fg_top, ← LinearMap.ker_rangeRestrict]

Premises used: LinearMap.ker_rangeRestrict, Module.finite_def, Submodule.fg_top
-- 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 : FiniteType R P.toExtension.Ring
⊢ Module.Finite.{v, u} S P.toExtension.Cotangent

Tactic:
have := Extension.Cotangent.finite P.fg_ker