-- Mathlib/RingTheory/Ideal/AssociatedPrime.lean
theorem exists_le_isAssociatedPrime_of_isNoetherianRing [H : IsNoetherianRing R] (x : M)
    (hx : x ≠ 0) : ∃ P : Ideal R, IsAssociatedPrime P M ∧ ker (toSpanSingleton R M x) ≤ P

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : ker (toSpanSingleton R M x) ≠ ⊤
⊢ ∃ P, IsAssociatedPrime P M ∧ ker (toSpanSingleton R M x) ≤ P

Tactic:
obtain ⟨P, ⟨l, h₁, y, rfl⟩, h₃⟩ :=
  set_has_maximal_iff_noetherian.mpr H
    { P | ker (toSpanSingleton R M x) ≤ P ∧ P ≠ ⊤ ∧ ∃ y : M, P = ker (toSpanSingleton R M y) }
    ⟨_, rfl.le, this, x, rfl⟩

Result:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : ker (toSpanSingleton R M x) ≠ ⊤
y : M
h₃ :
  ∀ I ∈ {P | ker (toSpanSingleton R M x) ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ker (toSpanSingleton R M y)},
    ¬ker (toSpanSingleton R M y) < I
l : ker (toSpanSingleton R M x) ≤ ker (toSpanSingleton R M y)
h₁ : ker (toSpanSingleton R M y) ≠ ⊤
⊢ ∃ P, IsAssociatedPrime P M ∧ ker (toSpanSingleton R M x) ≤ P

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : ker (toSpanSingleton R M x) ≠ ⊤
y : M
h₃ :
  ∀ I ∈ {P | ker (toSpanSingleton R M x) ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ker (toSpanSingleton R M y)},
    ¬ker (toSpanSingleton R M y) < I
l : ker (toSpanSingleton R M x) ≤ ker (toSpanSingleton R M y)
h₁ : ker (toSpanSingleton R M y) ≠ ⊤
⊢ ∃ P, IsAssociatedPrime P M ∧ ker (toSpanSingleton R M x) ≤ P

Tactic:
refine ⟨_, ⟨⟨h₁, ?_⟩, y, rfl⟩, l⟩

Result:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : ker (toSpanSingleton R M x) ≠ ⊤
y : M
h₃ :
  ∀ I ∈ {P | ker (toSpanSingleton R M x) ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ker (toSpanSingleton R M y)},
    ¬ker (toSpanSingleton R M y) < I
l : ker (toSpanSingleton R M x) ≤ ker (toSpanSingleton R M y)
h₁ : ker (toSpanSingleton R M y) ≠ ⊤
⊢ ∀ {x y_1 : R},
    x * y_1 ∈ ker (toSpanSingleton R M y) → x ∈ ker (toSpanSingleton R M y) ∨ y_1 ∈ ker (toSpanSingleton R M y)

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : ker (toSpanSingleton R M x) ≠ ⊤
y : M
h₃ :
  ∀ I ∈ {P | ker (toSpanSingleton R M x) ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ker (toSpanSingleton R M y)},
    ¬ker (toSpanSingleton R M y) < I
l : ker (toSpanSingleton R M x) ≤ ker (toSpanSingleton R M y)
h₁ : ker (toSpanSingleton R M y) ≠ ⊤
a b : R
hab : a * b ∈ ker (toSpanSingleton R M y)
⊢ a ∈ ker (toSpanSingleton R M y) ∨ b ∈ ker (toSpanSingleton R M y)

Tactic:
rw [or_iff_not_imp_left]

Result:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : ker (toSpanSingleton R M x) ≠ ⊤
y : M
h₃ :
  ∀ I ∈ {P | ker (toSpanSingleton R M x) ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ker (toSpanSingleton R M y)},
    ¬ker (toSpanSingleton R M y) < I
l : ker (toSpanSingleton R M x) ≤ ker (toSpanSingleton R M y)
h₁ : ker (toSpanSingleton R M y) ≠ ⊤
a b : R
hab : a * b ∈ ker (toSpanSingleton R M y)
⊢ a ∉ ker (toSpanSingleton R M y) → b ∈ ker (toSpanSingleton R M y)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : ker (toSpanSingleton R M x) ≠ ⊤
y : M
h₃ :
  ∀ I ∈ {P | ker (toSpanSingleton R M x) ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ker (toSpanSingleton R M y)},
    ¬ker (toSpanSingleton R M y) < I
