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
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ₚ
⊢ (r • r') • m =
    HSMul.hSMul (α := Rₚ) ((algebraMap (Localization (M := R) S) Rₚ : (a : Localization S) → Rₚ) r : Rₚ) (r' • m)
have rw : (r • r') • m = HMul.hMul (α := Rₚ) ((algebraMap (Localization (M := R) S) Rₚ : (a : Localization S) → Rₚ) r : Rₚ) r' • m
Tactic: rw [← mul_smul, ← Algebra.smul_def]
-- 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_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
⊢ (r • r') • m =
    HSMul.hSMul (α := Rₚ) ((algebraMap (Localization (M := R) S) Rₚ : (a : Localization S) → Rₚ) r : Rₚ) (r' • m)
have rw₁ : (r • r') • m = (r • r') • m
Tactic: rw [← mul_smul, ← Algebra.smul_def]
-- 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_4 : Module (Localization (M := R) S) Mₚ := compHom Mₚ (algebraMap (Localization (M := R) S) Rₚ)
this : IsScalarTower R (Localization (M := R) S) Mₚ
⊢ 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 (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]⟩
-- 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_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
have 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)
Tactic: have : IsLocalizedModule p'.primeCompl (l.restrictScalars R) :=
      inferInstanceAs (IsLocalizedModule p'.primeCompl
        (IsLocalizedModule.liftOfLE _ _ hp' (LocalizedModule.mkLinearMap S M)
        (LocalizedModule.mkLinearMap p'.primeCompl M)))
-- 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_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 p.asIdeal.primeCompl l
have this₁ : 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 ..
-- 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_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
⊢ IsLocalizedModule p.asIdeal.primeCompl l
have h : Algebra.algebraMapSubmonoid (Localization (M := R) S) p'.primeCompl ≤ p.asIdeal.primeCompl
Tactic: apply IsLocalizedModule.of_exists_mul_mem
      (Algebra.algebraMapSubmonoid (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_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
⊢ IsLocalizedModule p.asIdeal.primeCompl l
have 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))
Tactic: apply IsLocalizedModule.of_exists_mul_mem
      (Algebra.algebraMapSubmonoid (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_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
⊢ ∃ (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))
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))
      (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: 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_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
⊢ ∃ (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))
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_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)
⊢ 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_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))
⊢ 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₁ : 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