case intro.intro
R : Type u_2
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.27644
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
hI : Ideal.IsPrime I
x : M
hx : I = Submodule.annihilator (Submodule.span R {x})
⊢ False
R : Type u_2
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.27644
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
⊢ ¬IsAssociatedPrime I M
rintro ⟨hI, x, hx⟩
case intro.intro
R : Type u_2
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.27644
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
hI : Ideal.IsPrime I
x : M
hx : I = Submodule.annihilator (Submodule.span R {x})
⊢ I = ⊤
case intro.intro
R : Type u_2
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.27644
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
hI : Ideal.IsPrime I
x : M
hx : I = Submodule.annihilator (Submodule.span R {x})
⊢ False
apply hI.ne_top
no goals
case intro.intro
R : Type u_2
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.27644
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
hI : Ideal.IsPrime I
x : M
hx : I = Submodule.annihilator (Submodule.span R {x})
⊢ I = ⊤
rwa [Subsingleton.elim x 0, Submodule.span_singleton_eq_bot.mpr rfl, Submodule.annihilator_bot]
  at hx