awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Local (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsLocalRing S
inst_3 : Algebra R S
P : Type u_3
K : Type u_4
inst_4 : Field K
inst_5 : CommRing P
inst_6 : Algebra R P
inst_7 : Algebra P S
inst_8 : IsScalarTower R P S
inst_9 : Algebra S K
inst_10 : Algebra P K
inst_11 : IsScalarTower P S K
inst_12 : FormallySmooth R P
inst_13 : Module.Free P Ω[P⁄R]
inst_14 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
h₃ : LE.le (α := Ideal S) (maximalIdeal S) (RingHom.ker (F := S →+* K) (algebraMap S K))
f : ResidueField S →ₐ[S] K := Ideal.Quotient.liftₐ (maximalIdeal S) (ofId S K) h₃
this_1 : Algebra.{u_2, u_4} (ResidueField S) K := f.toAlgebra
this_2 : IsScalarTower S (ResidueField S) K
this : IsScalarTower.{u_3, u_2, u_4} P (ResidueField S) K
⊢ Function.Injective (α :=
      K ⊗[ResidueField S]
        TensorProduct.{u_3, u_2, u_3} P (ResidueField S) ↥(RingHom.ker (F := P →+* S) (algebraMap P S)))
      (β := K ⊗[ResidueField S] TensorProduct.{u_3, u_2, u_3} P (ResidueField S) Ω[P⁄R])
      (⇑(LinearMap.lTensor K (cotangentComplexBaseChange R S P (ResidueField S))) :
        (a : K ⊗[ResidueField S] (ResidueField S ⊗[P] ↥(RingHom.ker (algebraMap P S)))) →
          K ⊗[ResidueField S] (ResidueField S ⊗[P] Ω[P⁄R])) ↔
    Function.Injective (α := K ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) (β := K ⊗[P] Ω[P⁄R])
      (⇑(cotangentComplexBaseChange R S P K) : (a : K ⊗[P] ↥(RingHom.ker (algebraMap P S))) → K ⊗[P] Ω[P⁄R])
have this₁ : Eq (α := K ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) →ₗ[K] K ⊗[P] Ω[P⁄R])
  ((↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K Ω[P⁄R]) :
        K ⊗[ResidueField S] (ResidueField S ⊗[P] Ω[P⁄R]) →ₗ[K] K ⊗[P] Ω[P⁄R]) ∘ₗ
      LinearMap.baseChange K (cotangentComplexBaseChange R S P (ResidueField S)) ∘ₗ
        (↑(LinearEquiv.symm
              (AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K
                ↥(RingHom.ker (F := P →+* S) (algebraMap P S)))) :
          K ⊗[P] ↥(RingHom.ker (algebraMap P S)) →ₗ[K]
            K ⊗[ResidueField S] (ResidueField S ⊗[P] ↥(RingHom.ker (algebraMap P S)))) :
    K ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) →ₗ[K] K ⊗[P] Ω[P⁄R])
  (cotangentComplexBaseChange R S P K : K ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) →ₗ[K] K ⊗[P] Ω[P⁄R])
Tactic: have : (AlgebraTensorModule.cancelBaseChange _ _ _ _ _).toLinearMap ∘ₗ
      (cotangentComplexBaseChange R S P (ResidueField S)).baseChange K ∘ₗ
      (AlgebraTensorModule.cancelBaseChange _ _ _ _ _).symm.toLinearMap =
      (cotangentComplexBaseChange R S P K) := by
    ext; simp [cotangentComplexBaseChange_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
⊢ Eq (α := Set (PrimeSpectrum A)) (smoothLocus R A) ((Module.support A (H1Cotangent R A))ᶜ ∩ Module.freeLocus A Ω[A⁄R])
have h : ∀ (p : PrimeSpectrum A),
  Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) p ↔
    Membership.mem (γ := Set (PrimeSpectrum A)) ((Module.support A (H1Cotangent R A))ᶜ ∩ Module.freeLocus A Ω[A⁄R]) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
p : PrimeSpectrum A
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) p ↔
    Membership.mem (γ := Set (PrimeSpectrum A)) ((Module.support A (H1Cotangent R A))ᶜ ∩ Module.freeLocus A Ω[A⁄R]) p
have h : Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) p ↔
  Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A)) ∧
    Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
Tactic: simp only [Set.mem_inter_iff, Set.mem_compl_iff, Module.notMem_support_iff,
    Module.mem_freeLocus]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
p : PrimeSpectrum A
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) p ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A)) ∧
      Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
have h : Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.AtPrime p.asIdeal)) ∧
    Module.Projective.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
  Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A)) ∧
    Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
