awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.Locus
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 :
  ∀
    (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))
⊢ 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))
-- Module: Mathlib.RingTheory.Smooth.Locus
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 (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:
this.subsingleton_congr.symm

Premises used: Equiv.subsingleton_congr, LinearEquiv.toAddEquiv, AddEquiv.toEquiv, Iff.symm
-- Module: Mathlib.RingTheory.Smooth.Locus
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 (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:
exact this.subsingleton_congr.symm

Premises used: Equiv.subsingleton_congr, LinearEquiv.toAddEquiv, AddEquiv.toEquiv, Iff.symm
-- Module: Mathlib.RingTheory.Smooth.Locus
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]
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])
⊢ 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:
trans Module.Free (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R]

Premises used: Localization.AtPrime, Module.Free, KaehlerDifferential, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Smooth.Locus
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
⊢ EssFiniteType A (Localization.AtPrime p.asIdeal)

Tactic:
have : EssFiniteType A (Localization.AtPrime p.asIdeal) :=
        .of_isLocalization _ p.asIdeal.primeCompl
-- Module: Mathlib.RingTheory.Smooth.Locus
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)
⊢ EssFiniteType.{u_1, u_2} R (Localization.AtPrime p.asIdeal)

Tactic:
have : EssFiniteType R (Localization.AtPrime p.asIdeal) := .comp _ A _
-- Module: Mathlib.RingTheory.Smooth.Locus
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_1 : EssFiniteType A (Localization.AtPrime p.asIdeal)
this : EssFiniteType.{u_1, u_2} R (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]

Tactic:
⟨fun _ ↦ Module.free_of_flat_of_isLocalRing, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, Module.free_of_flat_of_isLocalRing
-- Module: Mathlib.RingTheory.Smooth.Locus
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_1 : EssFiniteType A (Localization.AtPrime p.asIdeal)
this : EssFiniteType.{u_1, u_2} R (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]

Tactic:
exact ⟨fun _ ↦ Module.free_of_flat_of_isLocalRing, fun _ ↦ inferInstance⟩
-- Module: Mathlib.RingTheory.Smooth.Locus
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
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])
⊢ 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))
-- Module: Mathlib.RingTheory.Smooth.Locus
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]
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])
⊢ 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)
-- Module: Mathlib.RingTheory.Smooth.Locus
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_1 : LocalizedModule p.asIdeal.primeCompl Ω[A⁄R] ≃ₗ[A] Ω[Localization.AtPrime p.asIdeal⁄R]
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:
⟨fun H ↦ H.of_equiv' this.symm, fun H ↦ H.of_equiv' this⟩

Premises used: LinearEquiv.symm, Module.Free.of_equiv', Iff.intro
-- Module: Mathlib.RingTheory.Smooth.Locus
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_1 : LocalizedModule p.asIdeal.primeCompl Ω[A⁄R] ≃ₗ[A] Ω[Localization.AtPrime p.asIdeal⁄R]
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:
exact ⟨fun H ↦ H.of_equiv' this.symm, fun H ↦ H.of_equiv' this⟩
-- Module: Mathlib.RingTheory.Smooth.Locus
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
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])
⊢ (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum A)) ⊆ smoothLocus R A ↔
    FormallySmooth.{u_1, u_2} R (Localization.Away f)

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]

Premises used: compl_compl, Set.subset_inter_iff, Set.subset_compl_comm, iff_comm, and_comm, LocalizedModule.subsingleton_iff_support_subset, PrimeSpectrum.basicOpen_eq_zeroLocus_compl, Algebra.formallySmooth_iff, Algebra.smoothLocus_eq_compl_support_inter
-- Module: Mathlib.RingTheory.Smooth.Locus
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))
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])
⊢ 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:
congr! 1
-- Module: Mathlib.RingTheory.Smooth.Locus
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 :
  ∀
    (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))
⊢ 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))
-- Module: Mathlib.RingTheory.Smooth.Locus
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)
a a₁ :
  Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.Away f)) ↔
    Subsingleton (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:
rw [this.subsingleton_congr]

Premises used: Equiv.subsingleton_congr, LinearEquiv.toAddEquiv, AddEquiv.toEquiv
-- Module: Mathlib.RingTheory.Smooth.Locus
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 :
  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])
⊢ 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:
rw [← PrimeSpectrum.basicOpen_eq_zeroLocus_compl, Module.basicOpen_subset_freeLocus_iff]

Premises used: Module.basicOpen_subset_freeLocus_iff, PrimeSpectrum.basicOpen_eq_zeroLocus_compl
-- Module: Mathlib.RingTheory.Smooth.Locus
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 :
  ∀ (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])
⊢ 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))
-- Module: Mathlib.RingTheory.Smooth.Locus
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]
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])
⊢ 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)
-- Module: Mathlib.RingTheory.Smooth.Locus
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_1 : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[A] Ω[Localization.Away f⁄R]
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:
⟨fun _ ↦ .of_equiv this.symm, fun _ ↦ .of_equiv this⟩

Premises used: LinearEquiv.symm, Module.Projective.of_equiv, Iff.intro
-- Module: Mathlib.RingTheory.Smooth.Locus
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_1 : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[A] Ω[Localization.Away f⁄R]
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:
exact ⟨fun _ ↦ .of_equiv this.symm, fun _ ↦ .of_equiv this⟩
-- Module: Mathlib.RingTheory.Smooth.Locus
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
⊢ FinitePresentation A (Localization.Away f)

