awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
inst_5 : IsStandardSmoothOfRelativeDimension n R S
w w_1 : Type
w_2 : Finite w_1
w_3 : Finite w
P : SubmersivePresentation R S w w_1
hP : P.dimension = n
⊢ IsStandardSmoothOfRelativeDimension n R T

Tactic:
exact (P.ofAlgEquiv e).isStandardSmoothOfRelativeDimension (by simpa)

Premises used: Algebra.SubmersivePresentation.ofAlgEquiv, Algebra.SubmersivePresentation.isStandardSmoothOfRelativeDimension
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsStandardSmooth R S
inst_8 : IsStandardSmooth S T
obtain :
  ∀ (w w_1 : Type) (w_2 : Finite w_1),
    Finite w →
      ∀ (P : SubmersivePresentation R S w w_1),
        ∃ (ι : Type) (σ : Type) (x : Finite σ), Finite ι ∧ Nonempty (SubmersivePresentation R T ι σ)
⊢ ∃ (ι : Type) (σ : Type) (x : Finite σ), Finite ι ∧ Nonempty (SubmersivePresentation R T ι σ)

Tactic:
obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›

Premises used: Algebra.IsStandardSmooth
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsStandardSmooth R S
inst_8 : IsStandardSmooth S T
w w_1 : Type
w_2 : Finite w_1
left : Finite w
P : SubmersivePresentation R S w w_1
obtain :
  ∀ (w w_3 : Type) (w_4 : Finite w_3),
    Finite w →
      ∀ (Q : SubmersivePresentation S T w w_3),
        ∃ (ι : Type) (σ : Type) (x : Finite σ), Finite ι ∧ Nonempty (SubmersivePresentation R T ι σ)
⊢ ∃ (ι : Type) (σ : Type) (x : Finite σ), Finite ι ∧ Nonempty (SubmersivePresentation R T ι σ)

Tactic:
obtain ⟨_, _, _, _, ⟨Q⟩⟩ := ‹IsStandardSmooth S T›

Premises used: Algebra.IsStandardSmooth
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsStandardSmooth R S
inst_8 : IsStandardSmooth S T
w w_1 : Type
w_2 : Finite w_1
left : Finite w
P : SubmersivePresentation R S w w_1
w_3 w_4 : Type
w_5 : Finite w_4
left_1 : Finite w_3
Q : SubmersivePresentation S T w_3 w_4
⊢ ∃ (ι : Type) (σ : Type) (x : Finite σ), Finite ι ∧ Nonempty (SubmersivePresentation R T ι σ)

Tactic:
⟨_, _, _, inferInstance, ⟨Q.comp P⟩⟩

Premises used: inferInstance, Nonempty.intro, And.intro, Exists.intro, Algebra.SubmersivePresentation.comp
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsStandardSmooth R S
inst_8 : IsStandardSmooth S T
w w_1 : Type
w_2 : Finite w_1
left : Finite w
P : SubmersivePresentation R S w w_1
w_3 w_4 : Type
w_5 : Finite w_4
left_1 : Finite w_3
Q : SubmersivePresentation S T w_3 w_4
⊢ ∃ (ι : Type) (σ : Type) (x : Finite σ), Finite ι ∧ Nonempty (SubmersivePresentation R T ι σ)

Tactic:
exact ⟨_, _, _, inferInstance, ⟨Q.comp P⟩⟩
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsStandardSmoothOfRelativeDimension n R S
inst_8 : IsStandardSmoothOfRelativeDimension m S T
obtain :
  ∀ (w w_1 : Type) (w_2 : Finite w_1),
    Finite w →
      ∀ (P : SubmersivePresentation R S w w_1) (hP : P.dimension = n),
        ∃ (ι : Type) (σ : Type) (x : Finite σ) (_ : Finite ι) (P : SubmersivePresentation R T ι σ), P.dimension = m + n
⊢ ∃ (ι : Type) (σ : Type) (x : Finite σ) (_ : Finite ι) (P : SubmersivePresentation R T ι σ), P.dimension = m + n

