awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : IsStandardSmooth R S
⊢ FormallySmooth R S
have rw : Module.Projective S Ω[S⁄R] ∧ Subsingleton (H1Cotangent R S)
Tactic: rw [Algebra.formallySmooth_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
hb :
  Subset (α := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R]))
    (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))
⊢ IsStandardSmooth R S
have a : Nontrivial S
Tactic: nontriviality S
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
hb :
  Subset (α := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R]))
    (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))
h : Nontrivial S
⊢ IsStandardSmooth R S
have obtain : ∀ (n : ℕ) (P : Generators R S (Fin n)), IsStandardSmooth R S
Tactic: obtain ⟨n, ⟨P⟩⟩ := (FiniteType.iff_exists_generators (R := R) (S := S)).mp inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
hb :
  Subset (α := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R]))
    (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))
h : Nontrivial S
n : ℕ
P : Generators R S (Fin n)
⊢ IsStandardSmooth R S
have choose : ∀
  (f' :
    ⦃a : Ω[S⁄R]⦄ → Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a → S)
  (hf' :
    ∀ ⦃a : Ω[S⁄R]⦄
      (a_1 : Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a),
      (D R S : (a : S) → Ω[S⁄R]) (f' a_1) = a),
  IsStandardSmooth R S
Tactic: choose f' hf' using hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
h : Nontrivial S
n : ℕ
P_1 : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a → S
hf' :
  ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a),
    (D R S : (a : S) → Ω[S⁄R]) (f' a_1) = a
P : Generators.{u_3, u_1, u_2} R S (Fin n ⊕ I) := P_1.extend fun (i : I) ↦ f' ⋯
⊢ IsStandardSmooth R S
have hb : ∀ (i : I),
  Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : I) → Ω[S⁄R]) i : Ω[S⁄R])
    ((D R S : (a : S) → Ω[S⁄R]) (P.val (Sum.inr i)) : Ω[S⁄R])
Tactic: have hb (i : I) : b i = D R S (P.val (Sum.inr i)) := by simp [P, hf']
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
h : Nontrivial S
n : ℕ
P_1 : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a → S
hf' :
  ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a),
    (D R S : (a : S) → Ω[S⁄R]) (f' a_1) = a
P : Generators.{u_3, u_1, u_2} R S (Fin n ⊕ I) := P_1.extend fun (i : I) ↦ f' ⋯
hb :
  ∀ (i : I),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : I) → Ω[S⁄R]) i : Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) (P.val (Sum.inr i)) : Ω[S⁄R])
⊢ IsStandardSmooth R S
have this : Function.Bijective (α := P.toExtension.Cotangent) (β := Fin n →₀ S)
  (⇑(P.cotangentRestrict sorry) : (a : P.toExtension.Cotangent) → Fin n →₀ S)
Tactic: have : Function.Bijective (P.cotangentRestrict _) :=
    P.cotangentRestrict_bijective_of_basis_kaehlerDifferential Sum.inl_injective
      Set.isCompl_range_inl_range_inr.symm b hb
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
h : Nontrivial S
n : ℕ
P_1 : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a → S
hf' :
  ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a),
    (D R S : (a : S) → Ω[S⁄R]) (f' a_1) = a
P : Generators.{u_3, u_1, u_2} R S (Fin n ⊕ I) := P_1.extend fun (i : I) ↦ f' ⋯
hb :
  ∀ (i : I),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : I) → Ω[S⁄R]) i : Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) (P.val (Sum.inr i)) : Ω[S⁄R])
this :
  Function.Bijective (α := P.toExtension.Cotangent) (β := Fin n →₀ S)
    (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → Fin n →₀ S)
bcot' : Module.Basis (Fin n) S P.toExtension.Cotangent :=
  { repr := LinearEquiv.ofBijective (P.cotangentRestrict ⋯) this }
