awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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')
⊢ ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
have this₁ : 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'
-- 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_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)
have inr : g * (IsLocalization.Away.sec g g').1 ∉ p
Tactic: refine ⟨g * (IsLocalization.Away.sec g g').1, ?_, .of_algEquiv (e.restrictScalars R).symm⟩
-- 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_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')
⊢ g * (IsLocalization.Away.sec g g').1 ∉ p
have inr : ∀ (hmem : (IsLocalization.Away.sec g g').1 ∈ p),
  Membership.mem (γ := Ideal (Localization.Away g))
    (Ideal.map (F := S →+* Localization.Away g) (algebraMap S (Localization.Away g)) p) g'
Tactic: refine Ideal.IsPrime.mul_notMem ‹_› hg fun hmem ↦ hg' ?_
-- 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_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')
hmem : (IsLocalization.Away.sec g g').1 ∈ p
⊢ Membership.mem (γ := Ideal (Localization.Away g))
    (Ideal.map (F := S →+* Localization.Away g) (algebraMap S (Localization.Away g)) p) g'
have inr : Membership.mem (α := Localization.Away g) (γ := Ideal (Localization.Away g))
  (Ideal.map (F := S →+* Localization.Away g) (algebraMap S (Localization.Away g)) p)
  ((algebraMap S (Localization.Away g) : (a : S) → Localization.Away g) (IsLocalization.Away.sec g g').1 :
    Localization.Away g)
Tactic: rw [Ideal.mem_iff_of_associated (IsLocalization.Away.associated_sec_fst g g').symm]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_1
S : Type u_2
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
inst_6 : FinitePresentation R S
p : Ideal S
inst_7 : p.IsPrime
inst_8 : IsSmoothAt R p
h : Smooth R S
⊢ ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
have obtain : ∀ (κ : Type u_2) (a : κ → S) (b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R])
  (hb :
    ∀ (i : κ),
      Eq (α := Ω[Localization.AtPrime p⁄R])
        ((b : (a : κ) → Ω[Localization.AtPrime p⁄R]) i : Ω[Localization.AtPrime p⁄R])
        (Function.comp (β := Ω[S⁄R])
            (⇑(map R R S (Localization.AtPrime p)) : (a : Ω[S⁄R]) → Ω[Localization.AtPrime p⁄R])
            (⇑(D R S) : (a : S) → Ω[S⁄R]) (a i) :
          Ω[Localization.AtPrime p⁄R])),
  ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
Tactic: obtain ⟨κ, a, b, hb⟩ := Module.exists_basis_of_span_of_flat _
    (span_range_map_derivation_of_isLocalization R _ (Localization.AtPrime p) p.primeCompl)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_1
S : Type u_2
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
inst_6 : FinitePresentation R S
p : Ideal S
inst_7 : p.IsPrime
inst_8 : IsSmoothAt R p
h : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb :
  ∀ (i : κ),
    Eq (α := Ω[Localization.AtPrime p⁄R]) ((b : (a : κ) → Ω[Localization.AtPrime p⁄R]) i : Ω[Localization.AtPrime p⁄R])
      (Function.comp (β := Ω[S⁄R]) (⇑(map R R S (Localization.AtPrime p)) : (a : Ω[S⁄R]) → Ω[Localization.AtPrime p⁄R])
          (⇑(D R S) : (a : S) → Ω[S⁄R]) (a i) :
        Ω[Localization.AtPrime p⁄R])
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : LinearMap (R := Localization.AtPrime p) (RingHom.id (Localization.AtPrime p)) (κ →₀ Localization.AtPrime p)
  Ω[Localization.AtPrime p⁄R] :=
  ((IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p) :
        ((κ →₀ S) →ₗ[S] Ω[S⁄R]) →ₗ[S]
          LinearMap (R := Localization.AtPrime p) (RingHom.id (Localization.AtPrime p)) (κ →₀ Localization.AtPrime p)
            Ω[Localization.AtPrime p⁄R]) :
      (a : (κ →₀ S) →ₗ[S] Ω[S⁄R]) →
        (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R])
    e
⊢ eₚ = (↑b.repr.symm : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R])
have h₁ : ∀ (i : κ),
  Eq (α := Ω[Localization.AtPrime p⁄R])
    ((eₚ ∘ₗ Finsupp.lsingle i : (a : Localization.AtPrime p) → Ω[Localization.AtPrime p⁄R]) 1)
    (((↑b.repr.symm : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R]) ∘ₗ
          Finsupp.lsingle i :
        (a : Localization.AtPrime p) → Ω[Localization.AtPrime p⁄R])
      1)
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_1
S : Type u_2
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
inst_6 : FinitePresentation R S
p : Ideal S
inst_7 : p.IsPrime
inst_8 : IsSmoothAt R p
h : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb :
  ∀ (i : κ),
    Eq (α := Ω[Localization.AtPrime p⁄R]) ((b : (a : κ) → Ω[Localization.AtPrime p⁄R]) i : Ω[Localization.AtPrime p⁄R])
      (Function.comp (β := Ω[S⁄R]) (⇑(map R R S (Localization.AtPrime p)) : (a : Ω[S⁄R]) → Ω[Localization.AtPrime p⁄R])
          (⇑(D R S) : (a : S) → Ω[S⁄R]) (a i) :
        Ω[Localization.AtPrime p⁄R])
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : LinearMap (R := Localization.AtPrime p) (RingHom.id (Localization.AtPrime p)) (κ →₀ Localization.AtPrime p)
  Ω[Localization.AtPrime p⁄R] :=
  ((IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p) :
        ((κ →₀ S) →ₗ[S] Ω[S⁄R]) →ₗ[S]
          LinearMap (R := Localization.AtPrime p) (RingHom.id (Localization.AtPrime p)) (κ →₀ Localization.AtPrime p)
            Ω[Localization.AtPrime p⁄R]) :
      (a : (κ →₀ S) →ₗ[S] Ω[S⁄R]) →
        (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R])
    e
i : κ
⊢ Eq (α := Ω[Localization.AtPrime p⁄R])
    ((eₚ ∘ₗ Finsupp.lsingle i : (a : Localization.AtPrime p) → Ω[Localization.AtPrime p⁄R]) 1)
    (((↑b.repr.symm : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R]) ∘ₗ
          Finsupp.lsingle i :
        (a : Localization.AtPrime p) → Ω[Localization.AtPrime p⁄R])
      1)
have trans : Eq (α := Ω[Localization.AtPrime p⁄R])
  ((eₚ ∘ₗ Finsupp.lsingle i : (a : Localization.AtPrime p) → Ω[Localization.AtPrime p⁄R]) 1 :
    Ω[Localization.AtPrime p⁄R])
  ((((IsLocalizedModule.map p.primeCompl l₁ l₂ :
              (a : (κ →₀ S) →ₗ[S] Ω[S⁄R]) → (κ →₀ Localization.AtPrime p) →ₗ[S] Ω[Localization.AtPrime p⁄R])
            e :
          (κ →₀ Localization.AtPrime p) →ₗ[S] Ω[Localization.AtPrime p⁄R]) :
        (a : κ →₀ Localization.AtPrime p) → Ω[Localization.AtPrime p⁄R])
      ((l₁ : (a : κ →₀ S) → κ →₀ Localization.AtPrime p) (Finsupp.single i 1)) :
    Ω[Localization.AtPrime p⁄R])
Tactic: trans IsLocalizedModule.map p.primeCompl l₁ l₂ e <| l₁ <| Finsupp.single i 1
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (hypothesis)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_1
S : Type u_2
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
inst_6 : FinitePresentation R S
p : Ideal S
inst_7 : p.IsPrime
inst_8 : IsSmoothAt R p
h : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb :
  ∀ (i : κ),
    Eq (α := Ω[Localization.AtPrime p⁄R]) ((b : (a : κ) → Ω[Localization.AtPrime p⁄R]) i : Ω[Localization.AtPrime p⁄R])
      (Function.comp (β := Ω[S⁄R]) (⇑(map R R S (Localization.AtPrime p)) : (a : Ω[S⁄R]) → Ω[Localization.AtPrime p⁄R])
          (⇑(D R S) : (a : S) → Ω[S⁄R]) (a i) :
        Ω[Localization.AtPrime p⁄R])
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : LinearMap (R := Localization.AtPrime p) (RingHom.id (Localization.AtPrime p)) (κ →₀ Localization.AtPrime p)
  Ω[Localization.AtPrime p⁄R] :=
  ((IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p) :
        ((κ →₀ S) →ₗ[S] Ω[S⁄R]) →ₗ[S]
          LinearMap (R := Localization.AtPrime p) (RingHom.id (Localization.AtPrime p)) (κ →₀ Localization.AtPrime p)
            Ω[Localization.AtPrime p⁄R]) :
      (a : (κ →₀ S) →ₗ[S] Ω[S⁄R]) →
        (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R])
    e
⊢ ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
have this : eₚ = (↑b.repr.symm : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R])
Tactic: have : eₚ = b.repr.symm := by
    ext i
    trans IsLocalizedModule.map p.primeCompl l₁ l₂ e <| l₁ <| Finsupp.single i 1
    · simp [eₚ, -IsLocalizedModule.map_apply, l₁]
    · simp [l₂, e, hb]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (hypothesis)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_1
S : Type u_2
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
inst_6 : FinitePresentation R S
p : Ideal S
inst_7 : p.IsPrime
inst_8 : IsSmoothAt R p
h : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb :
  ∀ (i : κ),
    Eq (α := Ω[Localization.AtPrime p⁄R]) ((b : (a : κ) → Ω[Localization.AtPrime p⁄R]) i : Ω[Localization.AtPrime p⁄R])
      (Function.comp (β := Ω[S⁄R]) (⇑(map R R S (Localization.AtPrime p)) : (a : Ω[S⁄R]) → Ω[Localization.AtPrime p⁄R])
          (⇑(D R S) : (a : S) → Ω[S⁄R]) (a i) :
        Ω[Localization.AtPrime p⁄R])
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : LinearMap (R := Localization.AtPrime p) (RingHom.id (Localization.AtPrime p)) (κ →₀ Localization.AtPrime p)
  Ω[Localization.AtPrime p⁄R] :=
  ((IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p) :
        ((κ →₀ S) →ₗ[S] Ω[S⁄R]) →ₗ[S]
          LinearMap (R := Localization.AtPrime p) (RingHom.id (Localization.AtPrime p)) (κ →₀ Localization.AtPrime p)
            Ω[Localization.AtPrime p⁄R]) :
      (a : (κ →₀ S) →ₗ[S] Ω[S⁄R]) →
        (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R])
    e
