-- Mathlib/RingTheory/Smooth/Locus.lean
lemma smoothLocus_eq_compl_support_inter [EssFiniteType R A] :
    smoothLocus R A = (Module.support A (H1Cotangent R A))ᶜ ∩ Module.freeLocus A (Ω[A⁄R])

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
this✝ : 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 (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R]) ↔
    Module.Free (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⟩

Result:
no goals

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
⊢ smoothLocus R A = (Module.support A (H1Cotangent R A))ᶜ ∩ Module.freeLocus A (Ω[A⁄R])

Tactic:
ext p

Result:
case h
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
⊢ p ∈ smoothLocus R A ↔ p ∈ (Module.support A (H1Cotangent R A))ᶜ ∩ Module.freeLocus A (Ω[A⁄R])

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
this : EssFiniteType A (Localization.AtPrime p.asIdeal)
⊢ Module.Projective (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R]) ↔
    Module.Free (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R])

Tactic:
have : EssFiniteType R (Localization.AtPrime p.asIdeal) := .comp _ A _

Result:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
this✝ : EssFiniteType A (Localization.AtPrime p.asIdeal)
this : EssFiniteType R (Localization.AtPrime p.asIdeal)
⊢ Module.Projective (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R]) ↔
    Module.Free (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R])

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
this : LocalizedModule p.asIdeal.primeCompl (Ω[A⁄R]) ≃ₗ[A] Ω[Localization.AtPrime p.asIdeal⁄R]
⊢ Module.Free (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R]) ↔
    Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (Ω[A⁄R]))

Tactic:
have := LinearEquiv.ofBijective (this.extendScalarsOfIsLocalization
  p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal)) this.bijective

Result:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
this✝ : 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 (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R]) ↔
    Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (Ω[A⁄R]))

Proof state:
case h
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
⊢ p ∈ smoothLocus R A ↔ p ∈ (Module.support A (H1Cotangent R A))ᶜ ∩ Module.freeLocus A (Ω[A⁄R])

Tactic:
simp only [Set.mem_inter_iff, Set.mem_compl_iff, Module.not_mem_support_iff,
  Module.mem_freeLocus]

Result:
case h
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
⊢ p ∈ smoothLocus R A ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A)) ∧
      Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (Ω[A⁄R]))

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
⊢ Module.Projective (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R]) ↔
    Module.Free (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R])

Tactic:
have : EssFiniteType A (Localization.AtPrime p.asIdeal) :=
  .of_isLocalization _ p.asIdeal.primeCompl

Result:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
this : EssFiniteType A (Localization.AtPrime p.asIdeal)
⊢ Module.Projective (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R]) ↔
    Module.Free (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R])

Proof state:
case h
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
⊢ p ∈ smoothLocus R A ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A)) ∧
      Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (Ω[A⁄R]))

Tactic:
refine Algebra.FormallySmooth.iff_subsingleton_and_projective.trans ?_

Result:
case h
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
⊢ Subsingleton (H1Cotangent R (Localization.AtPrime p.asIdeal)) ∧
      Module.Projective (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R]) ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A)) ∧
      Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (Ω[A⁄R]))

Proof state:
case h.a.h.e'_1.a
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
this : LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A) ≃ₗ[A] H1Cotangent R (Localization.AtPrime p.asIdeal)
⊢ Subsingleton (H1Cotangent R (Localization.AtPrime p.asIdeal)) ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))

Tactic:
exact this.subsingleton_congr.symm

Result:
no goals

Proof state:
case h.a.h.e'_2.a
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
⊢ Module.Projective (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R]) ↔
    Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (Ω[A⁄R]))

Tactic:
trans Module.Free (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R])

Result:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
⊢ Module.Projective (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R]) ↔
    Module.Free (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R])

R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
⊢ Module.Free (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R]) ↔
    Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (Ω[A⁄R]))

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
this✝ : EssFiniteType A (Localization.AtPrime p.asIdeal)
this : EssFiniteType R (Localization.AtPrime p.asIdeal)
⊢ Module.Projective (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R]) ↔
    Module.Free (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R])

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

Result:
no goals