awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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 : IsLocalization.mk' (M := S) R' ((↑t : R) * r) 1 ∈ p
⊢ IsLocalization.mk' (M := S) R' ((↑t : R) * r) 1 * IsLocalization.mk' R' 1 (t * s) ∈ p

Tactic:
apply Ideal.IsTwoSided.mul_mem_of_left

Premises used: Ideal.IsTwoSided.mul_mem_of_left
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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 : Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x})) ((↑t : R) * r)
⊢ IsLocalization.mk' (M := S) R' ((↑t : R) * r) 1 ∈ p

Tactic:
rw [IsLocalization.mk'_one, ← Ideal.mem_comap, hx]

Premises used: IsLocalization.mk'_one, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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)
h₁ : ∀ (hn : 0 < n), 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)

Tactic:
rcases eq_zero_or_pos n with rfl | hn

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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
t : ↥S
this : IsLocalization.mk' R' r s = IsLocalization.mk' (M := S) R' ((↑t : R) * r) 1 * IsLocalization.mk' R' 1 (t * s)
ht : t • HPow.hPow (β := ℕ) r 0 • x = 0
⊢ Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {x}) (HPow.hPow (β := ℕ) (↑t : R) 1)

Tactic:
simpa using ht
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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
t : ↥S
this : IsLocalization.mk' R' r s = IsLocalization.mk' (M := S) R' ((↑t : R) * r) 1 * IsLocalization.mk' R' 1 (t * s)
ht : t • HPow.hPow (β := ℕ) r 0 • x = 0
⊢ Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x})) ((↑t : R) * r)

Tactic:
exact Ideal.IsTwoSided.mul_mem_of_left _ ⟨1, by simpa using ht⟩
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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)
hn : 0 < n
h : Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {x}) (((↑t : R) * r) ^ n)
⊢ Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x})) ((↑t : R) * r)

Tactic:
use n
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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)
hn : 0 < n
h : Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {r ^ n • x}) ((↑t : R) ^ n)
⊢ Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {x}) (((↑t : R) * r) ^ n)

Tactic:
rw [mem_colon_singleton, mul_pow, mul_smul, ← mem_colon_singleton]

Premises used: Submodule.mem_colon_singleton, mul_pow, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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) ⊥ {r ^ n • x}) (↑t : R)

Tactic:
simpa using ht
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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) ⊥ {r ^ n • x}) ((↑t : R) ^ n)

Tactic:
exact Ideal.pow_mem_of_mem _ (by simpa using ht) n hn

Premises used: Ideal.pow_mem_of_mem
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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
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)))
⊢ Membership.mem (γ := Set (Ideal (Localization.AtPrime p)))
    (associatedPrimes (Localization.AtPrime p) (LocalizedModule.AtPrime p M)) (maximalIdeal (Localization.AtPrime p))

Tactic:
apply mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule
    p.primeCompl (LocalizedModule.mkLinearMap p.primeCompl M)

Premises used: Module.associatedPrimes.mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule, LocalizedModule.mkLinearMap, Ideal.primeCompl
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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 R)) (associatedPrimes R M)
    (Ideal.comap (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p))
      (maximalIdeal (Localization.AtPrime p)))

Tactic:
simpa [Localization.AtPrime.under_maximalIdeal] using ass

Premises used: Localization.AtPrime.under_maximalIdeal
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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)
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)
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* R') (algebraMap R R') p)

Tactic:
rcases ass with ⟨hp, x, hx⟩
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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})
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)
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* R') (algebraMap R R') p)

Tactic:
rcases fg with ⟨T, hT⟩
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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)
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)
⊢ 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⟩

Premises used: IsLocalizedModule.mk'_surjective, rfl
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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})
a : ↥T
⊢ Membership.mem (α := R') p ((algebraMap R R' : (a : R) → R') (↑a : R) : R')

Tactic:
simpa [← Ideal.mem_comap, ← hT] using Ideal.subset_span a.2

Premises used: Ideal.subset_span, Ideal.mem_comap, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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})
⊢ ∀ (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
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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')
⊢ ∀ (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

Premises used: IsLocalizedModule.mk'_eq_zero', Submodule.mem_bot, algebraMap_smul, map_pow, IsLocalizedModule.mk'_smul, Submodule.mem_colon_singleton, Ideal.mem_radical_iff
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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
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)
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* R') (algebraMap R R') p)

Tactic:
choose e g hg using mem
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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)

Tactic:
⟨.under R p, (∏ a, g a).1 • m, le_antisymm ?_ fun r hr ↦ ?_⟩

Premises used: IsAssociatedPrime, Submodule.IsAssociatedPrime.mk, Finset.univ, Set.Mem, setOf, Finset.prod, le_antisymm, associatedPrimes, Exists.intro, HSMul.hSMul, Ideal.IsPrime.under, Subtype.val
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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}))
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
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) (Ideal.comap (F := R →+* R') (algebraMap R R') p)

Tactic:
refine ⟨.under R p, (∏ a, g a).1 • m, le_antisymm ?_ fun r hr ↦ ?_⟩
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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 :
  (↑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)
⊢ 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:
rw [← hT, Ideal.span_le]

Premises used: Ideal.span_le
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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)
refine_1 : ∃ (n : ℕ), a ^ n • HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m = 0
⊢ a ∈ (↑(Ideal.radical (colon (M := M) ⊥ {HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m})) : Set R)

Tactic:
simp only [SetLike.mem_coe, Ideal.mem_radical_iff, mem_bot, mem_colon_singleton]

Premises used: Submodule.mem_bot, SetLike.mem_coe, Submodule.mem_colon_singleton, Ideal.mem_radical_iff
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
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)
⊢ g (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha) ∣ ∏ a : ↥T, g a

Tactic:
apply Finset.dvd_prod_of_mem g (Finset.mem_univ ⟨a, ha⟩)

Premises used: Finset.mem_univ, Finset.dvd_prod_of_mem