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
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst_3 : CommRing Rₚ
inst_4 : Algebra R Rₚ
inst_5 : IsLocalization.AtPrime Rₚ p.asIdeal
inst_6 : AddCommGroup Mₚ
inst_7 : Module R Mₚ
f : M →ₗ[R] Mₚ
inst_8 : IsLocalizedModule p.asIdeal.primeCompl f
inst_9 : Module Rₚ Mₚ
inst_10 : IsScalarTower R Rₚ Mₚ
e : RingEquiv.{uR, u_1} (Localization.AtPrime p.asIdeal) Rₚ :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ)
x : LocalizedModule p.asIdeal.primeCompl M
r : R
s : ↥p.asIdeal.primeCompl
a :
  HSMul.hSMul (β := Mₚ) (↑s : R)
      ((IsLocalizedModule.iso p.asIdeal.primeCompl f : (a : LocalizedModule p.asIdeal.primeCompl M) → Mₚ)
          (HSMul.hSMul (α := Localization.AtPrime p.asIdeal) (IsLocalization.mk' (Localization.AtPrime p.asIdeal) r s)
            x) :
        Mₚ) =
    (↑s : R) •
      HSMul.hSMul (β := Mₚ) (IsLocalization.mk' Rₚ r s)
        ((IsLocalizedModule.iso p.asIdeal.primeCompl f : (a : LocalizedModule p.asIdeal.primeCompl M) → Mₚ) x : Mₚ)
⊢ Eq (α := Mₚ)
    ((((algebraMap R (End R Mₚ) : (a : R) → End R Mₚ) (↑s : R) : End R Mₚ) : (a : Mₚ) → Mₚ)
        ((↑(IsLocalizedModule.iso p.asIdeal.primeCompl f) : LocalizedModule p.asIdeal.primeCompl M →ₗ[R] Mₚ).toFun
          (HSMul.hSMul (α := Localization.AtPrime p.asIdeal) (IsLocalization.mk' (Localization.AtPrime p.asIdeal) r s)
            x)) :
      Mₚ)
    ((((algebraMap R (End R Mₚ) : (a : R) → End R Mₚ) (↑s : R) : End R Mₚ) : (a : Mₚ) → Mₚ)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := Rₚ)
          (((↑e : Localization.AtPrime p.asIdeal →+* Rₚ) : (a : Localization.AtPrime p.asIdeal) → Rₚ)
              (IsLocalization.mk' (Localization.AtPrime p.asIdeal) r s) :
            Rₚ)
          ((↑(IsLocalizedModule.iso p.asIdeal.primeCompl f) : LocalizedModule p.asIdeal.primeCompl M →ₗ[R] Mₚ).toFun
            x)) :
      Mₚ)

Tactic:
simp only [e, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe,
    algebraMap_end_apply,
    AlgEquiv.toRingEquiv_toRingHom, RingHom.coe_coe, IsLocalization.algEquiv_apply,
    IsLocalization.map_id_mk']

Premises used: AlgEquiv.toRingEquiv_toRingHom, IsLocalization.algEquiv_apply, RingHom.coe_coe, AddHom.toFun_eq_coe, Module.algebraMap_end_apply, LinearMap.coe_toAddHom, IsLocalization.map_id_mk', LinearEquiv.coe_coe
-- 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
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst_3 : CommRing Rₚ
inst_4 : Algebra R Rₚ
inst_5 : IsLocalization.AtPrime Rₚ p.asIdeal
inst_6 : AddCommGroup Mₚ
inst_7 : Module R Mₚ
f : M →ₗ[R] Mₚ
inst_8 : IsLocalizedModule p.asIdeal.primeCompl f
inst_9 : Module Rₚ Mₚ
inst_10 : IsScalarTower R Rₚ Mₚ
e : RingEquiv.{uR, u_1} (Localization.AtPrime p.asIdeal) Rₚ :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ)
x : LocalizedModule p.asIdeal.primeCompl M
r : R
s : ↥p.asIdeal.primeCompl
⊢ HSMul.hSMul (β := Mₚ) (↑s : R)
      ((IsLocalizedModule.iso p.asIdeal.primeCompl f : (a : LocalizedModule p.asIdeal.primeCompl M) → Mₚ)
          (HSMul.hSMul (α := Localization.AtPrime p.asIdeal) (IsLocalization.mk' (Localization.AtPrime p.asIdeal) r s)
            x) :
        Mₚ) =
    (↑s : R) •
      HSMul.hSMul (β := Mₚ) (IsLocalization.mk' Rₚ r s)
        ((IsLocalizedModule.iso p.asIdeal.primeCompl f : (a : LocalizedModule p.asIdeal.primeCompl M) → Mₚ) x : Mₚ)

Tactic:
simp only [← map_smul, ← smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul]

Premises used: smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul, map_smul
-- 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
p : PrimeSpectrum R
Rₚ : Type u_1
inst_3 : CommRing Rₚ
inst_4 : Algebra R Rₚ
inst_5 : IsLocalization.AtPrime Rₚ p.asIdeal
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) p ↔ Free Rₚ (Rₚ ⊗[R] M)

Tactic:
mem_freeLocus_of_isLocalization p Rₚ (f := TensorProduct.mk R Rₚ M 1)

Premises used: Module.mem_freeLocus_of_isLocalization, OfNat.ofNat, DFunLike.coe, TensorProduct.mk
-- 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
p : PrimeSpectrum R
Rₚ : Type u_1
inst_3 : CommRing Rₚ
inst_4 : Algebra R Rₚ
inst_5 : IsLocalization.AtPrime Rₚ p.asIdeal
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) p ↔ Free Rₚ (Rₚ ⊗[R] M)

Tactic:
exact mem_freeLocus_of_isLocalization p Rₚ (f := TensorProduct.mk R Rₚ M 1)

Premises used: Module.mem_freeLocus_of_isLocalization, OfNat.ofNat, DFunLike.coe, TensorProduct.mk
-- 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
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
e : M ≃ₗ[R] M'
h :
  ∀ (p : PrimeSpectrum R),
    Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) p ↔
      Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M') p
⊢ Eq (α := Set (PrimeSpectrum R)) (freeLocus R M) (freeLocus R M')

Tactic:
ext p
-- 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
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
e : M ≃ₗ[R] M'
p : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) p ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M') p

Tactic:
mem_freeLocus_of_isLocalization _ _ _
    (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M' ∘ₗ e.toLinearMap)

Premises used: Set.Mem, setOf, Module.freeLocus, LinearMap.comp, LinearEquiv.toLinearMap, LocalizedModule.mkLinearMap, Module.mem_freeLocus_of_isLocalization, Ideal.primeCompl, PrimeSpectrum.asIdeal
-- 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
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
e : M ≃ₗ[R] M'
p : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) p ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M') p

Tactic:
exact mem_freeLocus_of_isLocalization _ _ _
    (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M' ∘ₗ e.toLinearMap)

Premises used: LinearMap.comp, LinearEquiv.toLinearMap, LocalizedModule.mkLinearMap, Module.mem_freeLocus_of_isLocalization, Ideal.primeCompl, PrimeSpectrum.asIdeal
-- 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
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
p : PrimeSpectrum A
hp :
  Membership.mem (γ := Set (PrimeSpectrum A))
    (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R A)) (freeLocus R M)) p
