awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
I : Ideal A
h : Disjoint (↑I : Set A) (↑(nonZeroDivisors A) : Set A)
obtain :
  ∀ (P : Ideal A) (h : Membership.mem (γ := Set (Ideal A)) (associatedPrimes A A) P) (hP : I ≤ P),
    LT.lt (α := Ideal A) ⊥ (Module.annihilator A ↥I)
⊢ LT.lt (α := Ideal A) ⊥ (Module.annihilator A ↥I)

Tactic:
obtain ⟨P, h, hP⟩ : ∃ P ∈ associatedPrimes A A, I ≤ P :=
    (I.subset_union_prime_finite (associatedPrimes.finite ..) (f := id) 0 0 fun _ h _ _ ↦ h.1).1 <|
    biUnion_associatedPrimes_eq_compl_nonZeroDivisors A ▸ h.subset_compl_right

Premises used: associatedPrimes.finite, associatedPrimes, Ideal.subset_union_prime_finite, Iff.mp, OfNat.ofNat, Submodule.IsAssociatedPrime.toIsPrime
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
I : Ideal A
h_1 : Disjoint (↑I : Set A) (↑(nonZeroDivisors A) : Set A)
P : Ideal A
h : Membership.mem (γ := Set (Ideal A)) (associatedPrimes A A) P
hP : I ≤ P
⊢ P.IsPrime ∧ ∃ (x : A), P = Submodule.colon (M := A) ⊥ {x}

Tactic:
rw [AssociatedPrimes.mem_iff, isAssociatedPrime_iff] at h

Premises used: AssociatedPrimes.mem_iff, isAssociatedPrime_iff
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
I : Ideal A
h_1 : Disjoint (↑I : Set A) (↑(nonZeroDivisors A) : Set A)
P : Ideal A
h : Membership.mem (γ := Set (Ideal A)) (associatedPrimes A A) P
hP : I ≤ P
h₁ : P.IsPrime ∧ ∃ (x : A), P = Submodule.colon (M := A) ⊥ {x}
⊢ I ≤ P

Tactic:
rw [AssociatedPrimes.mem_iff, isAssociatedPrime_iff] at h

Premises used: AssociatedPrimes.mem_iff, isAssociatedPrime_iff
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
I : Ideal A
h_1 : Disjoint (↑I : Set A) (↑(nonZeroDivisors A) : Set A)
P : Ideal A
h : P.IsPrime ∧ ∃ (x : A), P = Submodule.colon (M := A) ⊥ {x}
hP : I ≤ P
obtain :
  ∀ (x : A) (hP : I ≤ Submodule.colon (M := A) ⊥ {x}) (prime : IsPrime (α := A) (Submodule.colon (M := A) ⊥ {x})),
    LT.lt (α := Ideal A) ⊥ (Module.annihilator A ↥I)
⊢ LT.lt (α := Ideal A) ⊥ (Module.annihilator A ↥I)

Tactic:
obtain ⟨prime, x, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
I : Ideal A
h : Disjoint (↑I : Set A) (↑(nonZeroDivisors A) : Set A)
x : A
hP : I ≤ Submodule.colon (M := A) ⊥ {x}
prime : IsPrime (α := A) (Submodule.colon (M := A) ⊥ {x})
⊢ ∀ n ∈ I, x • n = 0

Tactic:
simpa only [smul_eq_mul, mul_comm x, SetLike.le_def, Submodule.mem_colon_singleton] using hP

Premises used: SetLike.le_def, mul_comm, Submodule.mem_colon_singleton, smul_eq_mul
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
I : Ideal A
h_1 : Disjoint (↑I : Set A) (↑(nonZeroDivisors A) : Set A)
x : A
hP : I ≤ Submodule.colon (M := A) ⊥ {x}
prime : IsPrime (α := A) (Submodule.colon (M := A) ⊥ {x})
h : x = 0
⊢ Eq (α := Ideal A) (Submodule.colon (M := A) ⊥ {x}) ⊤

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
I : Ideal A
h : Disjoint (↑I : Set A) (↑(nonZeroDivisors A) : Set A)
x : A
hP : I ≤ Submodule.colon (M := A) ⊥ {x}
prime : IsPrime (α := A) (Submodule.colon (M := A) ⊥ {x})
⊢ LT.lt (α := Ideal A) ⊥ (Module.annihilator A ↥I)

