-- Mathlib/RingTheory/Ideal/AssociatedPrime.lean
theorem biUnion_associatedPrimes_eq_zero_divisors [IsNoetherianRing R] :
    ⋃ p ∈ associatedPrimes R M, p = { r : R | ∃ x : M, x ≠ 0 ∧ r • x = 0 }

Proof state:
case refine_2
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
r : R
x : M
h : x ≠ 0
h' : r • x = 0
⊢ r ∈ ⋃ p ∈ associatedPrimes R M, ↑p

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

Result:
case refine_2.intro.intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
r : R
x : M
h : x ≠ 0
h' : r • x = 0
P : Ideal R
hP : IsAssociatedPrime P M
hx : ker (toSpanSingleton R M x) ≤ P
⊢ r ∈ ⋃ p ∈ associatedPrimes R M, ↑p

Proof state:
case refine_2.intro.intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
r : R
x : M
h : x ≠ 0
h' : r • x = 0
P : Ideal R
hP : IsAssociatedPrime P M
hx : ker (toSpanSingleton R M x) ≤ P
⊢ r ∈ ⋃ p ∈ associatedPrimes R M, ↑p

Tactic:
exact Set.mem_biUnion hP (hx h')

Result:
no goals

Proof state:
case refine_1
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
⊢ ∀ i ∈ associatedPrimes R M, ↑i ⊆ {r | ∃ x, x ≠ 0 ∧ r • x = 0}

Tactic:
rintro _ ⟨h, x, ⟨⟩⟩ r h'

Result:
case refine_1.intro.intro.refl
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
x : M
h : Ideal.IsPrime (ker (toSpanSingleton R M x))
r : R
h' : r ∈ ↑(ker (toSpanSingleton R M x))
⊢ r ∈ {r | ∃ x, x ≠ 0 ∧ r • x = 0}

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
⊢ ⋃ p ∈ associatedPrimes R M, ↑p = {r | ∃ x, x ≠ 0 ∧ r • x = 0}

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

Result:
case refine_1
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
⊢ ∀ i ∈ associatedPrimes R M, ↑i ⊆ {r | ∃ x, x ≠ 0 ∧ r • x = 0}

case refine_2
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
⊢ {r | ∃ x, x ≠ 0 ∧ r • x = 0} ⊆ ⋃ p ∈ associatedPrimes R M, ↑p

Proof state:
case refine_1.intro.intro.refl
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
x : M
h : Ideal.IsPrime (ker (toSpanSingleton R M x))
r : R
h' : r ∈ ↑(ker (toSpanSingleton R M x))
⊢ 1 • x ≠ 0

Tactic:
exact (Ideal.ne_top_iff_one _).mp h.ne_top

Result:
no goals

Proof state:
case refine_1.intro.intro.refl
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
x : M
h : Ideal.IsPrime (ker (toSpanSingleton R M x))
r : R
h' : r ∈ ↑(ker (toSpanSingleton R M x))
⊢ r ∈ {r | ∃ x, x ≠ 0 ∧ r • x = 0}

Tactic:
refine ⟨x, ne_of_eq_of_ne (one_smul R x).symm ?_, h'⟩

Result:
case refine_1.intro.intro.refl
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
x : M
h : Ideal.IsPrime (ker (toSpanSingleton R M x))
r : R
h' : r ∈ ↑(ker (toSpanSingleton R M x))
⊢ 1 • x ≠ 0

Proof state:
case refine_2
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
⊢ {r | ∃ x, x ≠ 0 ∧ r • x = 0} ⊆ ⋃ p ∈ associatedPrimes R M, ↑p

Tactic:
intro r ⟨x, h, h'⟩

Result:
case refine_2
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
r : R
x : M
h : x ≠ 0
h' : r • x = 0
⊢ r ∈ ⋃ p ∈ associatedPrimes R M, ↑p