⊢ IsStandardSmooth R S
have this₁ : Finite I
Tactic: have : Finite I := Module.Finite.finite_basis b
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
h : Nontrivial S
n : ℕ
P_1 : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a → S
hf' :
  ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a),
    (D R S : (a : S) → Ω[S⁄R]) (f' a_1) = a
P : Generators.{u_3, u_1, u_2} R S (Fin n ⊕ I) := P_1.extend fun (i : I) ↦ f' ⋯
hb :
  ∀ (i : I),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : I) → Ω[S⁄R]) i : Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) (P.val (Sum.inr i)) : Ω[S⁄R])
this_1 :
  Function.Bijective (α := P.toExtension.Cotangent) (β := Fin n →₀ S)
    (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → Fin n →₀ S)
bcot' : Module.Basis (Fin n) S P.toExtension.Cotangent :=
  { repr := LinearEquiv.ofBijective (P.cotangentRestrict ⋯) this_1 }
this : Finite I
⊢ IsStandardSmooth R S
have obtain : ∀ (Q : Presentation.{0, u_3, u_1, u_2} R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n))
  (bcot : Module.Basis (Unit ⊕ Fin n) S Q.toExtension.Cotangent) (hcomp : Q.val ∘ Sum.inr = P.val)
  (hbcot :
    ∀ (r : Unit ⊕ Fin n),
      Eq (α := Q.toExtension.Cotangent)
        ((bcot : (a : Unit ⊕ Fin n) → Q.toExtension.Cotangent) r : Q.toExtension.Cotangent)
        ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
            (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker) (Q.relation r) sorry) :
          Q.toExtension.Cotangent)),
  IsStandardSmooth R S
Tactic: obtain ⟨Q, bcot, hcomp, hbcot⟩ := P.exists_presentation_of_basis_cotangent bcot'
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
h : Nontrivial S
n : ℕ
P_1 : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a → S
hf' :
  ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a),
    (D R S : (a : S) → Ω[S⁄R]) (f' a_1) = a
P : Generators.{u_3, u_1, u_2} R S (Fin n ⊕ I) := P_1.extend fun (i : I) ↦ f' ⋯
hb :
  ∀ (i : I),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : I) → Ω[S⁄R]) i : Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) (P.val (Sum.inr i)) : Ω[S⁄R])
this_1 :
  Function.Bijective (α := P.toExtension.Cotangent) (β := Fin n →₀ S)
    (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → Fin n →₀ S)
bcot' : Module.Basis (Fin n) S P.toExtension.Cotangent :=
  { repr := LinearEquiv.ofBijective (P.cotangentRestrict ⋯) this_1 }
this : Finite I
Q : Presentation.{0, u_3, u_1, u_2} R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n)
bcot : Module.Basis (Unit ⊕ Fin n) S Q.toExtension.Cotangent
hcomp : Q.val ∘ Sum.inr = P.val
hbcot :
  ∀ (r : Unit ⊕ Fin n),
    Eq (α := Q.toExtension.Cotangent)
      ((bcot : (a : Unit ⊕ Fin n) → Q.toExtension.Cotangent) r : Q.toExtension.Cotangent)
      ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker) (Q.relation r) ⋯) :
        Q.toExtension.Cotangent)
P' : PreSubmersivePresentation.{0, u_3, u_1, u_2} R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n) :=
  let __spread.0 := Q;
  { toPresentation := __spread.0, map := Sum.map _root_.id Sum.inl, map_inj := ⋯ }
⊢ IsStandardSmooth R S
have hcompl : IsCompl (Set.range (Sum.inr ∘ Sum.inr)) (Set.range P'.map)
Tactic: have hcompl : IsCompl (Set.range (Sum.inr ∘ Sum.inr)) (Set.range P'.map) := by
    simp [P', ← eq_compl_iff_isCompl, Set.ext_iff, Set.mem_compl_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
h : Nontrivial S
n : ℕ
P_1 : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a → S
hf' :
  ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a),
    (D R S : (a : S) → Ω[S⁄R]) (f' a_1) = a
P : Generators.{u_3, u_1, u_2} R S (Fin n ⊕ I) := P_1.extend fun (i : I) ↦ f' ⋯
hb :
  ∀ (i : I),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : I) → Ω[S⁄R]) i : Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) (P.val (Sum.inr i)) : Ω[S⁄R])
