awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
neg :
  ∀ (b : R) (hb : b ∈ p),
    Membership.mem (γ := Submodule R R)
      (Ideal.radical (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M'')))) b
neg₁ :
  ∀ (b : R),
    Membership.mem (γ := Submodule R R)
        (Ideal.radical (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M'')))) b →
      ∀ (n : ℕ)
        (hb :
          Membership.mem (γ := Ideal R) (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M'')))
            (b ^ n)),
        b ∈ p
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M'') p

Tactic:
refine ⟨‹_›, g x, le_antisymm (fun b hb ↦ ?_) (fun b ⟨n, hb⟩ ↦ ?_)⟩
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
b : R
hb : b ∈ p
⊢ Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M') ⊥ {x})) b

Tactic:
rw [hx] at hb
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
b : R
hb : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M') ⊥ {x})) b
⊢ Membership.mem (γ := Submodule R R)
    (Ideal.radical (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M'')))) b

Tactic:
Ideal.radical_mono (fun b hb ↦ ?_) hb

Premises used: Ideal.radical_mono
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
b : R
hb : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M') ⊥ {x})) b
neg :
  ∀ (b : R) (hb : Membership.mem (γ := Submodule R R) (colon (M := M') ⊥ {x}) b),
    Membership.mem (γ := Submodule R R) (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M''))) b
⊢ Membership.mem (γ := Submodule R R)
    (Ideal.radical (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M'')))) b

Tactic:
refine Ideal.radical_mono (fun b hb ↦ ?_) hb