Tactic:
have : FinitePresentation A (Localization.Away f) := IsLocalization.Away.finitePresentation f
-- Module: Mathlib.RingTheory.Smooth.Locus
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)
rw : FormallySmooth.{u_1, u_2} R (Localization.Away f) ↔ Smooth.{u_2, u_1} R (Localization.Away f)
⊢ (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum A)) ⊆ smoothLocus R A ↔ Smooth.{u_2, u_1} R (Localization.Away f)

Tactic:
rw [basicOpen_subset_smoothLocus_iff]

Premises used: Algebra.basicOpen_subset_smoothLocus_iff
-- Module: Mathlib.RingTheory.Smooth.Locus
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)
⊢ FormallySmooth.{u_1, u_2} R (Localization.Away f) ↔ Smooth.{u_2, u_1} R (Localization.Away f)

Tactic:
⟨fun H ↦ ⟨H, .trans _ A _⟩, fun H ↦ H.1⟩

Premises used: Algebra.Smooth.formallySmooth, Algebra.Smooth.mk, Localization.Away, Iff.intro, Algebra.FinitePresentation.trans
-- Module: Mathlib.RingTheory.Smooth.Locus
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)
⊢ FormallySmooth.{u_1, u_2} R (Localization.Away f) ↔ Smooth.{u_2, u_1} R (Localization.Away f)

Tactic:
exact ⟨fun H ↦ ⟨H, .trans _ A _⟩, fun H ↦ H.1⟩
-- Module: Mathlib.RingTheory.Smooth.Locus
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
⊢ LE.le (α := Submonoid A) (Submonoid.powers 1) (IsUnit.submonoid A)

Tactic:
simp
-- Module: Mathlib.RingTheory.Smooth.Locus
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
have :
  ∀ (this : A ≃ₐ[A] Localization.Away (M := A) 1),
    Eq (α := Set (PrimeSpectrum A)) (smoothLocus R A) Set.univ ↔ FormallySmooth R A
⊢ 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)
-- Module: Mathlib.RingTheory.Smooth.Locus
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
rw :
  Eq (α := Set (PrimeSpectrum A)) (smoothLocus R A) Set.univ ↔
    (↑(PrimeSpectrum.basicOpen 1) : Set (PrimeSpectrum A)) ⊆ smoothLocus R A
⊢ Eq (α := Set (PrimeSpectrum A)) (smoothLocus R A) Set.univ ↔ FormallySmooth R A

Tactic:
rw [Algebra.FormallySmooth.iff_of_equiv (this.restrictScalars R),
    ← basicOpen_subset_smoothLocus_iff]

Premises used: AlgEquiv.restrictScalars, Algebra.basicOpen_subset_smoothLocus_iff, Algebra.FormallySmooth.iff_of_equiv
-- Module: Mathlib.RingTheory.Smooth.Locus
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 ↔
    (↑(PrimeSpectrum.basicOpen 1) : Set (PrimeSpectrum A)) ⊆ smoothLocus R A

Tactic:
simp
-- Module: Mathlib.RingTheory.Smooth.Locus
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
rw : FormallySmooth R A
⊢ Eq (α := Set (PrimeSpectrum A)) (smoothLocus R A) Set.univ

Tactic:
rw [smoothLocus_eq_univ_iff]

Premises used: Algebra.smoothLocus_eq_univ_iff
-- Module: Mathlib.RingTheory.Smooth.Locus
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
⊢ FormallySmooth R A

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Smooth.Locus
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
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
⊢ Eq (α := Set (PrimeSpectrum Af))
    (Set.preimage (β := PrimeSpectrum A) (PrimeSpectrum.comap (algebraMap A Af)) (smoothLocus R A)) (smoothLocus R Af)

Tactic:
ext p
-- Module: Mathlib.RingTheory.Smooth.Locus
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
⊢ 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
-- Module: Mathlib.RingTheory.Smooth.Locus
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

Tactic:
Algebra.FormallySmooth.iff_of_equiv ?_

Premises used: Set.Mem, setOf, Set.preimage, Algebra.smoothLocus, Algebra.FormallySmooth.iff_of_equiv
-- Module: Mathlib.RingTheory.Smooth.Locus
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
h :
  AlgEquiv.{u_1, u_2, u_3} R (Localization.AtPrime (PrimeSpectrum.asIdeal (PrimeSpectrum.comap (algebraMap A Af) p)))
    (Localization.AtPrime p.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

Tactic:
refine Algebra.FormallySmooth.iff_of_equiv ?_

Premises used: Algebra.FormallySmooth.iff_of_equiv
-- Module: Mathlib.RingTheory.Smooth.Locus
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
⊢ AlgEquiv.{u_1, u_2, u_3} R (Localization.AtPrime (PrimeSpectrum.asIdeal (PrimeSpectrum.comap (algebraMap A Af) p)))
    (Localization.AtPrime p.asIdeal)

Tactic:
exact (IsLocalization.algEquiv q.asIdeal.primeCompl _ _).restrictScalars R

Premises used: AlgEquiv.restrictScalars, IsLocalization.algEquiv, Ideal.primeCompl, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Smooth.Locus
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
rw :
  ∀ (x : PrimeSpectrum A),
    Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) x → ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t
⊢ IsOpen (X := PrimeSpectrum A) (smoothLocus R A)

Tactic:
rw [isOpen_iff_forall_mem_open]

Premises used: isOpen_iff_forall_mem_open
-- Module: Mathlib.RingTheory.Smooth.Locus
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
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
⊢ ∃ 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

Premises used: Eq.le, Module.isOpen_freeLocus, And.right, Algebra.smoothLocus_eq_compl_support_inter, PrimeSpectrum.isBasis_basic_opens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open