Tactic: refine (Algebra.formallySmooth_iff _ _).trans (and_comm.trans ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
p : PrimeSpectrum A
⊢ Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.AtPrime p.asIdeal)) ∧
      Module.Projective.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A)) ∧
      Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
have h : Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.AtPrime p.asIdeal)) ↔
  Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
p : PrimeSpectrum A
h :
  Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.AtPrime p.asIdeal)) ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))
⊢ Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.AtPrime p.asIdeal)) ∧
      Module.Projective.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A)) ∧
      Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
have h₁ : Module.Projective.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
  Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
p : PrimeSpectrum A
⊢ Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.AtPrime p.asIdeal)) ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))
have h : ∀
  (this :
    LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A) ≃ₗ[A]
      H1Cotangent.{u_1, u_2} R (Localization.AtPrime p.asIdeal)),
  Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.AtPrime p.asIdeal)) ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))
Tactic: have := IsLocalizedModule.iso p.asIdeal.primeCompl
      (H1Cotangent.map R R A (Localization.AtPrime p.asIdeal))
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
p : PrimeSpectrum A
⊢ Module.Projective.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
have trans : Module.Projective.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
  Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R]
Tactic: trans Module.Free (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
p : PrimeSpectrum A
trans :
  Module.Projective.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R]
⊢ Module.Projective.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
have trans₁ : Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
  Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
Tactic: trans Module.Free (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
p : PrimeSpectrum A
⊢ Module.Projective.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R]
have this : EssFiniteType A (Localization.AtPrime p.asIdeal)
Tactic: have : EssFiniteType A (Localization.AtPrime p.asIdeal) :=
        .of_isLocalization _ p.asIdeal.primeCompl
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
p : PrimeSpectrum A
this : EssFiniteType A (Localization.AtPrime p.asIdeal)
⊢ Module.Projective.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R]
have this₁ : EssFiniteType.{u_1, u_2} R (Localization.AtPrime p.asIdeal)
Tactic: have : EssFiniteType R (Localization.AtPrime p.asIdeal) := .comp _ A _
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
p : PrimeSpectrum A
⊢ Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
have have : ∀ (this : LocalizedModule p.asIdeal.primeCompl Ω[A⁄R] ≃ₗ[A] Ω[Localization.AtPrime p.asIdeal⁄R]),
  Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
Tactic: have := IsLocalizedModule.iso p.asIdeal.primeCompl
        (KaehlerDifferential.map R R A (Localization.AtPrime p.asIdeal))
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
p : PrimeSpectrum A
this : LocalizedModule p.asIdeal.primeCompl Ω[A⁄R] ≃ₗ[A] Ω[Localization.AtPrime p.asIdeal⁄R]
⊢ Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
have have : ∀
  (this :
    LocalizedModule p.asIdeal.primeCompl Ω[A⁄R] ≃ₗ[Localization.AtPrime p.asIdeal] Ω[Localization.AtPrime p.asIdeal⁄R]),
  Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
Tactic: have := this.extendScalarsOfIsLocalization
        p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
f : A
⊢ (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum A)) ⊆ smoothLocus R A ↔
    FormallySmooth.{u_1, u_2} R (Localization.Away f)
have rw : Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.Away f)) ∧
    Module.Projective.{u_2, u_2} (Localization.Away f) Ω[Localization.Away f⁄R] ↔
  Subsingleton (LocalizedModule.Away f (H1Cotangent R A)) ∧
    Subset (α := Set (PrimeSpectrum A)) (PrimeSpectrum.zeroLocus {f})ᶜ (Module.freeLocus A Ω[A⁄R])
Tactic: rw [smoothLocus_eq_compl_support_inter, Set.subset_inter_iff, Set.subset_compl_comm,
    PrimeSpectrum.basicOpen_eq_zeroLocus_compl, compl_compl,
    ← LocalizedModule.subsingleton_iff_support_subset,
    Algebra.formallySmooth_iff, iff_comm, and_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
f : A
⊢ Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.Away f)) ∧
      Module.Projective.{u_2, u_2} (Localization.Away f) Ω[Localization.Away f⁄R] ↔
    Subsingleton (LocalizedModule.Away f (H1Cotangent R A)) ∧
      Subset (α := Set (PrimeSpectrum A)) (PrimeSpectrum.zeroLocus {f})ᶜ (Module.freeLocus A Ω[A⁄R])
have a : Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.Away f)) ↔ Subsingleton (LocalizedModule.Away f (H1Cotangent R A))
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
f : A
a :
  Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.Away f)) ↔
    Subsingleton (LocalizedModule.Away f (H1Cotangent R A))
