-- Mathlib/RingTheory/Smooth/Locus.lean
lemma isOpen_smoothLocus [FinitePresentation R A] : IsOpen (smoothLocus R A)

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R]))
Af : Type u := Localization.Away f
this✝ : FinitePresentation A (Localization.Away f)
this : FinitePresentation R (Localization.Away f)
⊢ IsOpen (smoothLocus R Af)

Tactic:
have := IsLocalizedModule.iso (.powers f)
  (KaehlerDifferential.map R R A (Localization.Away f))

Result:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R]))
Af : Type u := Localization.Away f
this✝¹ : FinitePresentation A (Localization.Away f)
this✝ : FinitePresentation R (Localization.Away f)
this : LocalizedModule (Submonoid.powers f) (Ω[A⁄R]) ≃ₗ[A] Ω[Localization.Away f⁄R]
⊢ IsOpen (smoothLocus R Af)

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R]))
Af : Type u := Localization.Away f
this✝³ : FinitePresentation A (Localization.Away f)
this✝² : FinitePresentation R (Localization.Away f)
this✝¹ : 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]
this : Module.Projective (Localization.Away f) (Ω[Localization.Away f⁄R])
⊢ IsOpen (smoothLocus R Af)

Tactic:
rw [smoothLocus_eq_compl_support_inter, Module.support_eq_zeroLocus]

Result:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R]))
Af : Type u := Localization.Away f
this✝³ : FinitePresentation A (Localization.Away f)
this✝² : FinitePresentation R (Localization.Away f)
this✝¹ : 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]
this : Module.Projective (Localization.Away f) (Ω[Localization.Away f⁄R])
⊢ IsOpen ((zeroLocus ↑(Module.annihilator Af (H1Cotangent R Af)))ᶜ ∩ Module.freeLocus Af (Ω[Af⁄R]))

Proof state:
case intro.intro.intro.intro.intro.intro
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R]))
Af : Type u := Localization.Away f
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

Tactic:
have : Algebra.FinitePresentation A (Localization.Away f) :=
  IsLocalization.Away.finitePresentation f

Result:
case intro.intro.intro.intro.intro.intro
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R]))
Af : Type u := Localization.Away f
this : FinitePresentation A (Localization.Away f)
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R]))
Af : Type u := Localization.Away f
this✝² : FinitePresentation A (Localization.Away f)
this✝¹ : FinitePresentation R (Localization.Away f)
this✝ : 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]
⊢ IsOpen (smoothLocus R Af)

Tactic:
have := Module.Projective.of_equiv this

Result:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R]))
Af : Type u := Localization.Away f
this✝³ : FinitePresentation A (Localization.Away f)
this✝² : FinitePresentation R (Localization.Away f)
this✝¹ : 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]
this : Module.Projective (Localization.Away f) (Ω[Localization.Away f⁄R])
⊢ IsOpen (smoothLocus R Af)

Proof state:
case intro.intro.intro.intro.intro.intro
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R]))
Af : Type u := Localization.Away f
this : FinitePresentation A (Localization.Away f)
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

Tactic:
have : Algebra.FinitePresentation R (Localization.Away f) :=
  .trans _ A _

Result:
case intro.intro.intro.intro.intro.intro
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R]))
Af : Type u := Localization.Away f
this✝ : FinitePresentation A (Localization.Away f)
this : FinitePresentation R (Localization.Away f)
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R]))
Af : Type u := Localization.Away f
this✝³ : FinitePresentation A (Localization.Away f)
this✝² : FinitePresentation R (Localization.Away f)
this✝¹ : 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]
this : Module.Projective (Localization.Away f) (Ω[Localization.Away f⁄R])
⊢ IsOpen ((zeroLocus ↑(Module.annihilator Af (H1Cotangent R Af)))ᶜ ∩ Module.freeLocus Af (Ω[Af⁄R]))

Tactic:
exact (isClosed_zeroLocus _).isOpen_compl.inter Module.isOpen_freeLocus

Result:
no goals