this : eₚ = (↑b.repr.symm : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R])
⊢ ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
have heₚ : Function.Bijective (α := κ →₀ Localization.AtPrime p) (β := Ω[Localization.AtPrime p⁄R])
  (⇑eₚ : (a : κ →₀ Localization.AtPrime p) → Ω[Localization.AtPrime p⁄R])
Tactic: have heₚ : Function.Bijective eₚ := this ▸ b.repr.symm.bijective
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (hypothesis)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_1
S : Type u_2
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
inst_6 : FinitePresentation R S
p : Ideal S
inst_7 : p.IsPrime
inst_8 : IsSmoothAt R p
h : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb :
  ∀ (i : κ),
    Eq (α := Ω[Localization.AtPrime p⁄R]) ((b : (a : κ) → Ω[Localization.AtPrime p⁄R]) i : Ω[Localization.AtPrime p⁄R])
      (Function.comp (β := Ω[S⁄R]) (⇑(map R R S (Localization.AtPrime p)) : (a : Ω[S⁄R]) → Ω[Localization.AtPrime p⁄R])
          (⇑(D R S) : (a : S) → Ω[S⁄R]) (a i) :
        Ω[Localization.AtPrime p⁄R])
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : LinearMap (R := Localization.AtPrime p) (RingHom.id (Localization.AtPrime p)) (κ →₀ Localization.AtPrime p)
  Ω[Localization.AtPrime p⁄R] :=
  ((IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p) :
        ((κ →₀ S) →ₗ[S] Ω[S⁄R]) →ₗ[S]
          LinearMap (R := Localization.AtPrime p) (RingHom.id (Localization.AtPrime p)) (κ →₀ Localization.AtPrime p)
            Ω[Localization.AtPrime p⁄R]) :
      (a : (κ →₀ S) →ₗ[S] Ω[S⁄R]) →
        (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R])
    e
