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

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]))
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

Tactic:
let Af := Localization.Away 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
⊢ ∃ 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 ∈ smoothLocus R A, ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

Tactic:
intro x hx

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
⊢ ∃ 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
⊢ ∃ 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

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 : ↑(basicOpen f) ⊆ Module.freeLocus A (Ω[A⁄R])
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

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)
this✝ : FinitePresentation R (Localization.Away f)
this : IsOpen (smoothLocus R Af)
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

Tactic:
rw [← smoothLocus_comap_of_isLocalization f] at this

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)
this : IsOpen (⇑(comap (algebraMap A Af)) ⁻¹' smoothLocus R A)
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

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)
this✝ : FinitePresentation R (Localization.Away f)
this : IsOpen (⇑(comap (algebraMap A Af)) '' (⇑(comap (algebraMap A Af)) ⁻¹' smoothLocus R A))
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

Tactic:
rw [Set.image_preimage_eq_inter_range, localization_away_comap_range Af f] at this

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)
this : IsOpen (smoothLocus R A ∩ ↑(basicOpen 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
⊢ IsOpen (smoothLocus R A)

Tactic:
rw [isOpen_iff_forall_mem_open]

Result:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
⊢ ∀ x ∈ smoothLocus R A, ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

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)
this : FinitePresentation R (Localization.Away f)
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

Tactic:
have : IsOpen (smoothLocus R Af) := by
  have := IsLocalizedModule.iso (.powers f)
    (KaehlerDifferential.map R R A (Localization.Away f))
  have := LinearEquiv.ofBijective (this.extendScalarsOfIsLocalization
    (.powers f) (Localization.Away f)) this.bijective
  have := Module.Projective.of_equiv this
  rw [smoothLocus_eq_compl_support_inter, Module.support_eq_zeroLocus]
  exact (isClosed_zeroLocus _).isOpen_compl.inter Module.isOpen_freeLocus

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)
this : IsOpen (smoothLocus R Af)
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

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 : ↑(basicOpen f) ⊆ Module.freeLocus A (Ω[A⁄R])
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

Tactic:
rw [Module.basicOpen_subset_freeLocus_iff] at hf

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]))
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

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)
this✝ : FinitePresentation R (Localization.Away f)
this : IsOpen (smoothLocus R A ∩ ↑(basicOpen f))
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

Tactic:
exact ⟨_, Set.inter_subset_left, this, hx, hxf⟩

Result:
no goals