this_1 :
  Function.Bijective (α := P.toExtension.Cotangent) (β := Fin n →₀ S)
    (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → Fin n →₀ S)
bcot' : Module.Basis (Fin n) S P.toExtension.Cotangent :=
  { repr := LinearEquiv.ofBijective (P.cotangentRestrict ⋯) this_1 }
this : Finite I
Q : Presentation.{0, u_3, u_1, u_2} R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n)
bcot : Module.Basis (Unit ⊕ Fin n) S Q.toExtension.Cotangent
hcomp : Q.val ∘ Sum.inr = P.val
hbcot :
  ∀ (r : Unit ⊕ Fin n),
    Eq (α := Q.toExtension.Cotangent)
      ((bcot : (a : Unit ⊕ Fin n) → Q.toExtension.Cotangent) r : Q.toExtension.Cotangent)
      ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker) (Q.relation r) ⋯) :
        Q.toExtension.Cotangent)
P' : PreSubmersivePresentation.{0, u_3, u_1, u_2} R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n) :=
  let __spread.0 := Q;
  { toPresentation := __spread.0, map := Sum.map _root_.id Sum.inl, map_inj := ⋯ }
hcompl : IsCompl (Set.range (Sum.inr ∘ Sum.inr)) (Set.range P'.map)
⊢ Function.Bijective (α := P'.toExtension.Cotangent) (β := Unit ⊕ Fin n →₀ S)
    (⇑(P'.cotangentRestrict ⋯) : (a : P'.toExtension.Cotangent) → Unit ⊕ Fin n →₀ S)
have hb₁ : ∀ (k : I),
  Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : I) → Ω[S⁄R]) k : Ω[S⁄R])
    ((D R S : (a : S) → Ω[S⁄R]) (P'.val ((Sum.inr ∘ Sum.inr) k)) : Ω[S⁄R])
Tactic: apply P'.cotangentRestrict_bijective_of_basis_kaehlerDifferential P'.map_inj hcompl b
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
h : Nontrivial S
n : ℕ
P_1 : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a → S
hf' :
  ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a),
    (D R S : (a : S) → Ω[S⁄R]) (f' a_1) = a
P : Generators.{u_3, u_1, u_2} R S (Fin n ⊕ I) := P_1.extend fun (i : I) ↦ f' ⋯
hb :
  ∀ (i : I),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : I) → Ω[S⁄R]) i : Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) (P.val (Sum.inr i)) : Ω[S⁄R])
this_1 :
  Function.Bijective (α := P.toExtension.Cotangent) (β := Fin n →₀ S)
    (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → Fin n →₀ S)
bcot' : Module.Basis (Fin n) S P.toExtension.Cotangent :=
  { repr := LinearEquiv.ofBijective (P.cotangentRestrict ⋯) this_1 }
this : Finite I
Q : Presentation.{0, u_3, u_1, u_2} R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n)
bcot : Module.Basis (Unit ⊕ Fin n) S Q.toExtension.Cotangent
hcomp : Q.val ∘ Sum.inr = P.val
hbcot :
  ∀ (r : Unit ⊕ Fin n),
    Eq (α := Q.toExtension.Cotangent)
      ((bcot : (a : Unit ⊕ Fin n) → Q.toExtension.Cotangent) r : Q.toExtension.Cotangent)
      ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker) (Q.relation r) ⋯) :
        Q.toExtension.Cotangent)
P' : PreSubmersivePresentation.{0, u_3, u_1, u_2} R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n) :=
  let __spread.0 := Q;
  { toPresentation := __spread.0, map := Sum.map _root_.id Sum.inl, map_inj := ⋯ }
