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_5 : IsScalarTower R (Localization (M := R) S) Mₚ
this_6 : IsScalarTower (Localization (M := R) S) Rₚ Mₚ
l : LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
  (LocalizedModule p'.primeCompl M) :=
  LinearMap.extendScalarsOfIsLocalization S (Localization (M := R) S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
this : IsLocalizedModule p.asIdeal.primeCompl l
⊢ 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 h : Free Rₚ Mₚ ↔
  Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) (comap (algebraMap R (Localization (M := R) S)) p)
Tactic: rw [mem_freeLocus_of_isLocalization (R := Localization S) p Rₚ Mₚ l]
-- 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
inst_3 : FinitePresentation R M
⊢ Eq (α := Set (PrimeSpectrum R)) (freeLocus R M) Set.univ ↔ Projective R M
have simp_rw : (∀ (x : PrimeSpectrum R), Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)) ↔
  Projective R M
Tactic: simp_rw [Set.eq_univ_iff_forall, mem_freeLocus]
-- 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
inst_3 : Module.Finite R M
inst_4 : Flat R M
⊢ Eq (α := Set (PrimeSpectrum R)) (freeLocus R M) Set.univ
have simp_rw : ∀ (x : PrimeSpectrum R), Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
Tactic: simp_rw [Set.eq_univ_iff_forall, mem_freeLocus]
-- 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
inst_3 : FinitePresentation R M
f : R
⊢ (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔ Projective (Localization.Away f) (LocalizedModule.Away f M)
have rw : (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔
  Eq.{uR + 1} (α := Set (PrimeSpectrum (Localization.Away f)))
    (freeLocus (Localization.Away f) (LocalizedModule.Away f M)) Set.univ
Tactic: rw [← freeLocus_eq_univ_iff, freeLocus_localization,
    Set.preimage_eq_univ_iff, localization_away_comap_range _ f]
-- 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
inst_3 : FinitePresentation R M
f : R
rw :
  (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔
    Eq.{uR + 1} (α := Set (PrimeSpectrum (Localization.Away f)))
      (freeLocus (Localization.Away f) (LocalizedModule.Away f M)) Set.univ
⊢ (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔ Projective (Localization.Away f) (LocalizedModule.Away f M)
have rw₁ : (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔
  Eq (α := Set (PrimeSpectrum (Localization.Away f)))
    (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R (Localization (Submonoid.powers f)))) (freeLocus R M))
    Set.univ
Tactic: rw [← freeLocus_eq_univ_iff, freeLocus_localization,
    Set.preimage_eq_univ_iff, localization_away_comap_range _ f]
-- 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
inst_3 : FinitePresentation R M
f : R
rw :
  (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔
    Eq.{uR + 1} (α := Set (PrimeSpectrum (Localization.Away f)))
      (freeLocus (Localization.Away f) (LocalizedModule.Away f M)) Set.univ
rw₁ :
  (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔
    Eq (α := Set (PrimeSpectrum (Localization.Away f)))
      (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R (Localization (Submonoid.powers f)))) (freeLocus R M))
      Set.univ
⊢ (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔ Projective (Localization.Away f) (LocalizedModule.Away f M)
have rw₂ : (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔
  Subset (α := Set (PrimeSpectrum R))
    (Set.range (ι := PrimeSpectrum (Localization (Submonoid.powers f)))
      (comap (algebraMap R (Localization (Submonoid.powers f)))))
    (freeLocus R M)
Tactic: rw [← freeLocus_eq_univ_iff, freeLocus_localization,
    Set.preimage_eq_univ_iff, localization_away_comap_range _ f]
-- 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
inst_3 : FinitePresentation R M
f : R
rw :
  (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔
    Eq.{uR + 1} (α := Set (PrimeSpectrum (Localization.Away f)))
      (freeLocus (Localization.Away f) (LocalizedModule.Away f M)) Set.univ
rw₁ :
  (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔
    Eq (α := Set (PrimeSpectrum (Localization.Away f)))
      (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R (Localization (Submonoid.powers f)))) (freeLocus R M))
      Set.univ
rw₂ :
  (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔
    Subset (α := Set (PrimeSpectrum R))
      (Set.range (ι := PrimeSpectrum (Localization (Submonoid.powers f)))
        (comap (algebraMap R (Localization (Submonoid.powers f)))))
      (freeLocus R M)
⊢ (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔ Projective (Localization.Away f) (LocalizedModule.Away f M)
have rw₃ : (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔ (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ freeLocus R M
Tactic: rw [← freeLocus_eq_univ_iff, freeLocus_localization,
    Set.preimage_eq_univ_iff, localization_away_comap_range _ f]
-- 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
inst_3 : FinitePresentation R M
⊢ IsOpen (X := PrimeSpectrum R) (freeLocus R M)
have refine : ∀ (x : PrimeSpectrum R) (hx : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x),
  ∃ t ⊆ freeLocus R M, IsOpen t ∧ x ∈ t
Tactic: refine isOpen_iff_forall_mem_open.mpr fun 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
inst_3 : FinitePresentation R M
x : PrimeSpectrum R
hx : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x
⊢ ∃ t ⊆ freeLocus R M, IsOpen t ∧ x ∈ t
have this : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
Tactic: have : Module.Free _ _ := 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
inst_3 : FinitePresentation R M
x : PrimeSpectrum R
hx : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x
this : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
⊢ ∃ t ⊆ freeLocus R M, IsOpen t ∧ x ∈ t
have obtain : ∀ (r : R) (hr : r ∈ x.asIdeal.primeCompl) (hr' : Free (Localization (Submonoid.powers r)) (LocalizedModule.Away r M)),
  finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) =
      finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M) →
    ∃ t ⊆ freeLocus R M, IsOpen t ∧ x ∈ t
Tactic: obtain ⟨r, hr, hr', _⟩ := Module.FinitePresentation.exists_free_localizedModule_powers
    x.asIdeal.primeCompl (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
    (Localization.AtPrime x.asIdeal)
-- 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
inst_3 : FinitePresentation R M
⊢ IsLocallyConstant (Y := ℕ) fun (x : (↑(freeLocus R M) : Type uR)) ↦ rankAtStalk M (↑x : PrimeSpectrum R)
have refine : ∀ (x : (↑(freeLocus R M) : Type uR)) (x : PrimeSpectrum R)
  (hx : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x),
  ∃ (U : Set (↑(freeLocus R M) : Type uR)),
    IsOpen U ∧
      Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) x hx ∈
          U ∧
        ∀ x' ∈ U,
          rankAtStalk M (↑x' : PrimeSpectrum R) =
            rankAtStalk M
              (↑(Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
                    Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) x hx) :
                PrimeSpectrum R)
Tactic: refine (IsLocallyConstant.iff_exists_open _).mpr fun ⟨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
inst_3 : FinitePresentation R M
x_1 : (↑(freeLocus R M) : Type uR)
x : PrimeSpectrum R
hx : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x
⊢ ∃ (U : Set (↑(freeLocus R M) : Type uR)),
    IsOpen U ∧
      Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) x hx ∈
          U ∧
        ∀ x' ∈ U,
          rankAtStalk M (↑x' : PrimeSpectrum R) =
            rankAtStalk M
              (↑(Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
                    Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) x hx) :
                PrimeSpectrum R)
have this : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
Tactic: have : Module.Free _ _ := 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
inst_3 : FinitePresentation R M
x_1 : (↑(freeLocus R M) : Type uR)
x : PrimeSpectrum R
hx : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x
this : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
⊢ ∃ (U : Set (↑(freeLocus R M) : Type uR)),
    IsOpen U ∧
      Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) x hx ∈
          U ∧
        ∀ x' ∈ U,
          rankAtStalk M (↑x' : PrimeSpectrum R) =
            rankAtStalk M
              (↑(Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
                    Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) x hx) :
                PrimeSpectrum R)
have obtain : ∀ (f : R) (hf : f ∈ x.asIdeal.primeCompl) (hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M))
  (hf'' :
    finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
      finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)),
  ∃ (U : Set (↑(freeLocus R M) : Type uR)),
    IsOpen U ∧
      Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) x hx ∈
          U ∧
        ∀ x' ∈ U,
          rankAtStalk M (↑x' : PrimeSpectrum R) =
            rankAtStalk M
              (↑(Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
                    Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) x hx) :
                PrimeSpectrum R)
Tactic: obtain ⟨f, hf, hf', hf''⟩ := Module.FinitePresentation.exists_free_localizedModule_powers
    x.asIdeal.primeCompl (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
    (Localization.AtPrime x.asIdeal)
-- 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
inst_3 : FinitePresentation R M
x_1 : (↑(freeLocus R M) : Type uR)
x : PrimeSpectrum R
hx : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x
this : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
⊢ ∃ (U : Set (↑(freeLocus R M) : Type uR)),
    IsOpen U ∧
      Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) x hx ∈
          U ∧
        ∀ x' ∈ U,
          rankAtStalk M (↑x' : PrimeSpectrum R) =
            rankAtStalk M
              (↑(Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
                    Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) x hx) :
                PrimeSpectrum R)
have refine : ∀ (x' : (↑(freeLocus R M) : Type uR)),
  Membership.mem (γ := Set (↑(freeLocus R M) : Type uR))
      (Subtype.val (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) ⁻¹'
        (↑(basicOpen f) : Set (PrimeSpectrum R)))
      x' →
    rankAtStalk M (↑x' : PrimeSpectrum R) =
      rankAtStalk M
        (↑(Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) x
              hx) :
          PrimeSpectrum R)
Tactic: refine ⟨Subtype.val ⁻¹' basicOpen f, (basicOpen f).2.preimage continuous_subtype_val, hf, ?_⟩
-- 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
inst_3 : FinitePresentation R M
x_1 : (↑(freeLocus R M) : Type uR)
x : PrimeSpectrum R
hx : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x
this : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) p
hp :
  Membership.mem (γ := Set (↑(freeLocus R M) : Type uR))
    (Subtype.val (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) ⁻¹'
      (↑(basicOpen f) : Set (PrimeSpectrum R)))
    (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) p hp'')
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
⊢ rankAtStalk M
      (↑(Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) p
            hp'') :
        PrimeSpectrum R) =
    rankAtStalk M
      (↑(Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) x
            hx) :
        PrimeSpectrum R)
have hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl
Tactic: have hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl := by
    simpa [Submonoid.powers_le, Ideal.primeCompl]
-- 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
inst_3 : FinitePresentation R M
x_1 : (↑(freeLocus R M) : Type uR)
x : PrimeSpectrum R
hx : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x
this_1 : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) p
hp :
  Membership.mem (γ := Set (↑(freeLocus R M) : Type uR))
    (Subtype.val (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) ⁻¹'
      (↑(basicOpen f) : Set (PrimeSpectrum R)))
    (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) p hp'')
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl
Rₚ : Type uR := Localization.AtPrime p.asIdeal
Mₚ : Type (max uR uM) := LocalizedModule p.asIdeal.primeCompl M
this : Algebra (Localization.Away f) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization.Away f) Rₚ (Submonoid.powers f) p.asIdeal.primeCompl hp'
⊢ rankAtStalk M
      (↑(Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) p
            hp'') :
        PrimeSpectrum R) =
    rankAtStalk M
      (↑(Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) x
            hx) :
        PrimeSpectrum R)
have this₁ : IsScalarTower R (Localization.Away f) Rₚ
Tactic: have : IsScalarTower R (Localization.Away f) Rₚ :=
    IsLocalization.localization_isScalarTower_of_submonoid_le ..
-- 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
inst_3 : FinitePresentation R M
x_1 : (↑(freeLocus R M) : Type uR)
x : PrimeSpectrum R
hx : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x
this_1 : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) p
hp :
  Membership.mem (γ := Set (↑(freeLocus R M) : Type uR))
    (Subtype.val (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) ⁻¹'
      (↑(basicOpen f) : Set (PrimeSpectrum R)))
    (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) p hp'')
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl
Rₚ : Type uR := Localization.AtPrime p.asIdeal
Mₚ : Type (max uR uM) := LocalizedModule p.asIdeal.primeCompl M
this_2 : Algebra (Localization.Away f) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization.Away f) Rₚ (Submonoid.powers f) p.asIdeal.primeCompl hp'
this_3 : IsScalarTower R (Localization.Away f) Rₚ
this : Module (Localization.Away f) Mₚ := compHom Mₚ (algebraMap (Localization.Away f) Rₚ)
r : R
r' : Localization.Away f
m : Mₚ
⊢ HSMul.hSMul (α := Rₚ) ((algebraMap (Localization.Away f) Rₚ : (a : Localization.Away f) → Rₚ) (r • r') : Rₚ) m =
    r • r' • m
have simp : r •
    HSMul.hSMul (α := Localization.AtPrime p.asIdeal)
      ((algebraMap (Localization.Away f) (Localization.AtPrime p.asIdeal) :
            (a : Localization.Away f) → Localization.AtPrime p.asIdeal)
          r' :
        Localization.AtPrime p.asIdeal)
      m =
  r • r' • m
Tactic: simp [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
inst_3 : FinitePresentation R M
x_1 : (↑(freeLocus R M) : Type uR)
x : PrimeSpectrum R
hx : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x
this_1 : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) p
hp :
  Membership.mem (γ := Set (↑(freeLocus R M) : Type uR))
    (Subtype.val (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) ⁻¹'
      (↑(basicOpen f) : Set (PrimeSpectrum R)))
    (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) p hp'')
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl
Rₚ : Type uR := Localization.AtPrime p.asIdeal
Mₚ : Type (max uR uM) := LocalizedModule p.asIdeal.primeCompl M
this_2 : Algebra (Localization.Away f) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization.Away f) Rₚ (Submonoid.powers f) p.asIdeal.primeCompl hp'
this_3 : IsScalarTower R (Localization.Away f) Rₚ
this : Module (Localization.Away f) Mₚ := compHom Mₚ (algebraMap (Localization.Away f) Rₚ)
⊢ rankAtStalk M
      (↑(Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) p
            hp'') :
        PrimeSpectrum R) =
    rankAtStalk M
      (↑(Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) x
            hx) :
        PrimeSpectrum R)
have this₁ : IsScalarTower R (Localization.Away f) Mₚ
Tactic: have : IsScalarTower R (Localization.Away f) Mₚ :=
    ⟨fun r r' m ↦ show algebraMap _ Rₚ (r • r') • m = _ by
      simp [Rₚ, Mₚ, Algebra.smul_def, ← IsScalarTower.algebraMap_apply, mul_smul]; rfl⟩