Tactic:
obtain ⟨_, _, _, _, P, hP⟩ := ‹IsStandardSmoothOfRelativeDimension n R S›

Premises used: Algebra.IsStandardSmoothOfRelativeDimension
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsStandardSmoothOfRelativeDimension n R S
inst_8 : IsStandardSmoothOfRelativeDimension m S T
w w_1 : Type
w_2 : Finite w_1
w_3 : Finite w
P : SubmersivePresentation R S w w_1
hP : P.dimension = n
obtain :
  ∀ (w w_4 : Type) (w_5 : Finite w_4),
    Finite w →
      ∀ (Q : SubmersivePresentation S T w w_4) (hQ : Q.dimension = m),
        ∃ (ι : Type) (σ : Type) (x : Finite σ) (_ : Finite ι) (P : SubmersivePresentation R T ι σ), P.dimension = m + n
⊢ ∃ (ι : Type) (σ : Type) (x : Finite σ) (_ : Finite ι) (P : SubmersivePresentation R T ι σ), P.dimension = m + n

Tactic:
obtain ⟨_, _, _, _, Q, hQ⟩ := ‹IsStandardSmoothOfRelativeDimension m S T›

Premises used: Algebra.IsStandardSmoothOfRelativeDimension
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsStandardSmoothOfRelativeDimension n R S
inst_8 : IsStandardSmoothOfRelativeDimension m S T
w w_1 : Type
w_2 : Finite w_1
w_3 : Finite w
P : SubmersivePresentation R S w w_1
hP : P.dimension = n
w_4 w_5 : Type
w_6 : Finite w_5
w_7 : Finite w_4
Q : SubmersivePresentation S T w_4 w_5
hQ : Q.dimension = m
⊢ ∃ (ι : Type) (σ : Type) (x : Finite σ) (_ : Finite ι) (P : SubmersivePresentation R T ι σ), P.dimension = m + n

Tactic:
⟨_, _, _, inferInstance, Q.comp P, hP ▸ hQ ▸ ?_⟩

Premises used: Eq.rec, inferInstance, Exists.intro, Algebra.SubmersivePresentation.comp
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsStandardSmoothOfRelativeDimension n R S
inst_8 : IsStandardSmoothOfRelativeDimension m S T
w w_1 : Type
w_2 : Finite w_1
w_3 : Finite w
P : SubmersivePresentation R S w w_1
hP : P.dimension = n
w_4 w_5 : Type
w_6 : Finite w_5
w_7 : Finite w_4
Q : SubmersivePresentation S T w_4 w_5
hQ : Q.dimension = m
⊢ Presentation.dimension
      (PreSubmersivePresentation.toPresentation (SubmersivePresentation.toPreSubmersivePresentation (Q.comp P))) =
    Q.dimension + P.dimension

Tactic:
apply PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension

Premises used: Algebra.PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
T : Type u_1
inst_4 : CommRing T
inst_5 : Algebra R T
inst_6 : IsStandardSmooth R S
obtain :
  ∀ (ι σ : Type) (w : Finite σ),
    Finite ι →
      ∀ (P : SubmersivePresentation R S ι σ),
        ∃ (ι : Type) (σ : Type) (x : Finite σ), Finite ι ∧ Nonempty (SubmersivePresentation T (T ⊗[R] S) ι σ)
⊢ ∃ (ι : Type) (σ : Type) (x : Finite σ), Finite ι ∧ Nonempty (SubmersivePresentation T (T ⊗[R] S) ι σ)

Tactic:
obtain ⟨ι, σ, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›

Premises used: Algebra.IsStandardSmooth
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
ι_1 : Type w
σ_1 : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ_1
T : Type u_1
inst_4 : CommRing T
inst_5 : Algebra R T
inst_6 : IsStandardSmooth R S
ι σ : Type
w : Finite σ
left : Finite ι
P : SubmersivePresentation R S ι σ
⊢ ∃ (ι : Type) (σ : Type) (x : Finite σ), Finite ι ∧ Nonempty (SubmersivePresentation T (T ⊗[R] S) ι σ)