Tactic:
exact SetLike.lt_iff_le_and_exists.mpr ⟨bot_le, x, Submodule.mem_annihilator.mpr <| by
    simpa only [smul_eq_mul, mul_comm x, SetLike.le_def, Submodule.mem_colon_singleton] using hP,
      fun h : x = 0 ↦ prime.ne_top <| by simp [h]⟩

Premises used: Iff.mpr, SetLike.lt_iff_le_and_exists, Submodule.mem_annihilator, And.intro, Exists.intro, Ideal.IsPrime.ne_top, bot_le
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
I : Ideal A
inst_2 : FaithfulSMul A ↥I
by_contra! : ∀ (this : (↑I : Set A) ∩ (↑(nonZeroDivisors A) : Set A) = ∅), False
⊢ ((↑I : Set A) ∩ (↑(nonZeroDivisors A) : Set A)).Nonempty

Tactic:
by_contra!
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
I : Ideal A
inst_2 : FaithfulSMul A ↥I
this : (↑I : Set A) ∩ (↑(nonZeroDivisors A) : Set A) = ∅
rwa rwa₁ rwa₂ rwa₃ : FaithfulSMul A ↥I
⊢ Eq (α := Ideal A) (Module.annihilator A ↥I) ⊥

Tactic:
rwa [Module.annihilator_eq_bot]

Premises used: Module.annihilator_eq_bot
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
I : Ideal A
inst_2 : FaithfulSMul A ↥I
this : (↑I : Set A) ∩ (↑(nonZeroDivisors A) : Set A) = ∅
⊢ False

Tactic:
exact (bot_lt_annihilator_of_disjoint_nonZeroDivisors
    (Set.disjoint_iff_inter_eq_empty.mpr this)).ne' <| by rwa [Module.annihilator_eq_bot]

Premises used: Iff.mpr, Set.disjoint_iff_inter_eq_empty, LT.lt.ne', Ideal.bot_lt_annihilator_of_disjoint_nonZeroDivisors
-- 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) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
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
⊢ Membership.mem (γ := Set (Ideal R')) (associatedPrimes R' M') 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'
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
eq_radical_colon : ∃ (x : M'), p = Ideal.radical (colon (M := M') ⊥ {x})
⊢ Membership.mem (γ := Set (Ideal R')) (associatedPrimes R' M') p

Tactic:
constructor
-- 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}))
⊢ p.IsPrime

Tactic:
(IsLocalization.isPrime_iff_isPrime_disjoint S _ _).mpr
      ⟨hp, (IsLocalization.disjoint_under_iff S R' p).mpr ?_⟩

Premises used: Iff.mpr, IsLocalization.isPrime_iff_isPrime_disjoint, And.intro, IsLocalization.disjoint_under_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 : 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 ≠ ⊤
⊢ p.IsPrime

Tactic:
refine (IsLocalization.isPrime_iff_isPrime_disjoint S _ _).mpr
      ⟨hp, (IsLocalization.disjoint_under_iff S R' p).mpr ?_⟩

Premises used: Iff.mpr, IsLocalization.isPrime_iff_isPrime_disjoint, And.intro, IsLocalization.disjoint_under_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 : 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 : ∀ (eqtop : p = ⊤), False
⊢ p ≠ ⊤

Tactic:
by_contra eqtop
-- 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}))
eqtop : p = ⊤
⊢ False

Tactic:
simp [eqtop, Ideal.comap_top, Ideal.isPrime_iff] at hp

Premises used: Ideal.isPrime_iff, Ideal.comap_top
-- 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}))
h : p = Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M')))
⊢ ∃ (x : M'), p = Ideal.radical (colon (M := M') ⊥ {x})