hcompl : IsCompl (Set.range (Sum.inr ∘ Sum.inr)) (Set.range P'.map)
⊢ IsStandardSmooth R S
have hbij : Function.Bijective (α := P'.toExtension.Cotangent) (β := Unit ⊕ Fin n →₀ S)
  (⇑(P'.cotangentRestrict sorry) : (a : P'.toExtension.Cotangent) → Unit ⊕ Fin n →₀ S)
Tactic: have hbij : Function.Bijective (P'.cotangentRestrict P'.map_inj) := by
    apply P'.cotangentRestrict_bijective_of_basis_kaehlerDifferential P'.map_inj hcompl b
    intro k
    simp only [hb, ← hcomp, P', Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
⊢ IsStandardSmooth R S ↔
    Subsingleton (H1Cotangent R S) ∧
      ∃ (I : Type) (b : Module.Basis I S Ω[S⁄R]),
        Subset (α := Set Ω[S⁄R]) (Set.range (ι := I) (⇑b : (a : I) → Ω[S⁄R]))
          (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))
have refine : ∀ (h : IsStandardSmooth R S),
  ∃ (I : Type) (b : Module.Basis I S Ω[S⁄R]),
    Subset (α := Set Ω[S⁄R]) (Set.range (ι := I) (⇑b : (a : I) → Ω[S⁄R]))
      (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))
Tactic: refine ⟨fun h ↦ ⟨inferInstance, ?_⟩, fun ⟨h, ⟨_, b, hb⟩⟩ ↦ .of_basis_kaehlerDifferential b hb⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
h : IsStandardSmooth R S
⊢ ∃ (I : Type) (b : Module.Basis I S Ω[S⁄R]),
    Subset (α := Set Ω[S⁄R]) (Set.range (ι := I) (⇑b : (a : I) → Ω[S⁄R]))
      (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))
have obtain : ∀ (ι σ : Type) (w : Finite σ),
  Finite ι →
    ∀ (P : SubmersivePresentation R S ι σ),
      ∃ (I : Type) (b : Module.Basis I S Ω[S⁄R]),
        Subset (α := Set Ω[S⁄R]) (Set.range (ι := I) (⇑b : (a : I) → Ω[S⁄R]))
          (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))
Tactic: obtain ⟨ι, σ, _, _, ⟨P⟩⟩ := Algebra.IsStandardSmooth.out (R := R) (S := S)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ Etale R S ↔ IsStandardSmoothOfRelativeDimension 0 R S
have refine : ∀ (h : Etale R S), IsStandardSmoothOfRelativeDimension 0 R S
Tactic: refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : Etale R S
⊢ IsStandardSmoothOfRelativeDimension 0 R S
have a : Nontrivial S
Tactic: nontriviality S
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : Etale R S
h_1 : Nontrivial S
⊢ IsStandardSmoothOfRelativeDimension 0 R S
have suffices : IsStandardSmooth R S
Tactic: suffices h : IsStandardSmooth R S by
    simp [IsStandardSmoothOfRelativeDimension.iff_of_isStandardSmooth]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : Etale R S
h_1 : Nontrivial S
⊢ IsStandardSmooth R S
have rw : Subsingleton (H1Cotangent R S) ∧
  ∃ (I : Type) (b : Module.Basis I S Ω[S⁄R]),
    Subset (α := Set Ω[S⁄R]) (Set.range (ι := I) (⇑b : (a : I) → Ω[S⁄R]))
      (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))
Tactic: rw [IsStandardSmooth.iff_exists_basis_kaehlerDifferential]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : Etale R S
h_1 : Nontrivial S
⊢ Subsingleton (H1Cotangent R S) ∧
    ∃ (I : Type) (b : Module.Basis I S Ω[S⁄R]),
      Subset (α := Set Ω[S⁄R]) (Set.range (ι := I) (⇑b : (a : I) → Ω[S⁄R]))
        (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))
have refine : Subset (α := Set Ω[S⁄R]) (Set.range (ι := Empty) (⇑(Module.Basis.empty Ω[S⁄R]) : (a : Empty) → Ω[S⁄R]))
  (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))