Rₚ : Type uR := Localization.AtPrime (asIdeal (comap (algebraMap R A) p))
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
⊢ let Rₚ := Localization.AtPrime (asIdeal (comap (algebraMap R A) p));
  Free Rₚ (Rₚ ⊗[R] M)

Tactic:
rw [Set.mem_preimage, mem_freeLocus_iff_tensor _ Rₚ] at hp

Premises used: Module.mem_freeLocus_iff_tensor, Set.mem_preimage
-- 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
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
p : PrimeSpectrum A
Rₚ : Type uR := Localization.AtPrime (asIdeal (comap (algebraMap R A) p))
hp : Free Rₚ (Rₚ ⊗[R] M)
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
rw : Free Aₚ (Aₚ ⊗[A] (A ⊗[R] M))
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (freeLocus A (A ⊗[R] M)) p

Tactic:
rw [mem_freeLocus_iff_tensor _ Aₚ]

Premises used: Module.mem_freeLocus_iff_tensor
-- 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
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
p : PrimeSpectrum A
Rₚ : Type uR := Localization.AtPrime (asIdeal (comap (algebraMap R A) p))
hp : Free Rₚ (Rₚ ⊗[R] M)
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
algebra : Algebra Rₚ Aₚ :=
  RingHom.toAlgebra (Localization.localRingHom (asIdeal (comap (algebraMap R A) p)) p.asIdeal (algebraMap R A) ⋯)