Tactic:
⟨ι, σ, _, inferInstance, ⟨P.baseChange T⟩⟩

Premises used: inferInstance, Nonempty.intro, And.intro, Exists.intro, Algebra.SubmersivePresentation.baseChange
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
ι_1 : Type w
σ_1 : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ_1
T : Type u_1
inst_4 : CommRing T
inst_5 : Algebra R T
inst_6 : IsStandardSmooth R S
ι σ : Type
w : Finite σ
left : Finite ι
P : SubmersivePresentation R S ι σ
⊢ ∃ (ι : Type) (σ : Type) (x : Finite σ), Finite ι ∧ Nonempty (SubmersivePresentation T (T ⊗[R] S) ι σ)

Tactic:
exact ⟨ι, σ, _, inferInstance, ⟨P.baseChange T⟩⟩
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
T : Type u_1
inst_4 : CommRing T
inst_5 : Algebra R T
inst_6 : IsStandardSmoothOfRelativeDimension n R S
obtain :
  ∀ (w w_1 : Type) (w_2 : Finite w_1),
    Finite w →
      ∀ (P : SubmersivePresentation R S w w_1) (hP : P.dimension = n),
        ∃ (ι : Type) (σ : Type) (x : Finite σ) (_ : Finite ι) (P : SubmersivePresentation T (T ⊗[R] S) ι σ),
          P.dimension = n
⊢ ∃ (ι : Type) (σ : Type) (x : Finite σ) (_ : Finite ι) (P : SubmersivePresentation T (T ⊗[R] S) ι σ), P.dimension = n

Tactic:
obtain ⟨_, _, _, _, P, hP⟩ := ‹IsStandardSmoothOfRelativeDimension n R S›

Premises used: Algebra.IsStandardSmoothOfRelativeDimension
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
T : Type u_1
inst_4 : CommRing T
inst_5 : Algebra R T
inst_6 : IsStandardSmoothOfRelativeDimension n R S
w w_1 : Type
w_2 : Finite w_1
w_3 : Finite w
P : SubmersivePresentation R S w w_1
hP : P.dimension = n
⊢ ∃ (ι : Type) (σ : Type) (x : Finite σ) (_ : Finite ι) (P : SubmersivePresentation T (T ⊗[R] S) ι σ), P.dimension = n

Tactic:
⟨_, _, _, inferInstance, P.baseChange T, hP⟩

Premises used: inferInstance, Exists.intro, Algebra.SubmersivePresentation.baseChange
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
T : Type u_1
inst_4 : CommRing T
inst_5 : Algebra R T
inst_6 : IsStandardSmoothOfRelativeDimension n R S
w w_1 : Type
w_2 : Finite w_1
w_3 : Finite w
P : SubmersivePresentation R S w w_1
hP : P.dimension = n
⊢ ∃ (ι : Type) (σ : Type) (x : Finite σ) (_ : Finite ι) (P : SubmersivePresentation T (T ⊗[R] S) ι σ), P.dimension = n

Tactic:
exact ⟨_, _, _, inferInstance, P.baseChange T, hP⟩
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
inst_4 : Subsingleton S
⊢ IsStandardSmooth R S

Tactic:
⟨Unit, Unit, inferInstance, inferInstance, ⟨.ofSubsingleton R S⟩⟩

Premises used: inferInstance, Nonempty.intro, Unit, And.intro, Algebra.IsStandardSmooth.mk, Exists.intro, Algebra.SubmersivePresentation.ofSubsingleton
-- Module: Mathlib.RingTheory.Smooth.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
inst_4 : Subsingleton S
⊢ Presentation.dimension
      (PreSubmersivePresentation.toPresentation
        (SubmersivePresentation.toPreSubmersivePresentation (SubmersivePresentation.ofSubsingleton R S))) =
    0

Tactic:
simp [Presentation.dimension]

