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
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)
r : R
hr : r ∈ x.asIdeal.primeCompl
hr' : Free (Localization (Submonoid.powers r)) (LocalizedModule.Away r M)
right :
  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:
⟨basicOpen r, basicOpen_subset_freeLocus_iff.mpr inferInstance, (basicOpen r).2, hr⟩

Premises used: Iff.mpr, Module.basicOpen_subset_freeLocus_iff, PrimeSpectrum.basicOpen, inferInstance, SetLike.coe, And.intro, Exists.intro, TopologicalSpace.Opens.is_open'
-- 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
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)
r : R
hr : r ∈ x.asIdeal.primeCompl
hr' : Free (Localization (Submonoid.powers r)) (LocalizedModule.Away r M)
right :
  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:
exact ⟨basicOpen r, basicOpen_subset_freeLocus_iff.mpr inferInstance, (basicOpen r).2, hr⟩
-- 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
inst_3 : FinitePresentation R M
⊢ IsLocallyConstant (Y := ℕ) fun (x : (↑(freeLocus R M) : Type uR)) ↦ rankAtStalk M (↑x : PrimeSpectrum R)

Tactic:
(IsLocallyConstant.iff_exists_open _).mpr fun ⟨x, hx⟩ ↦ ?_

Premises used: Iff.mpr, IsLocallyConstant.iff_exists_open, Membership.mem, Exists, And, IsOpen, _private.0.Module.isLocallyConstant_rankAtStalk_freeLocus.match_1
-- 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
inst_3 : FinitePresentation R M
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)
⊢ IsLocallyConstant (Y := ℕ) fun (x : (↑(freeLocus R M) : Type uR)) ↦ rankAtStalk M (↑x : PrimeSpectrum R)

Tactic:
refine (IsLocallyConstant.iff_exists_open _).mpr fun ⟨x, hx⟩ ↦ ?_

Premises used: Iff.mpr, IsLocallyConstant.iff_exists_open
-- 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
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
⊢ Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)

Tactic:
have : Module.Free _ _ := 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
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)
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)
⊢ ∃ (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)

Premises used: Localization.AtPrime, Module.FinitePresentation.exists_free_localizedModule_powers, LocalizedModule.mkLinearMap, Ideal.primeCompl, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
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)

Tactic:
⟨Subtype.val ⁻¹' basicOpen f, (basicOpen f).2.preimage continuous_subtype_val, hf, ?_⟩

Premises used: PrimeSpectrum.basicOpen, continuous_subtype_val, SetLike.coe, Set.preimage, And.intro, Exists.intro, TopologicalSpace.Opens.is_open', IsOpen.preimage, Subtype.val
-- 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
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)
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)
⊢ ∃ (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 ⟨Subtype.val ⁻¹' basicOpen f, (basicOpen f).2.preimage continuous_subtype_val, hf, ?_⟩
-- 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
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
⊢ Submonoid.powers f ≤ p.asIdeal.primeCompl

Tactic:
simpa [Submonoid.powers_le, Ideal.primeCompl]

Premises used: Ideal.primeCompl, Submonoid.powers_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
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
⊢ Submonoid.powers f ≤ p.asIdeal.primeCompl

Tactic:
have hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl := by
    simpa [Submonoid.powers_le, Ideal.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
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'
⊢ IsScalarTower R (Localization.Away f) Rₚ

Tactic:
have : IsScalarTower R (Localization.Away f) Rₚ :=
    IsLocalization.localization_isScalarTower_of_submonoid_le ..
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
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ₚ
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
⊢ HSMul.hSMul (α := Rₚ) ((algebraMap (Localization.Away f) Rₚ : (a : Localization.Away f) → Rₚ) (r • r') : Rₚ) m =
    r • r' • m

Tactic:
simp [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
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ₚ
⊢ 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:
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
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ₚ)
⊢ 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⟩
-- 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
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_4 : Module (Localization.Away f) Mₚ := compHom Mₚ (algebraMap (Localization.Away f) Rₚ)
this : IsScalarTower R (Localization.Away f) Mₚ
r : Localization.Away f
r' : Rₚ
m : Mₚ
rw :
  (r • r') • m =
    HMul.hMul (α := Rₚ) ((algebraMap (Localization.Away f) Rₚ : (a : Localization.Away f) → Rₚ) r : Rₚ) r' • m
rw₁ rw₂ : (r • r') • m = (r • r') • m
⊢ (r • r') • m =
    HSMul.hSMul (α := Rₚ) ((algebraMap (Localization.Away f) Rₚ : (a : Localization.Away f) → 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
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_4 : Module (Localization.Away f) Mₚ := compHom Mₚ (algebraMap (Localization.Away f) Rₚ)
this : IsScalarTower R (Localization.Away f) Mₚ
⊢ IsScalarTower (Localization.Away f) Rₚ Mₚ

Tactic:
have : IsScalarTower (Localization.Away f) Rₚ Mₚ :=
    ⟨fun r r' m ↦ show _ = algebraMap _ Rₚ r • r' • m by rw [← mul_smul, ← Algebra.smul_def]⟩