awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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) ((map f₂ ∘ₗ map f₁ : (a : P₁.H1Cotangent) → P₁.H1Cotangent) x : P₁.H1Cotangent)
    ((LinearMap.id : (a : P₁.H1Cotangent) → P₁.H1Cotangent) x : P₁.H1Cotangent)
have rw : Eq (α := P₁.H1Cotangent)
  (((↑S :
              {S_1 : Type v} →
                {M : Type u_2} →
                  {M₂ : Type u_1} →
                    [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: rw [← Extension.H1Cotangent.map_id, eq_comm, map_eq _ (f₂.comp f₁),
      Extension.H1Cotangent.map_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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) ((map f₁ ∘ₗ map f₂ : (a : P₂.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)
    ((LinearMap.id : (a : P₂.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)
have rw : 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: rw [← Extension.H1Cotangent.map_id, eq_comm, map_eq _ (f₁.comp f₂),
      Extension.H1Cotangent.map_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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
⊢ 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)
have 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)
Tactic: ext j
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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.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)
have 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)
Tactic: simp only [cotangentRestrict, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    Finsupp.lcomapDomain_apply, Finsupp.comapDomain_apply, Extension.cotangentComplex_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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 : ι'
⊢ 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')
have 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')
Tactic: rw [cotangentSpaceBasis_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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 : ι'
⊢ 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')
have simp : Eq.{v' + 1} (α := S')
  ((((P'.cotangentSpaceBasis.repr :
              (a :
                  { Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                      algebra₂ := P'.instRing, isScalarTower := sorry, σ := P'.σ, algebraMap_σ := sorry }.CotangentSpace) →
                ι' →₀ S')
            ((CotangentSpace.map f.toExtensionHom :
                (a :
                    { Ring := P.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                        algebra₂ := P.instRing, isScalarTower := sorry, σ := P.σ, algebraMap_σ := sorry }.CotangentSpace) →
                  { Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                      algebra₂ := P'.instRing, isScalarTower := sorry, σ := P'.σ, algebraMap_σ := sorry }.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]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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])
        ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i) :
      Ω[S⁄R])
    ((D R S : (a : S) → Ω[S⁄R]) (P.val i) : Ω[S⁄R])
have 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])
Tactic: rw [cotangentSpaceBasis_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (hypothesis)
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
⊢ Module.FinitePresentation S Ω[S⁄R]
have this : FiniteType R P.toExtension.Ring
Tactic: have : Algebra.FiniteType R P.toExtension.Ring := by simp [P]; infer_instance
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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]
have refine : P.toExtension.toKaehler.ker.FG
Tactic: refine Module.finitePresentation_of_surjective _ P.toExtension.toKaehler_surjective ?_
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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
⊢ P.toExtension.toKaehler.ker.FG
have rw : (Submodule.map P.toExtension.cotangentComplex ⊤).FG
Tactic: rw [LinearMap.exact_iff.mp P.toExtension.exact_cotangentComplex_toKaehler, ← Submodule.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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 : 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
e : S ≃ₐ[R] S'
this_1 : Algebra S S' := e.toRingEquiv.toRingHom.toAlgebra
this_2 : Algebra S' S := e.symm.toRingEquiv.toRingHom.toAlgebra
this_3 : IsScalarTower R S S'
this_4 : IsScalarTower R S' S
this_5 : IsScalarTower S S' S
this : IsScalarTower S' S S'
x : H1Cotangent R S
⊢ ((↑S :
              {S_1 : Type u_2} →
                {M : Type (max u u_2)} →
                  {M₂ : Type (max u v)} →
                    [inst : Semiring S] →
                      [inst_11 : Semiring S_1] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] →
                                [inst_16 : Module S_1 M] →
                                  [inst_17 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (map R R S' S) ∘ₗ
          map R R S S' :
        (a : H1Cotangent R S) → H1Cotangent R S)
      x =
    x
have rw : ((↑S :
            {S_1 : Type u_2} →
              {M : Type (max u u_2)} →
                {M₂ : Type (max u v)} →
                  [inst : Semiring S] →
                    [inst_11 : Semiring S_1] →
                      [inst_12 : AddCommMonoid M] →
                        [inst_13 : AddCommMonoid M₂] →
                          [inst_14 : Module S M] →
                            [inst_15 : Module S M₂] →
                              [inst_16 : Module S_1 M] →
                                [inst_17 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
          (Extension.H1Cotangent.map
            (Generators.Hom.toExtensionHom (Generators.defaultHom (Generators.self R S') (Generators.self R S)))) ∘ₗ
        map R R S S' :
      (a : H1Cotangent R S) → H1Cotangent R S)
    x =
  x
Tactic: rw [map, map, ← Extension.H1Cotangent.map_comp, Extension.H1Cotangent.map_eq,
        Extension.H1Cotangent.map_id, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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 : 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
e : S ≃ₐ[R] S'
this_1 : Algebra S S' := e.toRingEquiv.toRingHom.toAlgebra
this_2 : Algebra S' S := e.symm.toRingEquiv.toRingHom.toAlgebra
this_3 : IsScalarTower R S S'
this_4 : IsScalarTower R S' S
this_5 : IsScalarTower S S' S
this : IsScalarTower S' S S'
x : H1Cotangent R S'
⊢ ((↑S' :
              {S : Type v} →
                {M : Type (max u v)} →
                  {M₂ : Type (max u u_2)} →
                    [inst : Semiring S'] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module S' M] →
                              [inst_15 : Module S' M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S' S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[S'] M₂)
            (map R R S S') ∘ₗ
          map R R S' S :
        (a : H1Cotangent R S') → H1Cotangent R S')
      x =
    x
have rw : ((↑S' :
            {S : Type v} →
              {M : Type (max u v)} →
                {M₂ : Type (max u u_2)} →
                  [inst : Semiring S'] →
                    [inst_11 : Semiring S] →
                      [inst_12 : AddCommMonoid M] →
                        [inst_13 : AddCommMonoid M₂] →
                          [inst_14 : Module S' M] →
                            [inst_15 : Module S' M₂] →
                              [inst_16 : Module S M] →
                                [inst_17 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S' S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[S'] M₂)
          (Extension.H1Cotangent.map
            (Generators.Hom.toExtensionHom (Generators.defaultHom (Generators.self R S) (Generators.self R S')))) ∘ₗ
        map R R S' S :
      (a : H1Cotangent R S') → H1Cotangent R S')
    x =
  x
Tactic: rw [map, map, ← Extension.H1Cotangent.map_comp, Extension.H1Cotangent.map_eq,
        Extension.H1Cotangent.map_id, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (hypothesis)
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
⊢ Module.Finite S (H1Cotangent R S)
have this : FiniteType R P.toExtension.Ring
Tactic: have : Algebra.FiniteType R P.toExtension.Ring := by simp [P]; infer_instance
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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 S (H1Cotangent R S)
have suffices : Module.Finite.{v, u} S P.toExtension.H1Cotangent
Tactic: suffices Module.Finite S P.toExtension.H1Cotangent from
    .of_surjective P.equivH1Cotangent.toLinearMap P.equivH1Cotangent.surjective
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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.H1Cotangent
have rw : (LinearMap.ker (M₂ := ↥P.toExtension.cotangentComplex.range) P.toExtension.cotangentComplex.rangeRestrict).FG
Tactic: rw [Module.finite_def, Submodule.fg_top, ← LinearMap.ker_rangeRestrict]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (hypothesis)
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
⊢ (LinearMap.ker (M₂ := ↥P.toExtension.cotangentComplex.range) P.toExtension.cotangentComplex.rangeRestrict).FG
have this₁ : Module.Finite.{v, u} S P.toExtension.Cotangent
Tactic: have := Extension.Cotangent.finite P.fg_ker
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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
have rw : Module.FinitePresentation S ↥P.toExtension.toKaehler.ker
Tactic: rw [← LinearMap.exact_iff.mp P.toExtension.exact_cotangentComplex_toKaehler]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (hypothesis)
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
⊢ (LinearMap.ker (M₂ := ↥P.toExtension.cotangentComplex.range) P.toExtension.cotangentComplex.rangeRestrict).FG
have this₁ : 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 _)