Tactic:
use f x

Premises used: DFunLike.coe
-- 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}))
h :
  ∀ (t : R'),
    t ∈ p ↔
      Membership.mem (γ := Ideal R')
        (Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M')))) t
⊢ p = Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M')))

Tactic:
ext t
-- 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 : R'
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
⊢ 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⟩

Premises used: IsLocalization.exists_mk'_eq
-- 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 : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t
h : IsLocalization.mk' R' r s ∈ p ↔ ∃ (n : ℕ) (s' : ↥S), s' • r ^ n • x = 0
⊢ t ∈ p ↔
    Membership.mem (γ := Ideal R') (Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))))
      t

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']

Premises used: IsLocalization.mk'_pow, IsLocalizedModule.mk'_eq_zero', Submodule.mem_bot, IsLocalizedModule.mk'_one, IsLocalizedModule.mk'_smul_mk', Submodule.mem_colon_singleton, Ideal.mem_radical_iff, mul_one
-- 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 : 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

Tactic:
⟨fun h ↦ exists_comm.mp ⟨1, ?_⟩, fun ⟨n, t, ht⟩ ↦ ?_⟩

Premises used: Membership.mem, _private.0.Module.associatedPrimes.mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule.match_6, IsLocalization.mk', exists_comm, Iff.intro, Exists.intro, Iff.mp, OfNat.ofNat
-- 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 : 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
h₁ :
  (∃ (n : ℕ) (s' : ↥S), s' • r ^ n • x = 0) → ∀ (n : ℕ) (t : ↥S) (ht : t • r ^ n • x = 0), IsLocalization.mk' R' r s ∈ p
⊢ IsLocalization.mk' R' r s ∈ p ↔ ∃ (n : ℕ) (s' : ↥S), s' • r ^ n • x = 0

Tactic:
refine ⟨fun h ↦ exists_comm.mp ⟨1, ?_⟩, fun ⟨n, 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 : 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
h₁ : Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) r
⊢ ∃ (b : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := ↥S) 1 (r ^ b • x) = 0

Tactic:
simp only [← mem_colon_singleton, one_smul, ← mem_bot R, ← hx, ← Ideal.mem_radical_iff]

Premises used: Submodule.mem_bot, one_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 : 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
⊢ Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) r

Tactic:
hSR'.mk'_mem_iff.mp h

Premises used: Set.Mem, setOf, IsLocalization.mk'_mem_iff, Set.preimage, Iff.mp
-- 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 : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t
h : IsLocalization.mk' R' r s ∈ p
⊢ Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) r

Tactic:
exact hSR'.mk'_mem_iff.mp h

Premises used: IsLocalization.mk'_mem_iff, Iff.mp
-- 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
rw : IsLocalization.mk' R' (r * ((↑t : R) * (↑s : R)) - (↑t : R) * r * (↑s : R)) (s * (t * s)) = 0
⊢ IsLocalization.mk' R' r s = IsLocalization.mk' (M := S) R' ((↑t : R) * r) 1 * IsLocalization.mk' R' 1 (t * s)

Tactic:
rw [← hSR'.mk'_mul, mul_one, one_mul, ← sub_eq_zero, ← hSR'.mk'_sub, Submonoid.coe_mul]

Premises used: sub_eq_zero, IsLocalization.mk'_sub, mul_one, one_mul, Submonoid.coe_mul, IsLocalization.mk'_mul
-- 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
⊢ IsLocalization.mk' R' (r * ((↑t : R) * (↑s : R)) - (↑t : R) * r * (↑s : R)) (s * (t * s)) = 0

Tactic:
simp [← mul_assoc, mul_comm r t.1, IsLocalization.mk'_zero]

Premises used: mul_assoc, IsLocalization.mk'_zero, mul_comm, 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 : 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)

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]
-- 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 * IsLocalization.mk' R' 1 (t * s) ∈ p
⊢ IsLocalization.mk' R' r s ∈ p

Tactic:
rw [this]