⊢ Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.Away f)) ∧
      Module.Projective.{u_2, u_2} (Localization.Away f) Ω[Localization.Away f⁄R] ↔
    Subsingleton (LocalizedModule.Away f (H1Cotangent R A)) ∧
      Subset (α := Set (PrimeSpectrum A)) (PrimeSpectrum.zeroLocus {f})ᶜ (Module.freeLocus A Ω[A⁄R])
have a₁ : Module.Projective.{u_2, u_2} (Localization.Away f) Ω[Localization.Away f⁄R] ↔
  Subset (α := Set (PrimeSpectrum A)) (PrimeSpectrum.zeroLocus {f})ᶜ (Module.freeLocus A Ω[A⁄R])
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
f : A
⊢ Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.Away f)) ↔
    Subsingleton (LocalizedModule.Away f (H1Cotangent R A))
have a : ∀ (this : LocalizedModule (Submonoid.powers f) (H1Cotangent R A) ≃ₗ[A] H1Cotangent.{u_1, u_2} R (Localization.Away f)),
  Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.Away f)) ↔
    Subsingleton (LocalizedModule.Away f (H1Cotangent R A))
Tactic: have := IsLocalizedModule.iso (.powers f) (H1Cotangent.map R R A (Localization.Away f))
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
f : A
this : LocalizedModule (Submonoid.powers f) (H1Cotangent R A) ≃ₗ[A] H1Cotangent.{u_1, u_2} R (Localization.Away f)
⊢ Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.Away f)) ↔
    Subsingleton (LocalizedModule.Away f (H1Cotangent R A))
have a : Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.Away f)) ↔
  Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.Away f))
Tactic: rw [this.subsingleton_congr]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
f : A
⊢ Module.Projective.{u_2, u_2} (Localization.Away f) Ω[Localization.Away f⁄R] ↔
    Subset (α := Set (PrimeSpectrum A)) (PrimeSpectrum.zeroLocus {f})ᶜ (Module.freeLocus A Ω[A⁄R])