l : ker (toSpanSingleton R M x) ≤ ker (toSpanSingleton R M y)
h₁ : ker (toSpanSingleton R M y) ≠ ⊤
a b : R
hab : (a * b) • y = 0
ha : ¬a • y = 0
c : R
hc : c ∈ ker (toSpanSingleton R M y)
⊢ c ∈ ker (toSpanSingleton R M (a • y))

Tactic:
rw [mem_ker, toSpanSingleton_apply] at hc ⊢

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : ker (toSpanSingleton R M x) ≠ ⊤
y : M
h₃ :
  ∀ I ∈ {P | ker (toSpanSingleton R M x) ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ker (toSpanSingleton R M y)},
    ¬ker (toSpanSingleton R M y) < I
l : ker (toSpanSingleton R M x) ≤ ker (toSpanSingleton R M y)
h₁ : ker (toSpanSingleton R M y) ≠ ⊤
a b : R
hab : (a * b) • y = 0
ha : ¬a • y = 0
c : R
hc : c • y = 0
⊢ c • a • y = 0

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : ker (toSpanSingleton R M x) ≠ ⊤
y : M
h₃ :
  ∀ I ∈ {P | ker (toSpanSingleton R M x) ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ker (toSpanSingleton R M y)},
    ¬ker (toSpanSingleton R M y) < I
l : ker (toSpanSingleton R M x) ≤ ker (toSpanSingleton R M y)
h₁ : ker (toSpanSingleton R M y) ≠ ⊤
a b : R
hab : a * b ∈ ker (toSpanSingleton R M y)
⊢ a ∉ ker (toSpanSingleton R M y) → b ∈ ker (toSpanSingleton R M y)

Tactic:
intro ha

Result:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : ker (toSpanSingleton R M x) ≠ ⊤
y : M
h₃ :
  ∀ I ∈ {P | ker (toSpanSingleton R M x) ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ker (toSpanSingleton R M y)},
    ¬ker (toSpanSingleton R M y) < I
l : ker (toSpanSingleton R M x) ≤ ker (toSpanSingleton R M y)
h₁ : ker (toSpanSingleton R M y) ≠ ⊤
a b : R
hab : a * b ∈ ker (toSpanSingleton R M y)
ha : a ∉ ker (toSpanSingleton R M y)
⊢ b ∈ ker (toSpanSingleton R M y)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : ker (toSpanSingleton R M x) ≠ ⊤
y : M
h₃ :
  ∀ I ∈ {P | ker (toSpanSingleton R M x) ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ker (toSpanSingleton R M y)},
    ¬ker (toSpanSingleton R M y) < I
l : ker (toSpanSingleton R M x) ≤ ker (toSpanSingleton R M y)
h₁ : ker (toSpanSingleton R M y) ≠ ⊤
a b : R
hab : (a * b) • y = 0
ha : ¬a • y = 0
H₁ : ker (toSpanSingleton R M y) ≤ ker (toSpanSingleton R M (a • y))
⊢ ker (toSpanSingleton R M (a • y)) ≠ ⊤

Tactic:
rwa [Ne, ker_eq_top, toSpanSingleton_eq_zero_iff]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : ker (toSpanSingleton R M x) ≠ ⊤
y : M
h₃ :
  ∀ I ∈ {P | ker (toSpanSingleton R M x) ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ker (toSpanSingleton R M y)},
    ¬ker (toSpanSingleton R M y) < I
l : ker (toSpanSingleton R M x) ≤ ker (toSpanSingleton R M y)
h₁ : ker (toSpanSingleton R M y) ≠ ⊤
a b : R
hab : a * b ∈ ker (toSpanSingleton R M y)
ha : a ∉ ker (toSpanSingleton R M y)
⊢ b ∈ ker (toSpanSingleton R M y)

Tactic:
rw [mem_ker, toSpanSingleton_apply] at ha hab

Result:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : ker (toSpanSingleton R M x) ≠ ⊤
y : M
h₃ :
  ∀ I ∈ {P | ker (toSpanSingleton R M x) ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ker (toSpanSingleton R M y)},
    ¬ker (toSpanSingleton R M y) < I
l : ker (toSpanSingleton R M x) ≤ ker (toSpanSingleton R M y)
h₁ : ker (toSpanSingleton R M y) ≠ ⊤
a b : R
hab : (a * b) • y = 0
ha : ¬a • y = 0
⊢ b ∈ ker (toSpanSingleton R M y)