awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
have mem : ∀ (a : ↥T), Membership.mem (α := R') p ((algebraMap R R' : (a : R) → R') (↑a : R) : R')
Tactic: have mem (a : T) : algebraMap R R' a ∈ p := by
    simpa [← Ideal.mem_comap, ← hT] using Ideal.subset_span a.2
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
mem : ∀ (a : ↥T), Membership.mem (α := R') p ((algebraMap R R' : (a : R) → R') (↑a : R) : R')
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
have mem₁ : ∀ (a : ↥T), ∃ (n : ℕ) (s' : ↥S), s' • (↑a : R) ^ n • m = 0
Tactic: simp only [hx, Ideal.mem_radical_iff, mem_bot, mem_colon_singleton, ← map_pow, algebraMap_smul,
    ← IsLocalizedModule.mk'_smul, IsLocalizedModule.mk'_eq_zero' f] at mem
Cleared hypotheses: mem
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
mem : ∀ (a : ↥T), ∃ (n : ℕ) (s' : ↥S), s' • (↑a : R) ^ n • m = 0
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
have choose : ∀ (e : (a : ↥T) → ℕ) (g : (a : ↥T) → ↥S) (hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0),
  Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
Tactic: choose e g hg using mem
Cleared hypotheses: mem
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
have refine_1 : LE.le (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
  (Ideal.radical (colon (M := M) ⊥ {HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m}))
Tactic: refine ⟨.under R p, (∏ a, g a).1 • m, le_antisymm ?_ fun r hr ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
refine_1 :
  LE.le (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
    (Ideal.radical (colon (M := M) ⊥ {HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m}))
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
have refine_2 : ∀ (r : R)
  (hr :
    Membership.mem (γ := Submodule R R)
      (Ideal.radical (colon (M := M) ⊥ {HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m})) r),
  Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) r
Tactic: refine ⟨.under R p, (∏ a, g a).1 • m, le_antisymm ?_ fun r hr ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
⊢ LE.le (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
    (Ideal.radical (colon (M := M) ⊥ {HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m}))
have refine_1 : (↑T : Set R) ⊆
  (↑(Ideal.radical (colon (M := M) ⊥ {HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m})) : Set R)
Tactic: rw [← hT, Ideal.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
a : R
ha : a ∈ (↑T : Set R)
⊢ a ∈ (↑(Ideal.radical (colon (M := M) ⊥ {HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m})) : Set R)
have refine_1 : ∃ (n : ℕ), a ^ n • HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m = 0
Tactic: simp only [SetLike.mem_coe, Ideal.mem_radical_iff, mem_bot, mem_colon_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
a : R
ha : a ∈ (↑T : Set R)
⊢ ∃ (n : ℕ), a ^ n • HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m = 0
have refine_1 : ∀ (u : ↥S) (hu : ∏ a : ↥T, g a = g (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha) * u),
  ∃ (n : ℕ), a ^ n • HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m = 0
Tactic: obtain ⟨u, hu⟩ : g ⟨a, ha⟩ ∣ (∏ a, g a) := by
      apply Finset.dvd_prod_of_mem g (Finset.mem_univ ⟨a, ha⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
a : R
ha : a ∈ (↑T : Set R)
u : ↥S
hu : ∏ a : ↥T, g a = g (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha) * u
⊢ ∃ (n : ℕ), a ^ n • HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m = 0
have h : a ^ e (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha) • HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m = 0
Tactic: use e ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
a : R
ha : a ∈ (↑T : Set R)
u : ↥S
hu : ∏ a : ↥T, g a = g (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha) * u
⊢ a ^ e (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha) • HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m = 0
have h : (↑u : R) •
    (↑(g (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha)) : R) • a ^ e (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha) • m =
  0
Tactic: rw [hu, Submonoid.coe_mul, smul_smul, ← mul_assoc, mul_comm, ← smul_smul, mul_comm, ← smul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
hr :
  Membership.mem (γ := Submodule R R)
    (Ideal.radical (colon (M := M) ⊥ {HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m})) r
⊢ Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) r
have hr₁ : ∃ (n : ℕ), (r ^ n * (↑(∏ a : ↥T, g a) : R)) • m = 0
Tactic: simp only [Ideal.mem_radical_iff, mem_bot, mem_colon_singleton, smul_smul] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
hr : ∃ (n : ℕ), (r ^ n * (↑(∏ a : ↥T, g a) : R)) • m = 0
⊢ Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) r
have refine_2 : ∀ (k : ℕ) (hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0),
  Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) r
Tactic: obtain ⟨k, hk⟩ := hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0
⊢ Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (r ^ k * (↑(∏ a : ↥T, g a) : R))
have rw : Membership.mem (γ := Ideal R)
  (Ideal.comap (F := R →+* R') (algebraMap R R') (Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})))
  (r ^ k * (↑(∏ a : ↥T, g a) : R))
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0
⊢ Membership.mem (γ := Ideal R)
    (Ideal.comap (F := R →+* R') (algebraMap R R') (Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})))
    (r ^ k * (↑(∏ a : ↥T, g a) : R))
have h : Membership.mem (γ := Ideal R') (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
  (HPow.hPow (α := R') (β := ℕ) ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R') 1)
Tactic: use 1
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0
⊢ Membership.mem (γ := Ideal R') (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
    (HPow.hPow (α := R') (β := ℕ) ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R') 1)
have h : Membership.mem.{u_2, u_2} (α := R') (γ := Ideal R') (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
  ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R')
Tactic: simp_rw [pow_one, mem_colon_singleton, algebraMap_smul, ← IsLocalizedModule.mk'_smul,
        hk, IsLocalizedModule.mk'_zero, mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0
h :
  Membership.mem.{u_2, u_2} (α := R') (γ := Ideal R') (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
    ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R')
⊢ Membership.mem (γ := Ideal R') (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
    (HPow.hPow (α := R') (β := ℕ) ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R') 1)
have h₁ : Membership.mem (γ := Submodule R' M') ⊥
  (HSMul.hSMul.{u_2, u_4, u_4} (α := R') ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R')
    (IsLocalizedModule.mk' f m s))
Tactic: simp_rw [pow_one, mem_colon_singleton, algebraMap_smul, ← IsLocalizedModule.mk'_smul,
        hk, IsLocalizedModule.mk'_zero, mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0
h :
  Membership.mem.{u_2, u_2} (α := R') (γ := Ideal R') (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
    ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R')
h₁ :
  Membership.mem (γ := Submodule R' M') ⊥
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R') ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R')
      (IsLocalizedModule.mk' f m s))
⊢ Membership.mem (γ := Ideal R') (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
    (HPow.hPow (α := R') (β := ℕ) ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R') 1)
have h₂ : Membership.mem (γ := Submodule R' M') ⊥ ((r ^ k * (↑(∏ a : ↥T, g a) : R)) • IsLocalizedModule.mk' f m s)
Tactic: simp_rw [pow_one, mem_colon_singleton, algebraMap_smul, ← IsLocalizedModule.mk'_smul,
        hk, IsLocalizedModule.mk'_zero, mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0
h :
  Membership.mem.{u_2, u_2} (α := R') (γ := Ideal R') (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
    ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R')
h₁ :
  Membership.mem (γ := Submodule R' M') ⊥
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R') ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R')
      (IsLocalizedModule.mk' f m s))
h₂ : Membership.mem (γ := Submodule R' M') ⊥ ((r ^ k * (↑(∏ a : ↥T, g a) : R)) • IsLocalizedModule.mk' f m s)
⊢ Membership.mem (γ := Ideal R') (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
    (HPow.hPow (α := R') (β := ℕ) ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R') 1)
have h₃ : Membership.mem (γ := Submodule R' M') ⊥ (IsLocalizedModule.mk' f ((r ^ k * (↑(∏ a : ↥T, g a) : R)) • m) s)
Tactic: simp_rw [pow_one, mem_colon_singleton, algebraMap_smul, ← IsLocalizedModule.mk'_smul,
        hk, IsLocalizedModule.mk'_zero, mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0
h :
  Membership.mem.{u_2, u_2} (α := R') (γ := Ideal R') (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
    ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R')
h₁ :
  Membership.mem (γ := Submodule R' M') ⊥
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R') ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R')
      (IsLocalizedModule.mk' f m s))
h₂ : Membership.mem (γ := Submodule R' M') ⊥ ((r ^ k * (↑(∏ a : ↥T, g a) : R)) • IsLocalizedModule.mk' f m s)
h₃ : Membership.mem (γ := Submodule R' M') ⊥ (IsLocalizedModule.mk' f ((r ^ k * (↑(∏ a : ↥T, g a) : R)) • m) s)
⊢ Membership.mem (γ := Ideal R') (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
    (HPow.hPow (α := R') (β := ℕ) ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R') 1)
have h₄ : Membership.mem (γ := Submodule R' M') ⊥ (IsLocalizedModule.mk' f 0 s)
Tactic: simp_rw [pow_one, mem_colon_singleton, algebraMap_smul, ← IsLocalizedModule.mk'_smul,
        hk, IsLocalizedModule.mk'_zero, mem_bot]