awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization (M := R) S)
p' : Ideal R := Ideal.comap (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this_1 : Algebra (Localization (M := R) S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization (M := R) S) Rₚ S p'.primeCompl hp'
this_2 : IsScalarTower R (Localization (M := R) S) Rₚ
this_3 : IsLocalization.AtPrime Rₚ p.asIdeal
this_4 : Module (Localization (M := R) S) Mₚ := compHom Mₚ (algebraMap (Localization (M := R) S) Rₚ)
this_5 : IsScalarTower R (Localization (M := R) S) Mₚ
this_6 : IsScalarTower (Localization (M := R) S) Rₚ Mₚ
l : LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
  (LocalizedModule p'.primeCompl M) :=
  LinearMap.extendScalarsOfIsLocalization S (Localization (M := R) S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
this_7 :
  IsLocalizedModule p'.primeCompl
    ((↑R :
        {S : Type uR} →
          {M M₂ : Type (max uM uR)} →
            [inst : Semiring R] →
              [inst_3 : Semiring S] →
                [inst_4 : AddCommMonoid M] →
                  [inst_5 : AddCommMonoid M₂] →
                    [inst_6 : Module R M] →
                      [inst_7 : Module R M₂] →
                        [inst_8 : Module S M] →
                          [inst_9 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      l)
this : IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization (M := R) S) p'.primeCompl) l
x : R
s : ↥S
hx : IsLocalization.mk' (Localization (M := R) S) x s ∈ p.asIdeal.primeCompl
⊢ (algebraMap R (Localization (M := R) S) : (a : R) → Localization S) x =
    HMul.hMul (α := Localization (M := R) S)
      ((algebraMap R (Localization (M := R) S) : (a : R) → Localization S) (↑s : R) : Localization (M := R) S)
      (↑(Subtype.mk (p := fun (x : Localization (M := R) S) ↦ x ∈ p.asIdeal.primeCompl)
            (IsLocalization.mk' (Localization (M := R) S) x s) hx) :
        Localization S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization (M := R) S)
p' : Ideal R := Ideal.comap (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this_1 : Algebra (Localization (M := R) S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization (M := R) S) Rₚ S p'.primeCompl hp'
this_2 : IsScalarTower R (Localization (M := R) S) Rₚ
this_3 : IsLocalization.AtPrime Rₚ p.asIdeal
this_4 : Module (Localization (M := R) S) Mₚ := compHom Mₚ (algebraMap (Localization (M := R) S) Rₚ)
this_5 : IsScalarTower R (Localization (M := R) S) Mₚ
this_6 : IsScalarTower (Localization (M := R) S) Rₚ Mₚ
l : LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
  (LocalizedModule p'.primeCompl M) :=
  LinearMap.extendScalarsOfIsLocalization S (Localization (M := R) S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
this_7 :
  IsLocalizedModule p'.primeCompl
    ((↑R :
        {S : Type uR} →
          {M M₂ : Type (max uM uR)} →
            [inst : Semiring R] →
              [inst_3 : Semiring S] →
                [inst_4 : AddCommMonoid M] →
                  [inst_5 : AddCommMonoid M₂] →
                    [inst_6 : Module R M] →
                      [inst_7 : Module R M₂] →
                        [inst_8 : Module S M] →
                          [inst_9 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      l)
this : IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization (M := R) S) p'.primeCompl) l
x : R
s : ↥S
hx : IsLocalization.mk' (Localization (M := R) S) x s ∈ p.asIdeal.primeCompl
h' : ∀ (H : x ∈ (↑p' : Set R)), IsLocalization.mk' (Localization (M := R) S) x s ∈ (↑p.asIdeal : Set (Localization S))
⊢ ∃ (m : Localization (M := R) S),
    Membership.mem (γ := Submonoid (Localization (M := R) S))
      (Algebra.algebraMapSubmonoid (Localization (M := R) S) p'.primeCompl)
      (m *
        (↑(Subtype.mk (p := fun (x : Localization (M := R) S) ↦ x ∈ p.asIdeal.primeCompl)
              (IsLocalization.mk' (Localization (M := R) S) x s) hx) :
          Localization S))

Tactic:
refine ⟨algebraMap _ _ s.1, x, fun H ↦ hx ?_, by simp⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization (M := R) S)
p' : Ideal R := Ideal.comap (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this_1 : Algebra (Localization (M := R) S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization (M := R) S) Rₚ S p'.primeCompl hp'
this_2 : IsScalarTower R (Localization (M := R) S) Rₚ
this_3 : IsLocalization.AtPrime Rₚ p.asIdeal
this_4 : Module (Localization (M := R) S) Mₚ := compHom Mₚ (algebraMap (Localization (M := R) S) Rₚ)
this_5 : IsScalarTower R (Localization (M := R) S) Mₚ
this_6 : IsScalarTower (Localization (M := R) S) Rₚ Mₚ
l : LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
  (LocalizedModule p'.primeCompl M) :=
  LinearMap.extendScalarsOfIsLocalization S (Localization (M := R) S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
this_7 :
  IsLocalizedModule p'.primeCompl
    ((↑R :
        {S : Type uR} →
          {M M₂ : Type (max uM uR)} →
            [inst : Semiring R] →
              [inst_3 : Semiring S] →
                [inst_4 : AddCommMonoid M] →
                  [inst_5 : AddCommMonoid M₂] →
                    [inst_6 : Module R M] →
                      [inst_7 : Module R M₂] →
                        [inst_8 : Module S M] →
                          [inst_9 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      l)
this : IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization (M := R) S) p'.primeCompl) l
x : R
s : ↥S
hx : IsLocalization.mk' (Localization (M := R) S) x s ∈ p.asIdeal.primeCompl
H : x ∈ (↑p' : Set R)
h' :
  HMul.hMul (α := Localization (M := R) S) (β := Localization (M := R) S)
      ((algebraMap R (Localization (M := R) S) : (a : R) → Localization S) x : Localization (M := R) S)
      (IsLocalization.mk' (Localization (M := R) S) 1 s : Localization (M := R) S) ∈
    (↑p.asIdeal : Set (Localization S))
⊢ IsLocalization.mk' (Localization (M := R) S) x s ∈ (↑p.asIdeal : Set (Localization S))

Tactic:
rw [IsLocalization.mk'_eq_mul_mk'_one]

Premises used: IsLocalization.mk'_eq_mul_mk'_one
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization (M := R) S)
p' : Ideal R := Ideal.comap (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this_1 : Algebra (Localization (M := R) S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization (M := R) S) Rₚ S p'.primeCompl hp'
this_2 : IsScalarTower R (Localization (M := R) S) Rₚ
this_3 : IsLocalization.AtPrime Rₚ p.asIdeal
this_4 : Module (Localization (M := R) S) Mₚ := compHom Mₚ (algebraMap (Localization (M := R) S) Rₚ)
this_5 : IsScalarTower R (Localization (M := R) S) Mₚ
this_6 : IsScalarTower (Localization (M := R) S) Rₚ Mₚ
l : LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
  (LocalizedModule p'.primeCompl M) :=
  LinearMap.extendScalarsOfIsLocalization S (Localization (M := R) S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
this_7 :
  IsLocalizedModule p'.primeCompl
    ((↑R :
        {S : Type uR} →
          {M M₂ : Type (max uM uR)} →
            [inst : Semiring R] →
              [inst_3 : Semiring S] →
                [inst_4 : AddCommMonoid M] →
                  [inst_5 : AddCommMonoid M₂] →
                    [inst_6 : Module R M] →
                      [inst_7 : Module R M₂] →
                        [inst_8 : Module S M] →
                          [inst_9 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      l)
this : IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization (M := R) S) p'.primeCompl) l
x : R
s : ↥S
hx : IsLocalization.mk' (Localization (M := R) S) x s ∈ p.asIdeal.primeCompl
H : x ∈ (↑p' : Set R)
⊢ HMul.hMul (α := Localization (M := R) S) (β := Localization (M := R) S)
      ((algebraMap R (Localization (M := R) S) : (a : R) → Localization S) x : Localization (M := R) S)
      (IsLocalization.mk' (Localization (M := R) S) 1 s : Localization (M := R) S) ∈
    (↑p.asIdeal : Set (Localization S))

Tactic:
Ideal.mul_mem_right _ _ H

Premises used: Set.Mem, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization (M := R) S)
p' : Ideal R := Ideal.comap (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this_1 : Algebra (Localization (M := R) S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization (M := R) S) Rₚ S p'.primeCompl hp'
this_2 : IsScalarTower R (Localization (M := R) S) Rₚ
this_3 : IsLocalization.AtPrime Rₚ p.asIdeal
this_4 : Module (Localization (M := R) S) Mₚ := compHom Mₚ (algebraMap (Localization (M := R) S) Rₚ)
this_5 : IsScalarTower R (Localization (M := R) S) Mₚ
this_6 : IsScalarTower (Localization (M := R) S) Rₚ Mₚ
l : LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
  (LocalizedModule p'.primeCompl M) :=
  LinearMap.extendScalarsOfIsLocalization S (Localization (M := R) S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
this_7 :
  IsLocalizedModule p'.primeCompl
    ((↑R :
        {S : Type uR} →
          {M M₂ : Type (max uM uR)} →
            [inst : Semiring R] →
              [inst_3 : Semiring S] →
                [inst_4 : AddCommMonoid M] →
                  [inst_5 : AddCommMonoid M₂] →
                    [inst_6 : Module R M] →
                      [inst_7 : Module R M₂] →
                        [inst_8 : Module S M] →
                          [inst_9 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      l)
this : IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization (M := R) S) p'.primeCompl) l
x : R
s : ↥S
hx : IsLocalization.mk' (Localization (M := R) S) x s ∈ p.asIdeal.primeCompl
H : x ∈ (↑p' : Set R)
⊢ HMul.hMul (α := Localization (M := R) S) (β := Localization (M := R) S)
      ((algebraMap R (Localization (M := R) S) : (a : R) → Localization S) x : Localization (M := R) S)
      (IsLocalization.mk' (Localization (M := R) S) 1 s : Localization (M := R) S) ∈
    (↑p.asIdeal : Set (Localization S))

Tactic:
exact Ideal.mul_mem_right _ _ H

Premises used: Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization (M := R) S)
p' : Ideal R := Ideal.comap (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this_1 : Algebra (Localization (M := R) S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization (M := R) S) Rₚ S p'.primeCompl hp'
this_2 : IsScalarTower R (Localization (M := R) S) Rₚ
this_3 : IsLocalization.AtPrime Rₚ p.asIdeal
this_4 : Module (Localization (M := R) S) Mₚ := compHom Mₚ (algebraMap (Localization (M := R) S) Rₚ)
this_5 : IsScalarTower R (Localization (M := R) S) Mₚ
this : IsScalarTower (Localization (M := R) S) Rₚ Mₚ
l : LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
  (LocalizedModule p'.primeCompl M) :=
  LinearMap.extendScalarsOfIsLocalization S (Localization (M := R) S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
⊢ IsLocalizedModule p.asIdeal.primeCompl l

Tactic:
have : IsLocalizedModule p.asIdeal.primeCompl l := by
    have : IsLocalizedModule p'.primeCompl (l.restrictScalars R) :=
      inferInstanceAs (IsLocalizedModule p'.primeCompl
        (IsLocalizedModule.liftOfLE _ _ hp' (LocalizedModule.mkLinearMap S M)
        (LocalizedModule.mkLinearMap p'.primeCompl M)))
    have : IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization S) p'.primeCompl) l :=
      IsLocalizedModule.of_restrictScalars p'.primeCompl ..
    apply IsLocalizedModule.of_exists_mul_mem
      (Algebra.algebraMapSubmonoid (Localization S) p'.primeCompl)
    · rintro _ ⟨x, hx, rfl⟩; exact hx
    · rintro ⟨x, hx⟩
      obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq S x
      refine ⟨algebraMap _ _ s.1, x, fun H ↦ hx ?_, by simp⟩
      rw [IsLocalization.mk'_eq_mul_mk'_one]
      exact Ideal.mul_mem_right _ _ H
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization (M := R) S)
p' : Ideal R := Ideal.comap (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this_1 : Algebra (Localization (M := R) S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization (M := R) S) Rₚ S p'.primeCompl hp'
this_2 : IsScalarTower R (Localization (M := R) S) Rₚ
this_3 : IsLocalization.AtPrime Rₚ p.asIdeal
this_4 : Module (Localization (M := R) S) Mₚ := compHom Mₚ (algebraMap (Localization (M := R) S) Rₚ)
this_5 : IsScalarTower R (Localization (M := R) S) Mₚ
this_6 : IsScalarTower (Localization (M := R) S) Rₚ Mₚ
l : LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
  (LocalizedModule p'.primeCompl M) :=
  LinearMap.extendScalarsOfIsLocalization S (Localization (M := R) S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
this : IsLocalizedModule p.asIdeal.primeCompl l
h :
  Free Rₚ Mₚ ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) (comap (algebraMap R (Localization (M := R) S)) p)
⊢ Membership.mem (γ := Set (PrimeSpectrum (Localization (M := R) S)))
      (freeLocus (Localization (M := R) S) (LocalizedModule S M)) p ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) (comap (algebraMap R (Localization (M := R) S)) p)

Tactic:
rw [mem_freeLocus_of_isLocalization (R := Localization S) p Rₚ Mₚ l]

Premises used: Module.mem_freeLocus_of_isLocalization
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization (M := R) S)
p' : Ideal R := Ideal.comap (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this_1 : Algebra (Localization (M := R) S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization (M := R) S) Rₚ S p'.primeCompl hp'
this_2 : IsScalarTower R (Localization (M := R) S) Rₚ
this_3 : IsLocalization.AtPrime Rₚ p.asIdeal
this_4 : Module (Localization (M := R) S) Mₚ := compHom Mₚ (algebraMap (Localization (M := R) S) Rₚ)
this_5 : IsScalarTower R (Localization (M := R) S) Mₚ
this_6 : IsScalarTower (Localization (M := R) S) Rₚ Mₚ
l : LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
  (LocalizedModule p'.primeCompl M) :=
  LinearMap.extendScalarsOfIsLocalization S (Localization (M := R) S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
this : IsLocalizedModule p.asIdeal.primeCompl l
⊢ Free Rₚ Mₚ ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) (comap (algebraMap R (Localization (M := R) S)) p)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FinitePresentation R M
simp_rw :
  (∀ (x : PrimeSpectrum R), Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)) ↔
    Projective R M
⊢ Eq (α := Set (PrimeSpectrum R)) (freeLocus R M) Set.univ ↔ Projective R M

Tactic:
simp_rw [Set.eq_univ_iff_forall, mem_freeLocus]

Premises used: Set.eq_univ_iff_forall, Module.mem_freeLocus
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FinitePresentation R M
⊢ (∀ (x : PrimeSpectrum R), Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)) ↔
    Projective R M

Tactic:
⟨fun H ↦ Module.projective_of_localization_maximal fun I hI ↦
    have := H ⟨I, hI.isPrime⟩; .of_free, fun H x ↦ Module.free_of_flat_of_isLocalRing⟩

Premises used: PrimeSpectrum.mk, Ideal.IsMaximal.isPrime, Module.Projective.of_free, Iff.intro, Module.projective_of_localization_maximal, Module.free_of_flat_of_isLocalRing
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FinitePresentation R M
⊢ (∀ (x : PrimeSpectrum R), Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)) ↔
    Projective R M

Tactic:
exact ⟨fun H ↦ Module.projective_of_localization_maximal fun I hI ↦
    have := H ⟨I, hI.isPrime⟩; .of_free, fun H x ↦ Module.free_of_flat_of_isLocalRing⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Flat R M
simp_rw : ∀ (x : PrimeSpectrum R), Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
⊢ Eq (α := Set (PrimeSpectrum R)) (freeLocus R M) Set.univ

Tactic:
simp_rw [Set.eq_univ_iff_forall, mem_freeLocus]

Premises used: Set.eq_univ_iff_forall, Module.mem_freeLocus
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Flat R M
⊢ ∀ (x : PrimeSpectrum R), Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)

Tactic:
fun x ↦ Module.free_of_flat_of_isLocalRing

Premises used: Module.free_of_flat_of_isLocalRing
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Flat R M
⊢ ∀ (x : PrimeSpectrum R), Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)

Tactic:
exact fun x ↦ Module.free_of_flat_of_isLocalRing

Premises used: Module.free_of_flat_of_isLocalRing
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FinitePresentation R M
f : R
rw :
  (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔
    Eq.{uR + 1} (α := Set (PrimeSpectrum (Localization.Away f)))
      (freeLocus (Localization.Away f) (LocalizedModule.Away f M)) Set.univ
rw₁ :
  (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔
    Eq (α := Set (PrimeSpectrum (Localization.Away f)))
      (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R (Localization (Submonoid.powers f)))) (freeLocus R M))
      Set.univ
rw₂ :
  (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔
    Subset (α := Set (PrimeSpectrum R))
      (Set.range (ι := PrimeSpectrum (Localization (Submonoid.powers f)))
        (comap (algebraMap R (Localization (Submonoid.powers f)))))
      (freeLocus R M)
rw₃ rw₄ :
  (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔ (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M
⊢ (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔ Projective (Localization.Away f) (LocalizedModule.Away f M)

Tactic:
rw [← freeLocus_eq_univ_iff, freeLocus_localization,
    Set.preimage_eq_univ_iff, localization_away_comap_range _ f]

Premises used: Module.freeLocus_localization, Set.preimage_eq_univ_iff, Module.freeLocus_eq_univ_iff, PrimeSpectrum.localization_away_comap_range
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FinitePresentation R M
⊢ IsOpen (X := PrimeSpectrum R) (freeLocus R M)

Tactic:
isOpen_iff_forall_mem_open.mpr fun x hx ↦ ?_

Premises used: Iff.mpr, isOpen_iff_forall_mem_open
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FinitePresentation R M
refine :
  ∀ (x : PrimeSpectrum R) (hx : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x),
    ∃ t ⊆ freeLocus R M, IsOpen t ∧ x ∈ t
⊢ IsOpen (X := PrimeSpectrum R) (freeLocus R M)

Tactic:
refine isOpen_iff_forall_mem_open.mpr fun x hx ↦ ?_

Premises used: Iff.mpr, isOpen_iff_forall_mem_open
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FinitePresentation R M
x : PrimeSpectrum R
hx : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x
⊢ Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)

Tactic:
have : Module.Free _ _ := hx
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FinitePresentation R M
x : PrimeSpectrum R
hx : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x
this : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
obtain :
  ∀ (r : R) (hr : r ∈ x.asIdeal.primeCompl) (hr' : Free (Localization (Submonoid.powers r)) (LocalizedModule.Away r M)),
    finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) =
        finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M) →
      ∃ t ⊆ freeLocus R M, IsOpen t ∧ x ∈ t
⊢ ∃ t ⊆ freeLocus R M, IsOpen t ∧ x ∈ t

Tactic:
obtain ⟨r, hr, hr', _⟩ := Module.FinitePresentation.exists_free_localizedModule_powers
    x.asIdeal.primeCompl (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
    (Localization.AtPrime x.asIdeal)

Premises used: Localization.AtPrime, Module.FinitePresentation.exists_free_localizedModule_powers, LocalizedModule.mkLinearMap, Ideal.primeCompl, PrimeSpectrum.asIdeal