awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Quotient (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
⊢ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J)) ≤ f.ker
have this : ∀ {x : R} (h : x ∈ I * J),
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) x sorry)) :
      J.Cotangent)
    (0 : J.Cotangent)
Tactic: have {x : R} (h : x ∈ I * J) : f (J.toCotangent ⟨x, Ideal.mul_le_left h⟩) = 0 := by
    induction h using Submodule.mul_induction_on' with
    | mem_mul_mem y hy z hz =>
      rcases Submodule.mem_map.mp (le (f.mem_range_self (J.toCotangent ⟨z, hz⟩))) with ⟨w, hw, eqz⟩
      have mem_bot := Ideal.mul_mem_mul hy (Submodule.mem_comap.mp hw)
      simp only [← mul_assoc, sq, Submodule.bot_mul, Submodule.mem_bot] at mem_bot
      have eq0 : y • w = 0 := SetCoe.ext mem_bot
      have : ⟨y * z, Ideal.mul_le_left (Submodule.mul_mem_mul hy hz)⟩ = y • (⟨z, hz⟩ : J) := rfl
      rw [this, map_smul, map_smul, ← eqz, ← map_smul, eq0, map_zero]
    | add y ymem z zmem hy hz =>
      have : (⟨y + z, Ideal.mul_le_left (add_mem ymem zmem)⟩ : J) =
        ⟨y, Ideal.mul_le_left ymem⟩ + ⟨z, Ideal.mul_le_left zmem⟩ := rfl
      rw [this, map_add, map_add, hy, hz, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
this :
  ∀ {x : R} (h : x ∈ I * J),
    Eq (α := J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) x ⋯)) :
        J.Cotangent)
      (0 : J.Cotangent)
