case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.70734
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
x : M
hI : Ideal.IsPrime (Submodule.annihilator (Submodule.span R {x}))
⊢ Submodule.annihilator ⊤ ≤ Submodule.annihilator (Submodule.span R {x})
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.70734
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : IsAssociatedPrime I M
⊢ Submodule.annihilator ⊤ ≤ I
obtain ⟨hI, x, rfl⟩ := h
no goals
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.70734
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
x : M
hI : Ideal.IsPrime (Submodule.annihilator (Submodule.span R {x}))
⊢ Submodule.annihilator ⊤ ≤ Submodule.annihilator (Submodule.span R {x})
exact Submodule.annihilator_mono le_top