Premises used: Algebra.Presentation.dimension
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : PreSubmersivePresentation R S ι σ
x : ↥P.ker
i : σ
dsimp :
  Eq.{u_2 + 1} (α := S)
    ((Finsupp.linearEquivFunOnFinite S S σ : (a : σ →₀ S) → σ → S)
        ((Finsupp.lcomapDomain P.map ⋯ : (a : ι →₀ S) → σ →₀ S)
            ((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
              (1 ⊗ₜ[P.toExtension.Ring]
                (KaehlerDifferential.D R P.toExtension.Ring : (a : P.toExtension.Ring) → Ω[P.toExtension.Ring⁄R])
                  (↑x : P.toExtension.Ring))) :
          σ →₀ S)
        i :
      S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
      S)
⊢ Eq.{u_2 + 1} (α := S)
    ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S)
        ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x : P.toExtension.Cotangent) i :
      S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
      S)

Tactic:
dsimp only [cotangentComplexAux, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    cotangentComplex_mk]

Premises used: LinearMap.coe_comp, Algebra.PreSubmersivePresentation.cotangentComplexAux, Function.comp_apply, LinearEquiv.coe_coe, Algebra.Extension.cotangentComplex_mk
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : PreSubmersivePresentation R S ι σ
x : ↥P.ker
i : σ
⊢ Eq.{u_2 + 1} (α := S)
    ((Finsupp.linearEquivFunOnFinite S S σ : (a : σ →₀ S) → σ → S)
        ((Finsupp.lcomapDomain P.map ⋯ : (a : ι →₀ S) → σ →₀ S)
            ((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
              (1 ⊗ₜ[P.toExtension.Ring]
                (KaehlerDifferential.D R P.toExtension.Ring : (a : P.toExtension.Ring) → Ω[P.toExtension.Ring⁄R])
                  (↑x : P.toExtension.Ring))) :
          σ →₀ S)
        i :
      S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
      S)

Tactic:
simp only [Generators.toExtension_Ring, Finsupp.lcomapDomain_apply,
    Finsupp.linearEquivFunOnFinite_apply, Finsupp.comapDomain_apply,
    Generators.cotangentSpaceBasis_repr_tmul, one_mul]

Premises used: Algebra.Generators.cotangentSpaceBasis_repr_tmul, Finsupp.lcomapDomain_apply, Finsupp.comapDomain_apply, Finsupp.linearEquivFunOnFinite_apply, Algebra.Generators.toExtension_Ring, one_mul
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : PreSubmersivePresentation R S ι σ
x : ↥P.ker
rw :
  (∀ (x_1 : σ),
      Eq.{u_2 + 1} (α := S)
        ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S)
            ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x : P.toExtension.Cotangent) x_1 :
          S)
        (0 x_1 : S)) ↔
    ∀ (i : σ),
      Eq.{u_2 + 1} (α := S)
        ((aeval P.val : (a : MvPolynomial ι R) → S)
            ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
          S)
        (0 : S)
⊢ Eq (α := σ → S)
      ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S)
          ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x : P.toExtension.Cotangent) :
        σ → S)
      (0 : σ → S) ↔
    ∀ (i : σ),
      Eq.{u_2 + 1} (α := S)
        ((aeval P.val : (a : MvPolynomial ι R) → S)
            ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
          S)
        (0 : S)

Tactic:
rw [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : PreSubmersivePresentation R S ι σ
x : ↥P.ker
simp_rw :
  (∀ (x_1 : σ),
      Eq.{u_2 + 1} (α := S)
        ((aeval P.val : (a : MvPolynomial ι R) → S)
            ((pderiv (P.map x_1) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
          S)
        (0 x_1 : S)) ↔
    ∀ (i : σ),
      Eq.{u_2 + 1} (α := S)
        ((aeval P.val : (a : MvPolynomial ι R) → S)
            ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
          S)
        (0 : S)
⊢ (∀ (x_1 : σ),
      Eq.{u_2 + 1} (α := S)
        ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S)
            ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x : P.toExtension.Cotangent) x_1 :
          S)
        (0 x_1 : S)) ↔
    ∀ (i : σ),
      Eq.{u_2 + 1} (α := S)
        ((aeval P.val : (a : MvPolynomial ι R) → S)
            ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
          S)
        (0 : S)

