case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R ⧸ I
e : J = Submodule.annihilator (Submodule.span R {x})
⊢ J = Ideal.radical I
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
h : IsAssociatedPrime J (R ⧸ I)
⊢ J = Ideal.radical I
obtain ⟨hJ, x, e⟩ := h
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R ⧸ I
e : J = Submodule.annihilator (Submodule.span R {x})
this : x ≠ 0
⊢ J = Ideal.radical I
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R ⧸ I
e : J = Submodule.annihilator (Submodule.span R {x})
⊢ J = Ideal.radical I
have : x ≠ 0 := by
  rintro rfl
  apply hJ.1
  rwa [Submodule.span_singleton_eq_bot.mpr rfl, Submodule.annihilator_bot] at e
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
e : J = Submodule.annihilator (Submodule.span R {↑(Ideal.Quotient.mkₐ R I) x})
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
⊢ J = Ideal.radical I
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R ⧸ I
e : J = Submodule.annihilator (Submodule.span R {x})
this : x ≠ 0
⊢ J = Ideal.radical I
obtain ⟨x, rfl⟩ := Ideal.Quotient.mkₐ_surjective R _ x
case e
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
e : J = Submodule.annihilator (Submodule.span R {↑(Ideal.Quotient.mkₐ R I) x})
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
⊢ ∀ {y : R}, y ∈ J ↔ x * y ∈ I

case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ J = Ideal.radical I
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
e : J = Submodule.annihilator (Submodule.span R {↑(Ideal.Quotient.mkₐ R I) x})
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
⊢ J = Ideal.radical I
replace e : ∀ {y}, y ∈ J ↔ x * y ∈ I
case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ J ≤ Ideal.radical I

case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ Ideal.radical I ≤ J
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ J = Ideal.radical I
apply le_antisymm
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
e : J = Submodule.annihilator (Submodule.span R {0})
⊢ False
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R ⧸ I
e : J = Submodule.annihilator (Submodule.span R {x})
⊢ x ≠ 0
rintro rfl
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
e : J = Submodule.annihilator (Submodule.span R {0})
⊢ J = ⊤
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
e : J = Submodule.annihilator (Submodule.span R {0})
⊢ False
apply hJ.1
no goals
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
e : J = Submodule.annihilator (Submodule.span R {0})
⊢ J = ⊤
rwa [Submodule.span_singleton_eq_bot.mpr rfl, Submodule.annihilator_bot] at e
case e
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
e : J = Submodule.annihilator (Submodule.span R {↑(Ideal.Quotient.mkₐ R I) x})
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
y : R
⊢ y ∈ J ↔ x * y ∈ I
case e
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
e : J = Submodule.annihilator (Submodule.span R {↑(Ideal.Quotient.mkₐ R I) x})
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
⊢ ∀ {y : R}, y ∈ J ↔ x * y ∈ I
intro y
no goals
case e
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
e : J = Submodule.annihilator (Submodule.span R {↑(Ideal.Quotient.mkₐ R I) x})
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
y : R
⊢ y ∈ J ↔ x * y ∈ I
rw [e, Submodule.mem_annihilator_span_singleton, ← map_smul, smul_eq_mul, mul_comm,
  Ideal.Quotient.mkₐ_eq_mk, ← Ideal.Quotient.mk_eq_mk, Submodule.Quotient.mk_eq_zero]
case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
y : R
hy : y ∈ J
⊢ y ∈ Ideal.radical I
case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ J ≤ Ideal.radical I
intro y hy
no goals
case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
y : R
hy : y ∈ J
⊢ y ∈ Ideal.radical I
exact (hI.2 <| e.mp hy).resolve_left ((Submodule.Quotient.mk_eq_zero I).not.mp this)
case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ I ≤ J
case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ Ideal.radical I ≤ J
rw [hJ.radical_le_iff]
case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
y : R
hy : y ∈ I
⊢ y ∈ J
case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ I ≤ J
intro y hy
no goals
case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type ?u.74241
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type ?u.74774
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
y : R
hy : y ∈ I
⊢ y ∈ J
exact e.mpr (I.mul_mem_left x hy)