Premises used: Ideal.radical_mono
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
b_1 : R
hb_1 : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M') ⊥ {x})) b_1
b : R
hb : Membership.mem (γ := Submodule R R) (colon (M := M') ⊥ {x}) b
neg : ∀ (hb : b • x = 0), HSMul.hSMul (β := M'') b ((g : (a : M') → M'') x : M'') = 0
⊢ Membership.mem (γ := Submodule R R) (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M''))) b

Tactic:
rw [mem_colon_singleton, mem_bot] at hb ⊢

Premises used: Submodule.mem_bot, Submodule.mem_colon_singleton
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
b_1 : R
hb_1 : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M') ⊥ {x})) b_1
b : R
hb : b • x = 0
neg : Eq.{u_4 + 1} (α := M'') ((g : (a : M') → M'') (b • x) : M'') (0 : M'')
neg₁ : Eq.{u_4 + 1} (α := M'') ((g : (a : M') → M'') 0 : M'') (0 : M'')
neg₂ neg₃ : Eq.{u_4 + 1} (α := M'') 0 0
⊢ HSMul.hSMul (β := M'') b ((g : (a : M') → M'') x : M'') = 0

Tactic:
rw [← map_smul, hb, map_zero]

Premises used: map_zero, map_smul
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
b : R
h_1 :
  Membership.mem (γ := Submodule R R)
    (Ideal.radical (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M'')))) b
n : ℕ
hb : Membership.mem (γ := Ideal R) (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M''))) (b ^ n)
⊢ b ^ n • x ∈ f.range

Tactic:
rw [mem_colon_singleton, mem_bot, ← map_smul, ← LinearMap.mem_ker,
        hfg.linearMap_ker_eq] at hb

Premises used: Submodule.mem_bot, Function.Exact.linearMap_ker_eq, LinearMap.mem_ker, Submodule.mem_colon_singleton, map_smul
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
b : R
h_1 :
  Membership.mem (γ := Submodule R R)
    (Ideal.radical (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M'')))) b
n : ℕ
hb : b ^ n • x ∈ f.range
neg : ∀ (y : M) (hy : (f : (a : M) → M') y = b ^ n • x), b ∈ p
⊢ b ∈ p

Tactic:
obtain ⟨y, hy⟩ := hb
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
b : R
h_1 :
  Membership.mem (γ := Submodule R R)
    (Ideal.radical (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M'')))) b
n : ℕ
y : M
hy : (f : (a : M) → M') y = b ^ n • x
neg : ∀ (H : b ∉ p), False
⊢ b ∈ p

Tactic:
by_contra H
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
b : R
h_1 :
  Membership.mem (γ := Submodule R R)
    (Ideal.radical (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M'')))) b
n : ℕ
y : M
hy : (f : (a : M) → M') y = b ^ n • x
H : b ∉ p
⊢ False

Tactic:
h b H y n hy
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
b : R
h_1 :
  Membership.mem (γ := Submodule R R)
    (Ideal.radical (colon (M := M'') ⊥ (singleton (α := M'') ((g : (a : M') → M'') x : M'')))) b
n : ℕ
y : M
hy : (f : (a : M) → M') y = b ^ n • x
H : b ∉ p
⊢ False

Tactic:
exact h b H y n hy
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
⊢ Eq (α := Set (Ideal R)) (associatedPrimes R (M × M')) (associatedPrimes R M ∪ associatedPrimes R M')

Tactic:
(subset_union_of_exact LinearMap.inl_injective .inl_snd).antisymm (Set.union_subset_iff.2
    ⟨subset_of_injective LinearMap.inl_injective, subset_of_injective LinearMap.inr_injective⟩)

Premises used: Iff.mpr, LinearMap.inl_injective, Set.union_subset_iff, LinearMap.inr_injective, associatedPrimes.subset_of_injective, HasSubset.Subset.antisymm, And.intro, associatedPrimes.subset_union_of_exact, Function.Exact.inl_snd
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
l : M ≃ₗ[R] M'
⊢ Eq (α := Set (Ideal R)) (associatedPrimes R M) (associatedPrimes R M')

Tactic:
le_antisymm (associatedPrimes.subset_of_injective l.injective)
    (associatedPrimes.subset_of_injective l.symm.injective)

Premises used: LinearEquiv.symm, associatedPrimes.subset_of_injective, le_antisymm, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Subsingleton M
h :
  ∀ (x : Ideal R),
    Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) x ↔ Membership.mem (γ := Set (Ideal R)) ∅ x
⊢ Eq (α := Set (Ideal R)) (associatedPrimes R M) ∅

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Subsingleton M
x : Ideal R
h : x ∉ associatedPrimes R M
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) x ↔ Membership.mem (γ := Set (Ideal R)) ∅ x

Tactic:
simp only [Set.mem_empty_iff_false, iff_false]

Premises used: iff_false, Set.mem_empty_iff_false
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Subsingleton M
x : Ideal R
⊢ x ∉ associatedPrimes R M

Tactic:
apply not_isAssociatedPrime_of_subsingleton

Premises used: not_isAssociatedPrime_of_subsingleton
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Nontrivial M
obtain : ∀ (x : M) (hx : x ≠ 0), Set.Nonempty (α := Ideal R) (associatedPrimes R M)
⊢ Set.Nonempty (α := Ideal R) (associatedPrimes R M)

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : M)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Nontrivial M
x : M
hx : x ≠ 0
obtain :
  ∀ (P : Ideal R) (hP : IsAssociatedPrime P M),
    colon (M := M) ⊥ {x} ≤ P → Set.Nonempty (α := Ideal R) (associatedPrimes R M)
⊢ Set.Nonempty (α := Ideal R) (associatedPrimes R M)

Tactic:
obtain ⟨P, hP, _⟩ := exists_le_isAssociatedPrime_of_isNoetherianRing R x hx

Premises used: exists_le_isAssociatedPrime_of_isNoetherianRing
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Nontrivial M
x : M
hx : x ≠ 0
P : Ideal R
hP : IsAssociatedPrime P M
right : colon (M := M) ⊥ {x} ≤ P
⊢ Set.Nonempty (α := Ideal R) (associatedPrimes R M)

Tactic:
⟨P, hP⟩

Premises used: Set.Nonempty, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Nontrivial M
x : M
hx : x ≠ 0
P : Ideal R
hP : IsAssociatedPrime P M
right : colon (M := M) ⊥ {x} ≤ P
⊢ Set.Nonempty (α := Ideal R) (associatedPrimes R M)

Tactic:
exact ⟨P, hP⟩
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
simp :
  Eq.{u_1 + 1} (α := Set R) (⋃ (p : Ideal R), ⋃ (_ : p.IsPrime ∧ ∃ (x : M), p = colon (M := M) ⊥ {x}), (↑p : Set R))
    {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0}
⊢ Eq.{u_1 + 1} (α := Set R)
    (⋃ (p : Ideal R), ⋃ (_ : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p), (↑p : Set R))
    {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0}

Tactic:
simp only [AssociatedPrimes.mem_iff, isAssociatedPrime_iff]

Premises used: AssociatedPrimes.mem_iff, isAssociatedPrime_iff
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
⊢ Eq.{u_1 + 1} (α := Set R) (⋃ (p : Ideal R), ⋃ (_ : p.IsPrime ∧ ∃ (x : M), p = colon (M := M) ⊥ {x}), (↑p : Set R))
    {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0}

Tactic:
subset_antisymm (Set.iUnion₂_subset ?_) ?_

Premises used: Set.iUnion₂_subset, subset_antisymm
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
refine_1 :
  ∀ (i : Ideal R) (j : i.IsPrime ∧ ∃ (x : M), i = colon (M := M) ⊥ {x}),
    (↑i : Set R) ⊆ {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0}
refine_2 :
  Subset.{u_1} (α := Set R) {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0}
    (⋃ (p : Ideal R), ⋃ (_ : p.IsPrime ∧ ∃ (x : M), p = colon (M := M) ⊥ {x}), (↑p : Set R))
⊢ Eq.{u_1 + 1} (α := Set R) (⋃ (p : Ideal R), ⋃ (_ : p.IsPrime ∧ ∃ (x : M), p = colon (M := M) ⊥ {x}), (↑p : Set R))
    {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0}

Tactic:
refine subset_antisymm (Set.iUnion₂_subset ?_) ?_

Premises used: Set.iUnion₂_subset, subset_antisymm
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
x : M
h : Ideal.IsPrime.{u_1} (α := R) (colon (M := M) ⊥ {x})
r : R
h' : r ∈ (↑(colon (M := M) ⊥ {x}) : Set R)
⊢ x ≠ 0

Tactic:
simpa using h.ne_top

Premises used: Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
x : M
h : Ideal.IsPrime.{u_1} (α := R) (colon (M := M) ⊥ {x})
r : R
h' : r ∈ (↑(colon (M := M) ⊥ {x}) : Set R)
⊢ r • x = 0

Tactic:
simpa using h'
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
x : M
h : Ideal.IsPrime.{u_1} (α := R) (colon (M := M) ⊥ {x})
r : R
h' : r ∈ (↑(colon (M := M) ⊥ {x}) : Set R)
⊢ Membership.mem (γ := Set R) {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0} r

Tactic:
exact ⟨x, by simpa using h.ne_top, by simpa using h'⟩
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
r : R
refine_2 :
  ∀ (x : M) (h : x ≠ 0) (h' : r • x = 0),
    Membership.mem (γ := Set R) (⋃ (p : Ideal R), ⋃ (_ : p.IsPrime ∧ ∃ (x : M), p = colon (M := M) ⊥ {x}), (↑p : Set R))
      r
⊢ Membership.mem (γ := Set R) {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0} r →
    Membership.mem (γ := Set R) (⋃ (p : Ideal R), ⋃ (_ : p.IsPrime ∧ ∃ (x : M), p = colon (M := M) ⊥ {x}), (↑p : Set R))
      r

Tactic:
⟨x, h, h'⟩
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
r : R
x : M
h : x ≠ 0
h' : r • x = 0
refine_2 :
  ∀ (P : Ideal R) (hP : IsAssociatedPrime P M) (hx : colon (M := M) ⊥ {x} ≤ P),
    Membership.mem (γ := Set R) (⋃ (p : Ideal R), ⋃ (_ : p.IsPrime ∧ ∃ (x : M), p = colon (M := M) ⊥ {x}), (↑p : Set R))
      r
⊢ Membership.mem (γ := Set R) (⋃ (p : Ideal R), ⋃ (_ : p.IsPrime ∧ ∃ (x : M), p = colon (M := M) ⊥ {x}), (↑p : Set R)) r

Tactic:
obtain ⟨P, hP, hx⟩ := exists_le_isAssociatedPrime_of_isNoetherianRing R x h

Premises used: exists_le_isAssociatedPrime_of_isNoetherianRing
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
r : R
x : M
h : x ≠ 0
h' : r • x = 0
P : Ideal R
hP : IsAssociatedPrime P M
hx : colon (M := M) ⊥ {x} ≤ P
⊢ P.IsPrime ∧ ∃ (x : M), P = colon (M := M) ⊥ {x}

Tactic:
rw [isAssociatedPrime_iff] at hP

Premises used: isAssociatedPrime_iff
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
r : R
x : M
h : x ≠ 0
h' : r • x = 0
P : Ideal R
hP : IsAssociatedPrime P M
hx : colon (M := M) ⊥ {x} ≤ P
hP₁ : P.IsPrime ∧ ∃ (x : M), P = colon (M := M) ⊥ {x}
⊢ colon (M := M) ⊥ {x} ≤ P

Tactic:
rw [isAssociatedPrime_iff] at hP

Premises used: isAssociatedPrime_iff
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
r : R
x : M
h : x ≠ 0
h' : r • x = 0
P : Ideal R
hP : P.IsPrime ∧ ∃ (x : M), P = colon (M := M) ⊥ {x}
hx : colon (M := M) ⊥ {x} ≤ P
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Submodule R M) ⊥ (r • x)
⊢ Membership.mem (γ := Submodule R R) (colon (M := M) ⊥ {x}) r

Tactic:
rwa [mem_colon_singleton]

Premises used: Submodule.mem_colon_singleton
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
r : R
x : M
h : x ≠ 0
h' : r • x = 0
P : Ideal R
hP : P.IsPrime ∧ ∃ (x : M), P = colon (M := M) ⊥ {x}
hx : colon (M := M) ⊥ {x} ≤ P
⊢ Membership.mem (γ := Set R) (⋃ (p : Ideal R), ⋃ (_ : p.IsPrime ∧ ∃ (x : M), p = colon (M := M) ⊥ {x}), (↑p : Set R)) r

Tactic:
exact Set.mem_iUnion₂_of_mem hP (hx (by rwa [mem_colon_singleton]))

Premises used: Set.mem_iUnion₂_of_mem
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsNoetherianRing R
h :
  ∀ (x : R), Membership.mem (γ := Set R) {r : R | ∃ (x : R), x ≠ 0 ∧ r • x = 0} x ↔ x ∈ (↑(nonZeroDivisors R) : Set R)ᶜ
⊢ {r : R | ∃ (x : R), x ≠ 0 ∧ r • x = 0} = (↑(nonZeroDivisors R) : Set R)ᶜ

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsNoetherianRing R
x : R
⊢ Membership.mem (γ := Set R) {r : R | ∃ (x : R), x ≠ 0 ∧ r • x = 0} x ↔ x ∈ (↑(nonZeroDivisors R) : Set R)ᶜ

Tactic:
simp [← nonZeroDivisorsLeft_eq_nonZeroDivisors, and_comm]

Premises used: nonZeroDivisorsLeft_eq_nonZeroDivisors, and_comm
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : IsAssociatedPrime I M
obtain :
  ∀ (x : M) (hI : Ideal.IsPrime.{u_1} (α := R) (Ideal.radical (colon (M := M) ⊥ {x}))),
    LE.le.{u_1} (α := Ideal R) (annihilator.{u_1, u_2} (M := M) ⊤) (Ideal.radical (colon (M := M) ⊥ {x}))
⊢ annihilator.{u_1, u_2} (M := M) ⊤ ≤ I

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

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
hI : Ideal.IsPrime.{u_1} (α := R) (Ideal.radical (colon (M := M) ⊥ {x}))
rw : LE.le (α := Ideal R) (annihilator.{u_1, u_2} (M := M) ⊤) (Ideal.radical (annihilator (M := M) (R ∙ x)))
⊢ LE.le.{u_1} (α := Ideal R) (annihilator.{u_1, u_2} (M := M) ⊤) (Ideal.radical (colon (M := M) ⊥ {x}))

Tactic:
rw [bot_colon']

Premises used: Submodule.bot_colon'
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
hI : Ideal.IsPrime.{u_1} (α := R) (Ideal.radical (colon (M := M) ⊥ {x}))
⊢ LE.le (α := Ideal R) (annihilator.{u_1, u_2} (M := M) ⊤) (Ideal.radical (annihilator (M := M) (R ∙ x)))

Tactic:
(annihilator_mono le_top).trans Ideal.le_radical

Premises used: Set.Mem, Ideal.le_radical, Submodule.annihilator_mono, le_top, LE.le.trans