Tactic:
simp_rw [cotangentComplexAux_apply, Pi.zero_apply]

Premises used: Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, Pi.zero_apply
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
rw : P.cotangentComplexAux.ker ≤ ⊥
⊢ Function.Injective (α := P.toExtension.Cotangent) (β := σ → S)
    (⇑P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S)

Tactic:
rw [← LinearMap.ker_eq_bot, eq_bot_iff]

Premises used: LinearMap.ker_eq_bot, eq_bot_iff
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : P.toExtension.Cotangent
hx : x ∈ P.cotangentComplexAux.ker
obtain :
  ∀ (x : ↥P.ker)
    (hx :
      Membership.mem (α := P.toExtension.Cotangent) P.cotangentComplexAux.ker
        ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x : P.toExtension.Cotangent)),
    Membership.mem (α := P.toExtension.Cotangent) (γ := Submodule S P.toExtension.Cotangent) ⊥
      ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x : P.toExtension.Cotangent)
⊢ Membership.mem (γ := Submodule S P.toExtension.Cotangent) ⊥ x

Tactic:
obtain ⟨(x : P.ker), rfl⟩ := Cotangent.mk_surjective x

Premises used: Algebra.Generators.ker, Algebra.SubmersivePresentation.toPreSubmersivePresentation, Algebra.PreSubmersivePresentation.toPresentation, Algebra.Extension.Cotangent.mk_surjective, Algebra.Presentation.toGenerators, rfl
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  Membership.mem (α := P.toExtension.Cotangent) P.cotangentComplexAux.ker
    ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x : P.toExtension.Cotangent)
rw : (↑x : P.toExtension.Ring) ∈ HPow.hPow (β := ℕ) P.toExtension.ker 2
⊢ Membership.mem (α := P.toExtension.Cotangent) (γ := Submodule S P.toExtension.Cotangent) ⊥
    ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x : P.toExtension.Cotangent)

Tactic:
rw [Submodule.mem_bot, Cotangent.mk_eq_zero_iff]

Premises used: Submodule.mem_bot, Algebra.Extension.Cotangent.mk_eq_zero_iff
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  Membership.mem (α := P.toExtension.Cotangent) P.cotangentComplexAux.ker
    ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x : P.toExtension.Cotangent)
⊢ ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)

Tactic:
rw [LinearMap.mem_ker, P.cotangentComplexAux_zero_iff] at hx

Premises used: Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, LinearMap.mem_ker
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
rw : (↑x : P.Ring) ∈ P.ker
⊢ Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (↑x : P.Ring)

Tactic:
rw [P.span_range_relation_eq_ker]

Premises used: Algebra.SubmersivePresentation.toPreSubmersivePresentation, Algebra.PreSubmersivePresentation.toPresentation, Algebra.Presentation.span_range_relation_eq_ker
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
⊢ (↑x : P.Ring) ∈ P.ker

Tactic:
x.property

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
⊢ (↑x : P.Ring) ∈ P.ker

Tactic:
exact x.property

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
⊢ Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (↑x : P.Ring)

Tactic:
have : x.val ∈ Ideal.span (Set.range P.relation) := by
    rw [P.span_range_relation_eq_ker]
    exact x.property
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (↑x : P.Ring) : MvPolynomial ι R) :
        S)
      (0 : S)
this : Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (↑x : P.Ring)
obtain :
  ∀ (c : σ →₀ P.Ring) (hc : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) = (↑x : P.Ring)),
    (↑x : P.toExtension.Ring) ∈ HPow.hPow (β := ℕ) P.toExtension.ker 2
⊢ (↑x : P.toExtension.Ring) ∈ HPow.hPow (β := ℕ) P.toExtension.ker 2

Tactic:
obtain ⟨c, hc⟩ := Finsupp.mem_ideal_span_range_iff_exists_finsupp.mp this

Premises used: Iff.mp, Finsupp.mem_ideal_span_range_iff_exists_finsupp