awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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ₚ)
r : Localization.AtPrime p.asIdeal
x : LocalizedModule p.asIdeal.primeCompl M
⊢ (↑(IsLocalizedModule.iso p.asIdeal.primeCompl f) : LocalizedModule p.asIdeal.primeCompl M →ₗ[R] Mₚ).toFun (r • x) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := Rₚ)
      (((↑e : Localization.AtPrime p.asIdeal →+* Rₚ) : (a : Localization.AtPrime p.asIdeal) → Rₚ) r : Rₚ)
      ((↑(IsLocalizedModule.iso p.asIdeal.primeCompl f) : LocalizedModule p.asIdeal.primeCompl M →ₗ[R] Mₚ).toFun x)
have obtain : ∀ (r : R) (s : ↥p.asIdeal.primeCompl),
  (↑(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) =
    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)
Tactic: obtain ⟨r, s, rfl⟩ := IsLocalization.exists_mk'_eq p.asIdeal.primeCompl r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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
⊢ (↑(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) =
    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)
have a : 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: apply ((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units f s)).1
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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
⊢ 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ₚ)
have 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ₚ)
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']
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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'
⊢ Eq (α := Set (PrimeSpectrum R)) (freeLocus R M) (freeLocus R M')
have h : ∀ (p : PrimeSpectrum R),
  Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) p ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M') p
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (hypothesis)
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
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (freeLocus A (A ⊗[R] M)) p
have hp₁ : 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
Cleared hypotheses: hp, Rₚ, Aₚ
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (freeLocus A (A ⊗[R] M)) p
have rw : Free Aₚ (Aₚ ⊗[A] (A ⊗[R] M))
Tactic: rw [mem_freeLocus_iff_tensor _ Aₚ]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (hypothesis)
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) ⋯)
⊢ Free Aₚ (Aₚ ⊗[A] (A ⊗[R] M))
have this : 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])
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
⊢ 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))
have 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
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (hypothesis)
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
⊢ 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)
have hp' : 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⟩))
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (hypothesis)
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'
⊢ 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)
have this₁ : IsScalarTower R (Localization (M := R) S) Rₚ
Tactic: have : IsScalarTower R (Localization S) Rₚ :=
    IsLocalization.localization_isScalarTower_of_submonoid_le ..
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (hypothesis)
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
have this₁ : 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'
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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ₚ
⊢ IsLocalization.AtPrime Rₚ p.asIdeal
have h : Submonoid.map (F := R →+* Localization (M := R) S) (algebraMap R (Localization (M := R) S)) p'.primeCompl ≤
  p.asIdeal.primeCompl
Tactic: apply IsLocalization.isLocalization_of_is_exists_mul_mem _
      (Submonoid.map (algebraMap R (Localization S)) p'.primeCompl)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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
⊢ IsLocalization.AtPrime Rₚ p.asIdeal
have 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))
Tactic: apply IsLocalization.isLocalization_of_is_exists_mul_mem _
      (Submonoid.map (algebraMap R (Localization S)) p'.primeCompl)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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
⊢ ∃ (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))
have 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))
Tactic: obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq S x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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
⊢ ∃ (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))
have h' : ∀ (H : x ∈ (↑p' : Set R)), IsLocalization.mk' (Localization (M := R) S) x s ∈ (↑p.asIdeal : Set (Localization S))
Tactic: refine ⟨algebraMap _ _ s.1, x, fun H ↦ hx ?_, by simp⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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)
⊢ IsLocalization.mk' (Localization (M := R) S) x s ∈ (↑p.asIdeal : Set (Localization S))
have 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))
Tactic: rw [IsLocalization.mk'_eq_mul_mk'_one]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (hypothesis)
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ₚ
⊢ 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)
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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ₚ
⊢ HSMul.hSMul (α := Rₚ) ((algebraMap (Localization (M := R) S) Rₚ : (a : Localization S) → Rₚ) (r • r') : Rₚ) m =
    r • r' • m
have 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
Tactic: simp [p', Rₚ, Mₚ, Algebra.smul_def, ← IsScalarTower.algebraMap_apply, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (hypothesis)
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ₚ)
⊢ 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)
have this₁ : 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⟩