⊢ Eq (α := R →+* Aₚ) (algebraMap R Aₚ) (RingHom.comp (algebraMap Rₚ Aₚ) (algebraMap R Rₚ))

Tactic:
simp [Rₚ, Aₚ, algebra, RingHom.algebraMap_toAlgebra, Localization.localRingHom,
        ← IsScalarTower.algebraMap_eq]

Premises used: Localization.localRingHom, IsScalarTower.algebraMap_eq, RingHom.algebraMap_toAlgebra
-- 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
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
p : PrimeSpectrum A
Rₚ : Type uR := Localization.AtPrime (asIdeal (comap (algebraMap R A) p))
hp : Free Rₚ (Rₚ ⊗[R] M)
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
algebra : Algebra Rₚ Aₚ :=
  RingHom.toAlgebra (Localization.localRingHom (asIdeal (comap (algebraMap R A) p)) p.asIdeal (algebraMap R A) ⋯)
⊢ IsScalarTower R Rₚ Aₚ

Tactic:
have : IsScalarTower R Rₚ Aₚ := IsScalarTower.of_algebraMap_eq'
    (by simp [Rₚ, Aₚ, algebra, RingHom.algebraMap_toAlgebra, Localization.localRingHom,
        ← IsScalarTower.algebraMap_eq])
-- 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
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
p : PrimeSpectrum A
Rₚ : Type uR := Localization.AtPrime (asIdeal (comap (algebraMap R A) p))
hp : Free Rₚ (Rₚ ⊗[R] M)
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
algebra : Algebra Rₚ Aₚ :=
  RingHom.toAlgebra (Localization.localRingHom (asIdeal (comap (algebraMap R A) p)) p.asIdeal (algebraMap R A) ⋯)
this : IsScalarTower R Rₚ Aₚ
e : Aₚ ⊗[Rₚ] (Rₚ ⊗[R] M) ≃ₗ[Aₚ] Aₚ ⊗[A] (A ⊗[R] M) :=
  (AlgebraTensorModule.cancelBaseChange R Rₚ Aₚ Aₚ M : Aₚ ⊗[Rₚ] (Rₚ ⊗[R] M) ≃ₗ[Aₚ] Aₚ ⊗[R] M) ≪≫ₗ
    (LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R A Aₚ Aₚ M) : Aₚ ⊗[R] M ≃ₗ[Aₚ] Aₚ ⊗[A] (A ⊗[R] M))
⊢ Free Aₚ (Aₚ ⊗[A] (A ⊗[R] M))

Tactic:
.of_equiv e

Premises used: Module.Free.of_equiv
-- 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
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra R A
p : PrimeSpectrum A
Rₚ : Type uR := Localization.AtPrime (asIdeal (comap (algebraMap R A) p))
hp : Free Rₚ (Rₚ ⊗[R] M)
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
algebra : Algebra Rₚ Aₚ :=
  RingHom.toAlgebra (Localization.localRingHom (asIdeal (comap (algebraMap R A) p)) p.asIdeal (algebraMap R A) ⋯)
this : IsScalarTower R Rₚ Aₚ
e : Aₚ ⊗[Rₚ] (Rₚ ⊗[R] M) ≃ₗ[Aₚ] Aₚ ⊗[A] (A ⊗[R] M) :=
  (AlgebraTensorModule.cancelBaseChange R Rₚ Aₚ Aₚ M : Aₚ ⊗[Rₚ] (Rₚ ⊗[R] M) ≃ₗ[Aₚ] Aₚ ⊗[R] M) ≪≫ₗ
    (LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R A Aₚ Aₚ M) : Aₚ ⊗[R] M ≃ₗ[Aₚ] Aₚ ⊗[A] (A ⊗[R] M))
⊢ Free Aₚ (Aₚ ⊗[A] (A ⊗[R] M))

Tactic:
exact .of_equiv e
-- 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
h :
  ∀ (p : PrimeSpectrum (Localization (M := R) S)),
    Membership.mem (γ := Set (PrimeSpectrum (Localization (M := R) S)))
        (freeLocus (Localization (M := R) S) (LocalizedModule S M)) p ↔
      Membership.mem (γ := Set (PrimeSpectrum (Localization (M := R) S)))
        (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R (Localization (M := R) S))) (freeLocus R M)) p
