awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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)

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]
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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)
hbij :
  Function.Bijective (α := P'.toExtension.Cotangent) (β := Unit ⊕ Fin n →₀ S)
    (⇑(P'.cotangentRestrict ⋯) : (a : P'.toExtension.Cotangent) → Unit ⊕ Fin n →₀ S)
P'' : SubmersivePresentation.{0, u_3, u_1, u_2} R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n) :=
  { toPreSubmersivePresentation := P', jacobian_isUnit := ⋯ }
⊢ IsStandardSmooth R S

Tactic:
P''.isStandardSmooth

Premises used: Algebra.SubmersivePresentation.isStandardSmooth
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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)
hbij :
  Function.Bijective (α := P'.toExtension.Cotangent) (β := Unit ⊕ Fin n →₀ S)
    (⇑(P'.cotangentRestrict ⋯) : (a : P'.toExtension.Cotangent) → Unit ⊕ Fin n →₀ S)
P'' : SubmersivePresentation.{0, u_3, u_1, u_2} R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n) :=
  { toPreSubmersivePresentation := P', jacobian_isUnit := ⋯ }
⊢ IsStandardSmooth R S

Tactic:
exact P''.isStandardSmooth

Premises used: Algebra.SubmersivePresentation.isStandardSmooth
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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]))

Tactic:
⟨fun h ↦ ⟨inferInstance, ?_⟩, fun ⟨h, ⟨_, b, hb⟩⟩ ↦ .of_basis_kaehlerDifferential b hb⟩

Premises used: Algebra.IsStandardSmooth, Algebra.IsStandardSmooth.of_basis_kaehlerDifferential, inferInstance, _private.0.Algebra.IsStandardSmooth.iff_exists_basis_kaehlerDifferential.match_1, And.intro, Iff.intro
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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
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]))
⊢ 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]))

Tactic:
refine ⟨fun h ↦ ⟨inferInstance, ?_⟩, fun ⟨h, ⟨_, b, hb⟩⟩ ↦ .of_basis_kaehlerDifferential b hb⟩
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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
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]))
⊢ ∃ (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)

Premises used: Algebra.IsStandardSmooth.out
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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
ι σ : Type
w : Finite σ
left : Finite ι
P : SubmersivePresentation R S ι σ
⊢ Subset (α := Set Ω[S⁄R])
    (Set.range (ι := (↑(Set.range P.map)ᶜ : Type)) (⇑P.basisKaehler : (a : (↑(Set.range P.map)ᶜ : Type)) → Ω[S⁄R]))
    (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))

Tactic:
simp [Set.range_subset_iff]

Premises used: Set.range_subset_iff
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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
ι σ : Type
w : Finite σ
left : 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:
exact ⟨_, P.basisKaehler, by simp [Set.range_subset_iff]⟩
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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

Tactic:
⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
refine : ∀ (h : Etale R S), IsStandardSmoothOfRelativeDimension 0 R S
⊢ Etale R S ↔ IsStandardSmoothOfRelativeDimension 0 R S

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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
⊢ Nontrivial S

Tactic:
nontriviality S
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h_1 : Etale R S
h_2 : Nontrivial S
h : IsStandardSmooth R S
⊢ IsStandardSmoothOfRelativeDimension 0 R S

Tactic:
simp [IsStandardSmoothOfRelativeDimension.iff_of_isStandardSmooth]

Premises used: Algebra.IsStandardSmoothOfRelativeDimension.iff_of_isStandardSmooth
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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
suffices : IsStandardSmooth R S
⊢ IsStandardSmoothOfRelativeDimension 0 R S

Tactic:
suffices h : IsStandardSmooth R S by
    simp [IsStandardSmoothOfRelativeDimension.iff_of_isStandardSmooth]
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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
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]))
⊢ IsStandardSmooth R S

Tactic:
rw [IsStandardSmooth.iff_exists_basis_kaehlerDifferential]

Premises used: Algebra.IsStandardSmooth.iff_exists_basis_kaehlerDifferential
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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]))

Tactic:
⟨inferInstance, ⟨Empty, Module.Basis.empty Ω[S⁄R], ?_⟩⟩

Premises used: inferInstance, Empty, And.intro, Exists.intro, Module.Basis.empty, KaehlerDifferential
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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
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]))
⊢ 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:
refine ⟨inferInstance, ⟨Empty, Module.Basis.empty Ω[S⁄R], ?_⟩⟩
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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
⊢ 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:
simp [Set.range_subset_iff]

Premises used: Set.range_subset_iff
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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)
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)
⊢ ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)

Tactic:
wlog h : Smooth R S

Premises used: Algebra.Smooth
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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
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)
⊢ ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)

Tactic:
obtain ⟨g, hg, hsm⟩ := IsSmoothAt.exists_notMem_smooth R p

Premises used: Algebra.IsSmoothAt.exists_notMem_smooth
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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)
apply : Disjoint (↑(Submonoid.powers g) : Set S) (↑p : Set S)
⊢ Ideal.IsPrime (α := Localization.Away g)
    (Ideal.map (F := S →+* Localization.Away g) (algebraMap S (Localization.Away g)) p)

Tactic:
apply IsLocalization.isPrime_of_isPrime_disjoint (.powers g) _ _ ‹_›

Premises used: IsLocalization.isPrime_of_isPrime_disjoint, Submonoid.powers
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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)
rwa rwa₁ rwa₂ rwa₃ : g ∉ p
⊢ Disjoint (↑(Submonoid.powers g) : Set S) (↑p : Set S)

Tactic:
rwa [Ideal.disjoint_powers_iff_notMem_of_isPrime]

Premises used: Ideal.disjoint_powers_iff_notMem_of_isPrime
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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)

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]
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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)
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)
⊢ ∃ 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

Premises used: Algebra.algebraMap, Localization.Away, Ideal.map
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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)
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')
⊢ IsLocalization.Away (g * (IsLocalization.Away.sec g g').1) (Localization.Away g')

Tactic:
have : IsLocalization.Away (g * (IsLocalization.Away.sec g g').1) (Localization.Away g') :=
      .mul_of_associated _ _ g' <| IsLocalization.Away.associated_sec_fst g g'
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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_1 :
  ∀ (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)
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')
this : IsLocalization.Away (g * (IsLocalization.Away.sec g g').1) (Localization.Away g')
e : Localization.Away (g * (IsLocalization.Away.sec g g').1) ≃ₐ[S] Localization.Away g' :=
  Localization.algEquiv (Submonoid.powers (g * (IsLocalization.Away.sec g g').1)) (Localization.Away g')
⊢ ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)

Tactic:
⟨g * (IsLocalization.Away.sec g g').1, ?_, .of_algEquiv (e.restrictScalars R).symm⟩

Premises used: HMul.hMul, AlgEquiv.symm, Algebra.IsStandardSmooth.of_algEquiv, IsLocalization.Away.sec, Prod.fst, AlgEquiv.restrictScalars, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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_1 :
  ∀ (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)
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')
this : IsLocalization.Away (g * (IsLocalization.Away.sec g g').1) (Localization.Away g')
e : Localization.Away (g * (IsLocalization.Away.sec g g').1) ≃ₐ[S] Localization.Away g' :=
  Localization.algEquiv (Submonoid.powers (g * (IsLocalization.Away.sec g g').1)) (Localization.Away g')
inr : g * (IsLocalization.Away.sec g g').1 ∉ p
⊢ ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)

Tactic:
refine ⟨g * (IsLocalization.Away.sec g g').1, ?_, .of_algEquiv (e.restrictScalars R).symm⟩