awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
ass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
⊢ Membership.mem (γ := Set (Ideal R')) (associatedPrimes R' M') p
have rcases : ∀ (hp : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)) (x : M)
  (hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))),
  Membership.mem (γ := Set (Ideal R')) (associatedPrimes R' M') p
Tactic: rcases ass with ⟨hp, x, hx⟩
Cleared hypotheses: ass
-- 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 : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)
x : M
hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))
⊢ Membership.mem (γ := Set (Ideal R')) (associatedPrimes R' M') p
have toIsPrime : p.IsPrime
Tactic: constructor
-- 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 : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)
x : M
hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))
toIsPrime : p.IsPrime
⊢ Membership.mem (γ := Set (Ideal R')) (associatedPrimes R' M') p
have eq_radical_colon : ∃ (x : M'), p = Ideal.radical (colon (M := M') ⊥ {x})
Tactic: constructor
-- 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 : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)
x : M
hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))
⊢ p.IsPrime
have toIsPrime : p ≠ ⊤
Tactic: refine (IsLocalization.isPrime_iff_isPrime_disjoint S _ _).mpr
      ⟨hp, (IsLocalization.disjoint_under_iff S R' p).mpr ?_⟩
-- 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 : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)
x : M
hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))
⊢ ∃ (x : M'), p = Ideal.radical (colon (M := M') ⊥ {x})
have h : p = Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M')))
Tactic: use f x
-- 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 : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)
x : M
hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))
⊢ p = Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M')))
have h : ∀ (t : R'),
  t ∈ p ↔
    Membership.mem (γ := Ideal R') (Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))))
      t
Tactic: ext t
-- 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 : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)
x : M
hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))
t : R'
⊢ t ∈ p ↔
    Membership.mem (γ := Ideal R') (Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))))
      t
have h : ∀ (r : R) (s : ↥S) (hrs : IsLocalization.mk' R' r s = t),
  t ∈ p ↔
    Membership.mem (γ := Ideal R') (Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))))
      t
Tactic: rcases IsLocalization.exists_mk'_eq S t with ⟨r, s, hrs⟩
-- 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 : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)
x : M
hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))
t : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t
⊢ t ∈ p ↔
    Membership.mem (γ := Ideal R') (Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))))
      t
have h : IsLocalization.mk' R' r s ∈ p ↔ ∃ (n : ℕ) (s' : ↥S), s' • r ^ n • x = 0
Tactic: simp_rw [← hrs, Ideal.mem_radical_iff, mem_colon_singleton, ← IsLocalizedModule.mk'_one S f,
      ← IsLocalization.mk'_pow, IsLocalizedModule.mk'_smul_mk', mul_one, mem_bot,
      IsLocalizedModule.mk'_eq_zero']
-- 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 : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)
x : M
hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))
t : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t
⊢ IsLocalization.mk' R' r s ∈ p ↔ ∃ (n : ℕ) (s' : ↥S), s' • r ^ n • x = 0
have h : ∀ (h : IsLocalization.mk' R' r s ∈ p), ∃ (b : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := ↥S) 1 (r ^ b • x) = 0
Tactic: refine ⟨fun h ↦ exists_comm.mp ⟨1, ?_⟩, fun ⟨n, t, ht⟩ ↦ ?_⟩
-- 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 : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)
x : M
hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))
t : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t
h : ∀ (h : IsLocalization.mk' R' r s ∈ p), ∃ (b : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := ↥S) 1 (r ^ b • x) = 0
⊢ IsLocalization.mk' R' r s ∈ p ↔ ∃ (n : ℕ) (s' : ↥S), s' • r ^ n • x = 0
have h₁ : (∃ (n : ℕ) (s' : ↥S), s' • r ^ n • x = 0) → ∀ (n : ℕ) (t : ↥S) (ht : t • r ^ n • x = 0), IsLocalization.mk' R' r s ∈ p
Tactic: refine ⟨fun h ↦ exists_comm.mp ⟨1, ?_⟩, fun ⟨n, t, ht⟩ ↦ ?_⟩
-- 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 : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)
x : M
hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))
t : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t
h : IsLocalization.mk' R' r s ∈ p
⊢ ∃ (b : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := ↥S) 1 (r ^ b • x) = 0
have h₁ : Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) r
Tactic: simp only [← mem_colon_singleton, one_smul, ← mem_bot R, ← hx, ← Ideal.mem_radical_iff]
-- 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 : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)
x : M
hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))
t_1 : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t_1
h : ∃ (n : ℕ) (s' : ↥S), s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
⊢ IsLocalization.mk' R' r s = IsLocalization.mk' (M := S) R' ((↑t : R) * r) 1 * IsLocalization.mk' R' 1 (t * s)
have rw : IsLocalization.mk' R' (r * ((↑t : R) * (↑s : R)) - (↑t : R) * r * (↑s : R)) (s * (t * s)) = 0
Tactic: rw [← hSR'.mk'_mul, mul_one, one_mul, ← sub_eq_zero, ← hSR'.mk'_sub, Submonoid.coe_mul]
-- 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 : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)
x : M
hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))
t_1 : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t_1
h : ∃ (n : ℕ) (s' : ↥S), s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
⊢ IsLocalization.mk' R' r s ∈ p
have this : IsLocalization.mk' R' r s = IsLocalization.mk' (M := S) R' ((↑t : R) * r) 1 * IsLocalization.mk' R' 1 (t * s)
Tactic: have : hSR'.mk' R' r s = hSR'.mk' R' (t.1 * r) 1 * hSR'.mk' R' 1 (t * s) := by
        rw [← hSR'.mk'_mul, mul_one, one_mul, ← sub_eq_zero, ← hSR'.mk'_sub, Submonoid.coe_mul]
        simp [← mul_assoc, mul_comm r t.1, IsLocalization.mk'_zero]
-- 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 : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)
x : M
hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))
t_1 : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t_1
h : ∃ (n : ℕ) (s' : ↥S), s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
this : IsLocalization.mk' R' r s = IsLocalization.mk' (M := S) R' ((↑t : R) * r) 1 * IsLocalization.mk' R' 1 (t * s)
⊢ IsLocalization.mk' R' r s ∈ p
have h : IsLocalization.mk' (M := S) R' ((↑t : R) * r) 1 * IsLocalization.mk' R' 1 (t * s) ∈ p
Tactic: rw [this]
-- 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 : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)
x : M
hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))
t_1 : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t_1
h : ∃ (n : ℕ) (s' : ↥S), s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
this : IsLocalization.mk' R' r s = IsLocalization.mk' (M := S) R' ((↑t : R) * r) 1 * IsLocalization.mk' R' 1 (t * s)
⊢ IsLocalization.mk' (M := S) R' ((↑t : R) * r) 1 * IsLocalization.mk' R' 1 (t * s) ∈ p
have h : IsLocalization.mk' (M := S) R' ((↑t : R) * r) 1 ∈ p
Tactic: apply Ideal.IsTwoSided.mul_mem_of_left
-- 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 : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)
x : M
hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))
t_1 : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t_1
h : ∃ (n : ℕ) (s' : ↥S), s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
this : IsLocalization.mk' R' r s = IsLocalization.mk' (M := S) R' ((↑t : R) * r) 1 * IsLocalization.mk' R' 1 (t * s)
⊢ IsLocalization.mk' (M := S) R' ((↑t : R) * r) 1 ∈ p
have h : Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x})) ((↑t : R) * r)
Tactic: rw [IsLocalization.mk'_one, ← Ideal.mem_comap, 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 : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)
x : M
hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))
t_1 : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t_1
h : ∃ (n : ℕ) (s' : ↥S), s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
this : IsLocalization.mk' R' r s = IsLocalization.mk' (M := S) R' ((↑t : R) * r) 1 * IsLocalization.mk' R' 1 (t * s)
⊢ Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x})) ((↑t : R) * r)
have h : ∀ (ht : t • HPow.hPow (β := ℕ) r 0 • x = 0),
  Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x})) ((↑t : R) * r)