⊢ Eq (α := Set (PrimeSpectrum (Localization (M := R) S))) (freeLocus (Localization (M := R) S) (LocalizedModule S M))
    (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R (Localization (M := R) S))) (freeLocus R M))

Tactic:
ext p
-- 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
⊢ S ≤ p'.primeCompl

Tactic:
have hp' : S ≤ p'.primeCompl := fun x hx H ↦
    p.isPrime.ne_top (Ideal.eq_top_of_isUnit_mem _ H (IsLocalization.map_units _ ⟨x, 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
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 : Algebra (Localization (M := R) S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization (M := R) S) Rₚ S p'.primeCompl hp'
⊢ IsScalarTower R (Localization (M := R) S) Rₚ

Tactic:
have : IsScalarTower R (Localization S) Rₚ :=
    IsLocalization.localization_isScalarTower_of_submonoid_le ..
-- 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 : IsScalarTower R (Localization (M := R) S) Rₚ
⊢ IsLocalization
    (Submonoid.map (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p'.primeCompl) Rₚ

Tactic:
have := IsLocalization.isLocalization_of_submonoid_le (Localization S) Rₚ _ _ hp'
-- 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 :
  IsLocalization
    (Submonoid.map (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p'.primeCompl) Rₚ
h :
  Submonoid.map (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p'.primeCompl ≤
    p.asIdeal.primeCompl
h' :
  ∀ (x : ↥p.asIdeal.primeCompl),
    ∃ (m : Localization (M := R) S),
      Membership.mem (γ := Submonoid (Localization (M := R) S))
        (Submonoid.map (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p'.primeCompl)
        (m * (↑x : Localization S))
⊢ IsLocalization.AtPrime Rₚ p.asIdeal

Tactic:
apply IsLocalization.isLocalization_of_is_exists_mul_mem _
      (Submonoid.map (algebraMap R (Localization S)) p'.primeCompl)

Premises used: Algebra.algebraMap, Localization, Submonoid.map, Ideal.primeCompl, IsLocalization.isLocalization_of_is_exists_mul_mem
-- 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 :
  IsLocalization
    (Submonoid.map (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p'.primeCompl) Rₚ
x : R
hx : x ∈ (↑p'.primeCompl : Set R)
⊢ Membership.mem (α := Localization (M := R) S) p.asIdeal.primeCompl
    ((algebraMap R (Localization (M := R) S) : (a : R) → Localization S) x : Localization (M := R) S)

Tactic:
hx

Premises used: Set.Mem, setOf, Set.preimage
-- 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 :
  IsLocalization
    (Submonoid.map (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p'.primeCompl) Rₚ
x : R
hx : x ∈ (↑p'.primeCompl : Set R)
⊢ Membership.mem (α := Localization (M := R) S) p.asIdeal.primeCompl
    ((algebraMap R (Localization (M := R) S) : (a : R) → Localization S) x : Localization (M := R) S)

Tactic:
exact 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
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 :
  IsLocalization
    (Submonoid.map (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p'.primeCompl) Rₚ
x : Localization (M := R) S
hx : x ∈ p.asIdeal.primeCompl
h' :
  ∀ (x : R) (s : ↥S) (hx : IsLocalization.mk' (Localization (M := R) S) x s ∈ p.asIdeal.primeCompl),
    ∃ (m : Localization (M := R) S),
      Membership.mem (γ := Submonoid (Localization (M := R) S))
        (Submonoid.map (F := R →+* Localization (M := R) S) (algebraMap R (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))
⊢ ∃ (m : Localization (M := R) S),
    Membership.mem (γ := Submonoid (Localization (M := R) S))
      (Submonoid.map (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p'.primeCompl)
      (m * (↑(Subtype.mk (p := fun (x : Localization (M := R) S) ↦ x ∈ p.asIdeal.primeCompl) x hx) : Localization S))

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq S x

Premises used: rfl, IsLocalization.exists_mk'_eq
-- 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 :
  IsLocalization
    (Submonoid.map (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p'.primeCompl) Rₚ
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 :
  IsLocalization
    (Submonoid.map (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p'.primeCompl) Rₚ
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))
      (Submonoid.map (F := R →+* Localization (M := R) S) (algebraMap R (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 :
  IsLocalization
    (Submonoid.map (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p'.primeCompl) Rₚ
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