have a : Module.Projective.{u_2, u_2} (Localization.Away f) Ω[Localization.Away f⁄R] ↔
  Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Tactic: rw [← PrimeSpectrum.basicOpen_eq_zeroLocus_compl, Module.basicOpen_subset_freeLocus_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
f : A
⊢ Module.Projective.{u_2, u_2} (Localization.Away f) Ω[Localization.Away f⁄R] ↔
    Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
have a : ∀ (this : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[A] Ω[Localization.Away f⁄R]),
  Module.Projective.{u_2, u_2} (Localization.Away f) Ω[Localization.Away f⁄R] ↔
    Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Tactic: have := IsLocalizedModule.iso (.powers f)
        (KaehlerDifferential.map R R A (Localization.Away f))
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
f : A
this : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[A] Ω[Localization.Away f⁄R]
⊢ Module.Projective.{u_2, u_2} (Localization.Away f) Ω[Localization.Away f⁄R] ↔
    Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
have a : ∀ (this : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[Localization.Away f] Ω[Localization.Away f⁄R]),
  Module.Projective.{u_2, u_2} (Localization.Away f) Ω[Localization.Away f⁄R] ↔
    Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Tactic: have := this.extendScalarsOfIsLocalization (.powers f) (Localization.Away f)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
f : A
⊢ (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum A)) ⊆ smoothLocus R A ↔ Smooth.{u_2, u_1} R (Localization.Away f)
have this : FinitePresentation A (Localization.Away f)
Tactic: have : FinitePresentation A (Localization.Away f) := IsLocalization.Away.finitePresentation f
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
f : A
this : FinitePresentation A (Localization.Away f)
⊢ (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum A)) ⊆ smoothLocus R A ↔ Smooth.{u_2, u_1} R (Localization.Away f)
have rw : FormallySmooth.{u_1, u_2} R (Localization.Away f) ↔ Smooth.{u_2, u_1} R (Localization.Away f)
Tactic: rw [basicOpen_subset_smoothLocus_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
⊢ Eq (α := Set (PrimeSpectrum A)) (smoothLocus R A) Set.univ ↔ FormallySmooth R A
have have : ∀ (this : A ≃ₐ[A] Localization.Away (M := A) 1),
  Eq (α := Set (PrimeSpectrum A)) (smoothLocus R A) Set.univ ↔ FormallySmooth R A
Tactic: have := IsLocalization.atUnits A (.powers 1) (S := Localization.Away (1 : A)) (by simp)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
this : A ≃ₐ[A] Localization.Away (M := A) 1
⊢ Eq (α := Set (PrimeSpectrum A)) (smoothLocus R A) Set.univ ↔ FormallySmooth R A
have rw : Eq (α := Set (PrimeSpectrum A)) (smoothLocus R A) Set.univ ↔
  (↑(PrimeSpectrum.basicOpen 1) : Set (PrimeSpectrum A)) ⊆ smoothLocus R A
Tactic: rw [Algebra.FormallySmooth.iff_of_equiv (this.restrictScalars R),
    ← basicOpen_subset_smoothLocus_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Smooth R A
⊢ Eq (α := Set (PrimeSpectrum A)) (smoothLocus R A) Set.univ
have rw : FormallySmooth R A
Tactic: rw [smoothLocus_eq_univ_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
Af : Type u_3
inst_3 : CommRing Af
inst_4 : Algebra A Af
inst_5 : Algebra R Af
inst_6 : IsScalarTower R A Af
f : A
inst_7 : IsLocalization.Away f Af
⊢ Eq (α := Set (PrimeSpectrum Af))
    (Set.preimage (β := PrimeSpectrum A) (PrimeSpectrum.comap (algebraMap A Af)) (smoothLocus R A)) (smoothLocus R Af)
have h : ∀ (p : PrimeSpectrum Af),
  Membership.mem (γ := Set (PrimeSpectrum Af))
      (Set.preimage (β := PrimeSpectrum A) (PrimeSpectrum.comap (algebraMap A Af)) (smoothLocus R A)) p ↔
    Membership.mem (γ := Set (PrimeSpectrum Af)) (smoothLocus R Af) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
Af : Type u_3
inst_3 : CommRing Af
inst_4 : Algebra A Af
inst_5 : Algebra R Af
inst_6 : IsScalarTower R A Af
f : A
inst_7 : IsLocalization.Away f Af
p : PrimeSpectrum Af
q : PrimeSpectrum A := PrimeSpectrum.comap (algebraMap A Af) p
⊢ Membership.mem (γ := Set (PrimeSpectrum Af))
      (Set.preimage (β := PrimeSpectrum A) (PrimeSpectrum.comap (algebraMap A Af)) (smoothLocus R A)) p ↔
    Membership.mem (γ := Set (PrimeSpectrum Af)) (smoothLocus R Af) p
have this : IsLocalization.AtPrime.{u_2, u_3} (Localization.AtPrime p.asIdeal) q.asIdeal
Tactic: have : IsLocalization.AtPrime (Localization.AtPrime p.asIdeal) q.asIdeal :=
    IsLocalization.isLocalization_isLocalization_atPrime_isLocalization (.powers f) _ p.asIdeal
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
Af : Type u_3
inst_3 : CommRing Af
inst_4 : Algebra A Af
inst_5 : Algebra R Af
inst_6 : IsScalarTower R A Af
f : A
inst_7 : IsLocalization.Away f Af
p : PrimeSpectrum Af
q : PrimeSpectrum A := PrimeSpectrum.comap (algebraMap A Af) p
this : IsLocalization.AtPrime.{u_2, u_3} (Localization.AtPrime p.asIdeal) q.asIdeal
⊢ Membership.mem (γ := Set (PrimeSpectrum Af))
      (Set.preimage (β := PrimeSpectrum A) (PrimeSpectrum.comap (algebraMap A Af)) (smoothLocus R A)) p ↔
    Membership.mem (γ := Set (PrimeSpectrum Af)) (smoothLocus R Af) p
have h : AlgEquiv.{u_1, u_2, u_3} R (Localization.AtPrime (PrimeSpectrum.asIdeal (PrimeSpectrum.comap (algebraMap A Af) p)))
  (Localization.AtPrime p.asIdeal)
Tactic: refine Algebra.FormallySmooth.iff_of_equiv ?_
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
⊢ IsOpen (X := PrimeSpectrum A) (smoothLocus R A)
have rw : ∀ (x : PrimeSpectrum A),
  Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) x → ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t
Tactic: rw [isOpen_iff_forall_mem_open]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
x : PrimeSpectrum A
hx : Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) x
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t
have obtain : ∀ (f : A) (hxf : x ∈ (↑(basicOpen f) : Set (PrimeSpectrum A)))
  (hf : (↑(basicOpen f) : Set (PrimeSpectrum A)) ⊆ Module.freeLocus A Ω[A⁄R]), ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t
Tactic: obtain ⟨_, ⟨_, ⟨f, rfl⟩, rfl⟩, hxf, hf⟩ :=
    isBasis_basic_opens.exists_subset_of_mem_open
    (smoothLocus_eq_compl_support_inter.le hx).2 Module.isOpen_freeLocus