x : J.Cotangent
hx : x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
⊢ x ∈ f.ker
have rcases : ∀ (x' : ↥J) (hx' : x' ∈ Submodule.comap (Submodule.subtype J) (I * J))
  (eq : (J.toCotangent : (a : ↥J) → J.Cotangent) x' = x), x ∈ f.ker
Tactic: rcases Submodule.mem_map.mp hx with ⟨x', hx', eq⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Quotient (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
R' : Type u_3
S' : Type u_4
inst_2 : CommRing R'
inst_3 : CommRing S'
f : R →+* S
flat : f.Flat
qR : R →+* R'
qS : S →+* S'
g : R' →+* S'
surjR : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑qR : (a : R) → R')
surjS : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑qS : (a : S) → S')
comm : qS.comp f = g.comp qR
sq0 : HPow.hPow (α := Ideal R) (β := ℕ) (ker qR) 2 = ⊥
eqmap : Eq (α := Ideal S) (ker qS) (Ideal.map f (ker qR))
smoothq : g.FormallySmooth
⊢ f.FormallySmooth
have algebraizeInst : Module.Flat R S
Tactic: algebraize [f, qR, qS, g, qS.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Quotient (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
R' : Type u_3
S' : Type u_4
inst_2 : CommRing R'
inst_3 : CommRing S'
f : R →+* S
flat : f.Flat
qR : R →+* R'
qS : S →+* S'
g : R' →+* S'
surjR : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑qR : (a : R) → R')
surjS : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑qS : (a : S) → S')
comm : qS.comp f = g.comp qR
sq0 : HPow.hPow (α := Ideal R) (β := ℕ) (ker qR) 2 = ⊥
eqmap : Eq (α := Ideal S) (ker qS) (Ideal.map f (ker qR))
smoothq : g.FormallySmooth
algebraizeInst : Module.Flat R S
⊢ f.FormallySmooth
have algebraizeInst₁ : Algebra.FormallySmooth R' S'
Tactic: algebraize [f, qR, qS, g, qS.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmooth (goal)
Goal:
n : ℕ
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 : Finite ι
P : SubmersivePresentation R S ι σ
hP : P.dimension = n
⊢ IsStandardSmoothOfRelativeDimension n R S
have refine : Presentation.dimension (ι := Fin (Fintype.card ι)) (σ := Fin (Fintype.card σ))
    (PreSubmersivePresentation.toPresentation
      (toPreSubmersivePresentation (P.reindex (Equiv.symm (Fintype.equivFin ι)) (Equiv.symm (Fintype.equivFin σ))))) =
  n
Tactic: refine ⟨⟨_, _, _, inferInstance,
    P.reindex (Fintype.equivFin _).symm (Fintype.equivFin σ).symm, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmooth (goal)
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 : IsStandardSmooth R S
⊢ FinitePresentation R S
have obtain : ∀ (w w_1 : Type) (w_2 : Finite w_1), Finite w → ∀ (P : SubmersivePresentation R S w w_1), FinitePresentation R S
Tactic: obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmooth (goal)
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
e : S ≃ₐ[R] T
inst_5 : IsStandardSmooth R S
⊢ IsStandardSmooth R T
have obtain : ∀ (w w_1 : Type) (w_2 : Finite w_1), Finite w → ∀ (P : SubmersivePresentation R S w w_1), IsStandardSmooth R T
Tactic: obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmooth (goal)
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
⊢ IsStandardSmoothOfRelativeDimension n R T
have obtain : ∀ (w w_1 : Type) (w_2 : Finite w_1),
  Finite w → ∀ (P : SubmersivePresentation R S w w_1) (hP : P.dimension = n), IsStandardSmoothOfRelativeDimension n R T
Tactic: obtain ⟨_, _, _, _, ⟨P, hP⟩⟩ := ‹IsStandardSmoothOfRelativeDimension n R S›
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmooth (goal)
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
⊢ ∃ (ι : Type) (σ : Type) (x : Finite σ), Finite ι ∧ Nonempty (SubmersivePresentation R T ι σ)
have 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 ι σ)
Tactic: obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmooth (goal)
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
⊢ ∃ (ι : Type) (σ : Type) (x : Finite σ), Finite ι ∧ Nonempty (SubmersivePresentation R T ι σ)
have 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 ι σ)
Tactic: obtain ⟨_, _, _, _, ⟨Q⟩⟩ := ‹IsStandardSmooth S T›
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmooth (goal)
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
⊢ ∃ (ι : Type) (σ : Type) (x : Finite σ) (_ : Finite ι) (P : SubmersivePresentation R T ι σ), P.dimension = m + n
have 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
Tactic: obtain ⟨_, _, _, _, P, hP⟩ := ‹IsStandardSmoothOfRelativeDimension n R S›
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmooth (goal)
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
⊢ ∃ (ι : Type) (σ : Type) (x : Finite σ) (_ : Finite ι) (P : SubmersivePresentation R T ι σ), P.dimension = m + n
have 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
Tactic: obtain ⟨_, _, _, _, Q, hQ⟩ := ‹IsStandardSmoothOfRelativeDimension m S T›
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmooth (goal)
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
⊢ ∃ (ι : Type) (σ : Type) (x : Finite σ), Finite ι ∧ Nonempty (SubmersivePresentation T (T ⊗[R] S) ι σ)
have obtain : ∀ (ι σ : Type) (w : Finite σ),
  Finite ι →
    ∀ (P : SubmersivePresentation R S ι σ),
      ∃ (ι : Type) (σ : Type) (x : Finite σ), Finite ι ∧ Nonempty (SubmersivePresentation T (T ⊗[R] S) ι σ)
Tactic: obtain ⟨ι, σ, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmooth (goal)
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
⊢ ∃ (ι : Type) (σ : Type) (x : Finite σ) (_ : Finite ι) (P : SubmersivePresentation T (T ⊗[R] S) ι σ), P.dimension = n
have 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
Tactic: obtain ⟨_, _, _, _, P, hP⟩ := ‹IsStandardSmoothOfRelativeDimension n R S›
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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)
    ((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)
have dsimp : Eq.{u_2 + 1} (α := S)
  ((Finsupp.linearEquivFunOnFinite S S σ : (a : σ →₀ S) → σ → S)
      ((Finsupp.lcomapDomain P.map sorry : (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: dsimp only [cotangentComplexAux, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    cotangentComplex_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
⊢ 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)
have 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)
Tactic: rw [funext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
⊢ (∀ (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)
have 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)
Tactic: simp_rw [cotangentComplexAux_apply, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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 ι σ
⊢ Function.Injective (α := P.toExtension.Cotangent) (β := σ → S)
    (⇑P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S)
have rw : P.cotangentComplexAux.ker ≤ ⊥
Tactic: rw [← LinearMap.ker_eq_bot, eq_bot_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
⊢ Membership.mem (γ := Submodule S P.toExtension.Cotangent) ⊥ x
have 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)
Tactic: obtain ⟨(x : P.ker), rfl⟩ := Cotangent.mk_surjective x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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)
⊢ Membership.mem (α := P.toExtension.Cotangent) (γ := Submodule S P.toExtension.Cotangent) ⊥
    ((Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x : P.toExtension.Cotangent)
have rw : (↑x : P.toExtension.Ring) ∈ HPow.hPow (β := ℕ) P.toExtension.ker 2
Tactic: rw [Submodule.mem_bot, Cotangent.mk_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (hypothesis)
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)
⊢ (↑x : P.toExtension.Ring) ∈ HPow.hPow (β := ℕ) P.toExtension.ker 2
have 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)
Tactic: rw [LinearMap.mem_ker, P.cotangentComplexAux_zero_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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)
have rw : (↑x : P.Ring) ∈ P.ker
Tactic: rw [P.span_range_relation_eq_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (hypothesis)
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.toExtension.Ring) ∈ HPow.hPow (β := ℕ) P.toExtension.ker 2
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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)
⊢ (↑x : P.toExtension.Ring) ∈ HPow.hPow (β := ℕ) P.toExtension.ker 2
have 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
Tactic: obtain ⟨c, hc⟩ := Finsupp.mem_ideal_span_range_iff_exists_finsupp.mp this
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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)
c : σ →₀ P.Ring
hc : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) = (↑x : P.Ring)
i : σ
⊢ Eq.{u_2 + 1} (α := S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R)
          (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i)) :
      S)
    (0 : S)
have rw : 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 [hc]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (hypothesis)
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)
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
have heq : ∀ (i : σ),
  Eq.{u_2 + 1} (α := S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R)
          (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i)) :
      S)
    (0 : S)
