case 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_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ↑f
x : M
h : IsAssociatedPrime (Submodule.annihilator (Submodule.span R {x})) M
⊢ IsAssociatedPrime (Submodule.annihilator (Submodule.span R {x})) M'
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_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : IsAssociatedPrime I M
hf : Function.Injective ↑f
⊢ IsAssociatedPrime I M'
obtain ⟨x, rfl⟩ := h.2
case 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_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ↑f
x : M
h : IsAssociatedPrime (Submodule.annihilator (Submodule.span R {x})) M
⊢ Submodule.annihilator (Submodule.span R {x}) = Submodule.annihilator (Submodule.span R {↑f x})
case 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_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ↑f
x : M
h : IsAssociatedPrime (Submodule.annihilator (Submodule.span R {x})) M
⊢ IsAssociatedPrime (Submodule.annihilator (Submodule.span R {x})) M'
refine' ⟨h.1, ⟨f x, _⟩⟩
case intro.h
R : Type u_1
inst✝⁴ : CommRing R
J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ↑f
x : M
h : IsAssociatedPrime (Submodule.annihilator (Submodule.span R {x})) M
r : R
⊢ r ∈ Submodule.annihilator (Submodule.span R {x}) ↔ r ∈ Submodule.annihilator (Submodule.span R {↑f x})
case 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_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ↑f
x : M
h : IsAssociatedPrime (Submodule.annihilator (Submodule.span R {x})) M
⊢ Submodule.annihilator (Submodule.span R {x}) = Submodule.annihilator (Submodule.span R {↑f x})
ext r
no goals
case intro.h
R : Type u_1
inst✝⁴ : CommRing R
J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ↑f
x : M
h : IsAssociatedPrime (Submodule.annihilator (Submodule.span R {x})) M
r : R
⊢ r ∈ Submodule.annihilator (Submodule.span R {x}) ↔ r ∈ Submodule.annihilator (Submodule.span R {↑f x})
rw [Submodule.mem_annihilator_span_singleton, Submodule.mem_annihilator_span_singleton, ←
  map_smul, ← f.map_zero, hf.eq_iff]