Tactic: refine ⟨inferInstance, ⟨Empty, Module.Basis.empty Ω[S⁄R], ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : IsSmoothAt R p
⊢ ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
have inr : ∀
  (this :
    ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S]
      [FinitePresentation R S] (p : Ideal S) [inst_9 : p.IsPrime] [IsSmoothAt R p] (h : Smooth R S),
      ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f))
  (h : ¬Smooth R S), ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
Tactic: wlog h : Smooth R S
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : IsSmoothAt R p
inr :
  ∀
    (this :
      ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S]
        [FinitePresentation R S] (p : Ideal S) [inst_9 : p.IsPrime] [IsSmoothAt R p] (h : Smooth R S),
        ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f))
    (h : ¬Smooth R S), ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
⊢ ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
have wlog : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S]
  [FinitePresentation R S] (p : Ideal S) [inst_9 : p.IsPrime] [IsSmoothAt R p] (h : Smooth R S),
  ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
Tactic: wlog h : Smooth R S
Cleared hypotheses: inst_3, p, inst_4, inst_5
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : IsSmoothAt R p
this :
  ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S]
    [FinitePresentation R S] (p : Ideal S) [inst_9 : p.IsPrime] [IsSmoothAt R p] (h : Smooth R S),
    ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
h : ¬Smooth R S
⊢ ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
have inr : ∀ (g : S) (hg : g ∉ p) (hsm : Smooth.{u_2, u_1} R (Localization.Away g)),
  ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
Tactic: obtain ⟨g, hg, hsm⟩ := IsSmoothAt.exists_notMem_smooth R p
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : IsSmoothAt R p
this :
  ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S]
    [FinitePresentation R S] (p : Ideal S) [inst_9 : p.IsPrime] [IsSmoothAt R p] (h : Smooth R S),
    ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
h : ¬Smooth R S
g : S
hg : g ∉ p
hsm : Smooth.{u_2, u_1} R (Localization.Away g)
⊢ Ideal.IsPrime (α := Localization.Away g)
    (Ideal.map (F := S →+* Localization.Away g) (algebraMap S (Localization.Away g)) p)
have apply : Disjoint (↑(Submonoid.powers g) : Set S) (↑p : Set S)
Tactic: apply IsLocalization.isPrime_of_isPrime_disjoint (.powers g) _ _ ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : IsSmoothAt R p
this :
  ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S]
    [FinitePresentation R S] (p : Ideal S) [inst_9 : p.IsPrime] [IsSmoothAt R p] (h : Smooth R S),
    ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
h : ¬Smooth R S
g : S
hg : g ∉ p
hsm : Smooth.{u_2, u_1} R (Localization.Away g)
⊢ ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
have x : Ideal.IsPrime (α := Localization.Away g)
  (Ideal.map (F := S →+* Localization.Away g) (algebraMap S (Localization.Away g)) p)
Tactic: have _ : (Ideal.map (algebraMap S (Localization.Away g)) p).IsPrime := by
      apply IsLocalization.isPrime_of_isPrime_disjoint (.powers g) _ _ ‹_›
      rwa [Ideal.disjoint_powers_iff_notMem_of_isPrime]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : IsSmoothAt R p
this :
  ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S]
    [FinitePresentation R S] (p : Ideal S) [inst_9 : p.IsPrime] [IsSmoothAt R p] (h : Smooth R S),
    ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
h : ¬Smooth R S
g : S
hg : g ∉ p
hsm : Smooth.{u_2, u_1} R (Localization.Away g)
h_1 :
  Ideal.IsPrime (α := Localization.Away g)
    (Ideal.map (F := S →+* Localization.Away g) (algebraMap S (Localization.Away g)) p)
⊢ ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
have inr : ∀ (g' : Localization.Away g)
  (hg' : g' ∉ Ideal.map (F := S →+* Localization.Away g) (algebraMap S (Localization.Away g)) p)
  (hstd : IsStandardSmooth.{u_1, u_2} R (Localization.Away g')),
  ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
Tactic: obtain ⟨g', hg', hstd⟩ := this (R := R) (p.map (algebraMap S (Localization.Away g))) hsm