Tactic: rcases eq_zero_or_pos n with rfl | hn
Cleared hypotheses: n, ht
-- 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 : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)
x : M
hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))
t_1 : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t_1
h_1 : ∃ (n : ℕ) (s' : ↥S), s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
this : IsLocalization.mk' R' r s = IsLocalization.mk' (M := S) R' ((↑t : R) * r) 1 * IsLocalization.mk' R' 1 (t * s)
h :
  ∀ (ht : t • HPow.hPow (β := ℕ) r 0 • x = 0),
    Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x})) ((↑t : R) * r)
⊢ Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x})) ((↑t : R) * r)
have h₁ : ∀ (hn : 0 < n), Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x})) ((↑t : R) * r)
Tactic: rcases eq_zero_or_pos n with rfl | hn
-- 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 : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)
x : M
hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))
t_1 : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t_1
h : ∃ (n : ℕ) (s' : ↥S), s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
this : IsLocalization.mk' R' r s = IsLocalization.mk' (M := S) R' ((↑t : R) * r) 1 * IsLocalization.mk' R' 1 (t * s)
hn : 0 < n
⊢ Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x})) ((↑t : R) * r)
have h : Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {x}) (((↑t : R) * r) ^ n)
Tactic: use n
-- 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 : Ideal.IsPrime (Ideal.comap (F := R →+* R') (algebraMap R R') p)
x : M
hx : Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (Ideal.radical (colon (M := M) ⊥ {x}))
t_1 : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t_1
h : ∃ (n : ℕ) (s' : ↥S), s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
this : IsLocalization.mk' R' r s = IsLocalization.mk' (M := S) R' ((↑t : R) * r) 1 * IsLocalization.mk' R' 1 (t * s)
hn : 0 < n
⊢ Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {x}) (((↑t : R) * r) ^ n)
have h : Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {r ^ n • x}) ((↑t : R) ^ n)
Tactic: rw [mem_colon_singleton, mul_pow, mul_smul, ← mem_colon_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Ideal R
inst_3 : p.IsPrime
ass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
⊢ Membership.mem (γ := Set (Ideal (Localization.AtPrime p)))
    (associatedPrimes (Localization.AtPrime p) (LocalizedModule.AtPrime p M)) (maximalIdeal (Localization.AtPrime p))
have ass₁ : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M)
  (Ideal.comap (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p))
    (maximalIdeal (Localization.AtPrime p)))
Tactic: apply mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule
    p.primeCompl (LocalizedModule.mkLinearMap p.primeCompl M)
-- 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'
ass : Membership.mem (γ := Set (Ideal R')) (associatedPrimes R' M') p
fg : Ideal.FG (Ideal.comap (F := R →+* R') (algebraMap R R') p)
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
have rcases : ∀ (hp : p.IsPrime) (x : M') (hx : p = Ideal.radical (colon (M := M') ⊥ {x})),
  Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
Tactic: rcases ass with ⟨hp, x, hx⟩
Cleared hypotheses: ass
-- 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'
fg : Ideal.FG (Ideal.comap (F := R →+* R') (algebraMap R R') p)
hp : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
have rcases : ∀ (T : Finset R) (hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)),
  Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
Tactic: rcases fg with ⟨T, hT⟩
Cleared hypotheses: fg
-- 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
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
have rcases : ∀ (m : M) (s : ↥S) (hx : p = Ideal.radical (colon (M := M') ⊥ {Function.uncurry (IsLocalizedModule.mk' f) (m, s)})),
  Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
Tactic: rcases IsLocalizedModule.mk'_surjective S f x with ⟨⟨m, s⟩, rfl⟩
Cleared hypotheses: x, hx