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 :
  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)
⊢ 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 :
  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)
⊢ 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 : IsScalarTower R (Localization (M := R) S) Rₚ
⊢ IsLocalization.AtPrime Rₚ p.asIdeal

Tactic:
have : IsLocalization.AtPrime Rₚ p.asIdeal := by
    have := IsLocalization.isLocalization_of_submonoid_le (Localization S) Rₚ _ _ hp'
    apply IsLocalization.isLocalization_of_is_exists_mul_mem _
      (Submonoid.map (algebraMap R (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 : Module (Localization (M := R) S) Mₚ := compHom Mₚ (algebraMap (Localization (M := R) S) Rₚ)
r : R
r' : Localization (M := R) S
m : Mₚ
simp :
  r •
      HSMul.hSMul (α :=
        Localization.AtPrime
          (Ideal.comap (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p.asIdeal))
        ((algebraMap (Localization (M := R) S)
                (Localization.AtPrime
                  (Ideal.comap (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S))
                    p.asIdeal)) :
              (a : Localization S) → Localization.AtPrime (Ideal.comap (algebraMap R (Localization S)) p.asIdeal))
            r' :
          Localization.AtPrime
            (Ideal.comap (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p.asIdeal))
        m =
    r • r' • m
⊢ HSMul.hSMul (α := Rₚ) ((algebraMap (Localization (M := R) S) Rₚ : (a : Localization S) → Rₚ) (r • r') : Rₚ) m =
    r • r' • m

Tactic:
simp [p', Rₚ, Mₚ, Algebra.smul_def, ← IsScalarTower.algebraMap_apply, mul_smul]

Premises used: Algebra.smul_def, IsScalarTower.algebraMap_apply, SemigroupAction.mul_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
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 : Module (Localization (M := R) S) Mₚ := compHom Mₚ (algebraMap (Localization (M := R) S) Rₚ)
r : R
r' : Localization (M := R) S
m : Mₚ
⊢ r •
      HSMul.hSMul (α :=
        Localization.AtPrime
          (Ideal.comap (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p.asIdeal))
        ((algebraMap (Localization (M := R) S)
                (Localization.AtPrime
                  (Ideal.comap (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S))
                    p.asIdeal)) :
              (a : Localization S) → Localization.AtPrime (Ideal.comap (algebraMap R (Localization S)) p.asIdeal))
            r' :
          Localization.AtPrime
            (Ideal.comap (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p.asIdeal))
        m =
    r • r' • m

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
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 : Module (Localization (M := R) S) Mₚ := compHom Mₚ (algebraMap (Localization (M := R) S) Rₚ)
⊢ IsScalarTower R (Localization (M := R) S) Mₚ

Tactic:
have : IsScalarTower R (Localization S) Mₚ :=
    ⟨fun r r' m ↦ show algebraMap _ Rₚ (r • r') • m = _ by
      simp [p', Rₚ, Mₚ, Algebra.smul_def, ← IsScalarTower.algebraMap_apply, mul_smul]; 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
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 : IsScalarTower R (Localization (M := R) S) Mₚ
r : Localization (M := R) S
r' : Rₚ
m : Mₚ
rw :
  (r • r') • m =
    HMul.hMul (α := Rₚ) ((algebraMap (Localization (M := R) S) Rₚ : (a : Localization S) → Rₚ) r : Rₚ) r' • m
rw₁ rw₂ : (r • r') • m = (r • r') • m
⊢ (r • r') • m =
    HSMul.hSMul (α := Rₚ) ((algebraMap (Localization (M := R) S) Rₚ : (a : Localization S) → Rₚ) r : Rₚ) (r' • m)

Tactic:
rw [← mul_smul, ← Algebra.smul_def]

Premises used: Algebra.smul_def, SemigroupAction.mul_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
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 : IsScalarTower R (Localization (M := R) S) Mₚ
⊢ IsScalarTower (Localization (M := R) S) Rₚ Mₚ

Tactic:
have : IsScalarTower (Localization S) Rₚ Mₚ :=
    ⟨fun r r' m ↦ show _ = algebraMap _ Rₚ r • r' • m by rw [← mul_smul, ← Algebra.smul_def]⟩
-- 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'.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)

Tactic:
have : IsLocalizedModule p'.primeCompl (l.restrictScalars R) :=
      inferInstanceAs (IsLocalizedModule p'.primeCompl
        (IsLocalizedModule.liftOfLE _ _ hp' (LocalizedModule.mkLinearMap S M)
        (LocalizedModule.mkLinearMap p'.primeCompl M)))
-- 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'.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)
⊢ IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization (M := R) S) p'.primeCompl) l

Tactic:
have : IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization S) p'.primeCompl) l :=
      IsLocalizedModule.of_restrictScalars p'.primeCompl ..
-- 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
h : Algebra.algebraMapSubmonoid (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))
        (Algebra.algebraMapSubmonoid (Localization (M := R) S) p'.primeCompl) (m * (↑x : Localization S))
⊢ IsLocalizedModule p.asIdeal.primeCompl l

Tactic:
apply IsLocalizedModule.of_exists_mul_mem
      (Algebra.algebraMapSubmonoid (Localization S) p'.primeCompl)

Premises used: Localization, IsLocalizedModule.of_exists_mul_mem, Ideal.primeCompl, Algebra.algebraMapSubmonoid
-- 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
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_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
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_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 : 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))
        (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))
⊢ ∃ (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) x hx) : Localization S))

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

Premises used: rfl, IsLocalization.exists_mk'_eq