-- Mathlib/RingTheory/Smooth/Locus.lean
lemma basicOpen_subset_smoothLocus_iff [FinitePresentation R A] {f : A} :
    ↑(PrimeSpectrum.basicOpen f) ⊆ smoothLocus R A ↔
      Algebra.FormallySmooth R (Localization.Away f)

Proof state:
case a.h.e'_2.a
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
this : LocalizedModule (Submonoid.powers f) (Ω[A⁄R]) ≃ₗ[A] Ω[Localization.Away f⁄R]
⊢ Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R])) ↔
    Module.Projective (Localization.Away f) (Ω[Localization.Away f⁄R])

Tactic:
have := LinearEquiv.ofBijective (this.extendScalarsOfIsLocalization
  (.powers f) (Localization.Away f)) this.bijective

Result:
case a.h.e'_2.a
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
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]
⊢ Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R])) ↔
    Module.Projective (Localization.Away f) (Ω[Localization.Away f⁄R])

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ smoothLocus R A ↔ FormallySmooth 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_subsingleton_and_projective]

Result:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ Subsingleton (LocalizedModule (Submonoid.powers f) (H1Cotangent R A)) ∧
      (PrimeSpectrum.zeroLocus {f})ᶜ ⊆ Module.freeLocus A (Ω[A⁄R]) ↔
    Subsingleton (H1Cotangent R (Localization.Away f)) ∧
      Module.Projective (Localization.Away f) (Ω[Localization.Away f⁄R])

Proof state:
case a.h.e'_1.a
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
this : LocalizedModule (Submonoid.powers f) (H1Cotangent R A) ≃ₗ[A] H1Cotangent R (Localization.Away f)
⊢ Subsingleton (LocalizedModule (Submonoid.powers f) (H1Cotangent R A)) ↔
    Subsingleton (H1Cotangent R (Localization.Away f))

Tactic:
rw [this.subsingleton_congr]

Result:
no goals

Proof state:
case a.h.e'_2.a
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
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]
⊢ Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R])) ↔
    Module.Projective (Localization.Away f) (Ω[Localization.Away f⁄R])

Tactic:
exact ⟨fun _ ↦ .of_equiv this, fun _ ↦ .of_equiv this.symm⟩

Result:
no goals

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ Subsingleton (LocalizedModule (Submonoid.powers f) (H1Cotangent R A)) ∧
      (PrimeSpectrum.zeroLocus {f})ᶜ ⊆ Module.freeLocus A (Ω[A⁄R]) ↔
    Subsingleton (H1Cotangent R (Localization.Away f)) ∧
      Module.Projective (Localization.Away f) (Ω[Localization.Away f⁄R])

Tactic:
congr! 1

Result:
case a.h.e'_1.a
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ Subsingleton (LocalizedModule (Submonoid.powers f) (H1Cotangent R A)) ↔
    Subsingleton (H1Cotangent R (Localization.Away f))

case a.h.e'_2.a
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ (PrimeSpectrum.zeroLocus {f})ᶜ ⊆ Module.freeLocus A (Ω[A⁄R]) ↔
    Module.Projective (Localization.Away f) (Ω[Localization.Away f⁄R])

Proof state:
case a.h.e'_2.a
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ (PrimeSpectrum.zeroLocus {f})ᶜ ⊆ Module.freeLocus A (Ω[A⁄R]) ↔
    Module.Projective (Localization.Away f) (Ω[Localization.Away f⁄R])

Tactic:
rw [← PrimeSpectrum.basicOpen_eq_zeroLocus_compl, Module.basicOpen_subset_freeLocus_iff]

Result:
case a.h.e'_2.a
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R])) ↔
    Module.Projective (Localization.Away f) (Ω[Localization.Away f⁄R])

Proof state:
case a.h.e'_1.a
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ Subsingleton (LocalizedModule (Submonoid.powers f) (H1Cotangent R A)) ↔
    Subsingleton (H1Cotangent R (Localization.Away f))

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

Result:
case a.h.e'_1.a
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
this : LocalizedModule (Submonoid.powers f) (H1Cotangent R A) ≃ₗ[A] H1Cotangent R (Localization.Away f)
⊢ Subsingleton (LocalizedModule (Submonoid.powers f) (H1Cotangent R A)) ↔
    Subsingleton (H1Cotangent R (Localization.Away f))

Proof state:
case a.h.e'_2.a
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R])) ↔
    Module.Projective (Localization.Away f) (Ω[Localization.Away f⁄R])

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

Result:
case a.h.e'_2.a
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
this : LocalizedModule (Submonoid.powers f) (Ω[A⁄R]) ≃ₗ[A] Ω[Localization.Away f⁄R]
⊢ Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) (Ω[A⁄R])) ↔
    Module.Projective (Localization.Away f) (Ω[Localization.Away f⁄R])