this : eₚ = (↑b.repr.symm : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R])
heₚ :
  Function.Bijective (α := κ →₀ Localization.AtPrime p) (β := Ω[Localization.AtPrime p⁄R])
    (⇑eₚ : (a : κ →₀ Localization.AtPrime p) → Ω[Localization.AtPrime p⁄R])
⊢ ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
have this₁ : Finite κ
Tactic: have : Finite κ := Module.Finite.finite_basis b
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_1
S : Type u_2
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
inst_6 : FinitePresentation R S
p : Ideal S
inst_7 : p.IsPrime
inst_8 : IsSmoothAt R p
h : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb :
  ∀ (i : κ),
    Eq (α := Ω[Localization.AtPrime p⁄R]) ((b : (a : κ) → Ω[Localization.AtPrime p⁄R]) i : Ω[Localization.AtPrime p⁄R])
      (Function.comp (β := Ω[S⁄R]) (⇑(map R R S (Localization.AtPrime p)) : (a : Ω[S⁄R]) → Ω[Localization.AtPrime p⁄R])
          (⇑(D R S) : (a : S) → Ω[S⁄R]) (a i) :
        Ω[Localization.AtPrime p⁄R])
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : LinearMap (R := Localization.AtPrime p) (RingHom.id (Localization.AtPrime p)) (κ →₀ Localization.AtPrime p)
  Ω[Localization.AtPrime p⁄R] :=
  ((IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p) :
        ((κ →₀ S) →ₗ[S] Ω[S⁄R]) →ₗ[S]
          LinearMap (R := Localization.AtPrime p) (RingHom.id (Localization.AtPrime p)) (κ →₀ Localization.AtPrime p)
            Ω[Localization.AtPrime p⁄R]) :
      (a : (κ →₀ S) →ₗ[S] Ω[S⁄R]) →
        (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R])
    e