Tactic: have heq (i : σ) :
      aeval P.val (pderiv (P.map i) <| c.sum fun i a ↦ a * P.relation i) = 0 := by
    rw [hc]
    apply hx
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (hypothesis)
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)
c : σ →₀ P.Ring
hc : (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i) = (↑x : P.Ring)
heq :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := S)
      ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R)
            (c.sum fun (i : σ) (a : P.Ring) ↦ a * P.relation i)) :
        S)
      (0 : S)
⊢ (↑x : P.toExtension.Ring) ∈ HPow.hPow (β := ℕ) P.toExtension.ker 2
have heq₁ : ∀ (i : σ),
  Eq.{u_2 + 1} (α := S)
    (∑ x ∈ c.support,
      HMul.hMul (α := S) (β := S) ((aeval P.val : (a : MvPolynomial ι R) → S) ((c : (a : σ) → P.Ring) x : P.Ring) : S)
        ((aeval P.val : (a : MvPolynomial ι R) → S)
            ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation x) : MvPolynomial ι R) :
          S))
    0
Tactic: simp only [Finsupp.sum, map_sum, Derivation.leibniz, smul_eq_mul, map_add, map_mul,
    Presentation.aeval_val_relation, zero_mul, add_zero] at heq
Cleared hypotheses: heq