this_1 : eₚ = (↑b.repr.symm : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R])
heₚ :
  Function.Bijective (α := κ →₀ Localization.AtPrime p) (β := Ω[Localization.AtPrime p⁄R])
    (⇑eₚ : (a : κ →₀ Localization.AtPrime p) → Ω[Localization.AtPrime p⁄R])
this : Finite κ
⊢ ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
have obtain : ∀ (g : S) (hg : g ∉ p)
  (h :
    Function.Bijective (α := LocalizedModule (Submonoid.powers g) (κ →₀ S)) (β :=
      LocalizedModule (Submonoid.powers g) Ω[S⁄R])
      (⇑((LocalizedModule.map (Submonoid.powers g) :
                (a : (κ →₀ S) →ₗ[S] Ω[S⁄R]) →
                  LocalizedModule (Submonoid.powers g) (κ →₀ S) →ₗ[Localization (Submonoid.powers g)]
                    LocalizedModule (Submonoid.powers g) Ω[S⁄R])
              e :
            LinearMap (R := Localization (Submonoid.powers g)) (RingHom.id (Localization (Submonoid.powers g)))
              (LocalizedModule (Submonoid.powers g) (κ →₀ S)) (LocalizedModule (Submonoid.powers g) Ω[S⁄R])) :
        (a : LocalizedModule (Submonoid.powers g) (κ →₀ S)) → LocalizedModule (Submonoid.powers g) Ω[S⁄R])),
  ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
Tactic: obtain ⟨g, hg, h⟩ := Module.FinitePresentation.exists_notMem_bijective e p l₁ l₂ heₚ
-- 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 : Smooth R S
⊢ ∃ (s : Set S), Eq (α := Ideal S) (Ideal.span s) ⊤ ∧ ∀ x ∈ s, IsStandardSmooth.{u_1, u_2} R (Localization.Away x)
have choose : ∀ (f : (p : Ideal S) → [inst_4 : p.IsPrime] → [IsSmoothAt R p] → S)
  (hf₁ : ∀ (p : Ideal S) [inst_4 : p.IsPrime] [inst : IsSmoothAt R p], f p ∉ p)
  (hf₂ :
    ∀ (p : Ideal S) [inst_4 : p.IsPrime] [inst_5 : IsSmoothAt R p],
      IsStandardSmooth.{u_1, u_2} R (Localization.Away (f p))),
  ∃ (s : Set S), Eq (α := Ideal S) (Ideal.span s) ⊤ ∧ ∀ x ∈ s, IsStandardSmooth.{u_1, u_2} R (Localization.Away x)
Tactic: choose f hf₁ hf₂ using IsSmoothAt.exists_notMem_isStandardSmooth 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
inst_3 : Smooth R S
f : (p : Ideal S) → [inst_4 : p.IsPrime] → [IsSmoothAt R p] → S
hf₁ : ∀ (p : Ideal S) [inst_4 : p.IsPrime] [inst : IsSmoothAt R p], f p ∉ p
hf₂ :
  ∀ (p : Ideal S) [inst_4 : p.IsPrime] [inst_5 : IsSmoothAt R p],
    IsStandardSmooth.{u_1, u_2} R (Localization.Away (f p))
⊢ ∀ (x : S),
    Membership.mem (γ := Set S) (Set.range fun (p : PrimeSpectrum S) ↦ f p.asIdeal) x →
      IsStandardSmooth.{u_1, u_2} R (Localization.Away x)
have simp : ∀ (a : PrimeSpectrum S), IsStandardSmooth.{u_1, u_2} R (Localization.Away (f a.asIdeal))
Tactic: simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_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 : Smooth R S
f : (p : Ideal S) → [inst_4 : p.IsPrime] → [IsSmoothAt R p] → S
hf₁ : ∀ (p : Ideal S) [inst_4 : p.IsPrime] [inst : IsSmoothAt R p], f p ∉ p
hf₂ :
  ∀ (p : Ideal S) [inst_4 : p.IsPrime] [inst_5 : IsSmoothAt R p],
    IsStandardSmooth.{u_1, u_2} R (Localization.Away (f p))
⊢ ∃ (s : Set S), Eq (α := Ideal S) (Ideal.span s) ⊤ ∧ ∀ x ∈ s, IsStandardSmooth.{u_1, u_2} R (Localization.Away x)
have refine : Eq.{u_2 + 1} (α := Ideal S) (Ideal.span (Set.range fun (p : PrimeSpectrum S) ↦ f p.asIdeal)) ⊤
Tactic: refine ⟨Set.range (fun p : PrimeSpectrum S ↦ f p.asIdeal), ?_, by
    simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]; intro; apply hf₂⟩