-- Mathlib/RingTheory/Ideal/AssociatedPrime.lean
theorem IsAssociatedPrime.eq_radical (hI : I.IsPrimary) (h : IsAssociatedPrime J (R ⧸ I)) :
    J = I.radical

Proof state:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R ⧸ I
e : J = ker (toSpanSingleton R (R ⧸ I) x)
⊢ x ≠ 0

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
e : J = ker (toSpanSingleton R (R ⧸ I) 0)
⊢ False

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R ⧸ I
e : J = ker (toSpanSingleton R (R ⧸ I) x)
⊢ J = I.radical

Tactic:
have : x ≠ 0 := by
  rintro rfl
  apply hJ.1
  rwa [toSpanSingleton_zero, ker_zero] at e

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R ⧸ I
e : J = ker (toSpanSingleton R (R ⧸ I) x)
this : x ≠ 0
⊢ J = I.radical

Proof state:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
e : J = ker (toSpanSingleton R (R ⧸ I) 0)
⊢ False

Tactic:
apply hJ.1

Result:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
e : J = ker (toSpanSingleton R (R ⧸ I) 0)
⊢ J = ⊤

Proof state:
case intro.intro.intro.a
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
this : (Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ J ≤ I.radical

Tactic:
intro y hy

Result:
case intro.intro.intro.a
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
this : (Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
y : R
hy : y ∈ J
⊢ y ∈ I.radical

Proof state:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e : J = ker (toSpanSingleton R (R ⧸ I) ((Ideal.Quotient.mkₐ R I) x))
this : (Ideal.Quotient.mkₐ R I) x ≠ 0
⊢ ∀ {y : R}, y ∈ J ↔ x * y ∈ I

Tactic:
intro y

Result:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e : J = ker (toSpanSingleton R (R ⧸ I) ((Ideal.Quotient.mkₐ R I) x))
this : (Ideal.Quotient.mkₐ R I) x ≠ 0
y : R
⊢ y ∈ J ↔ x * y ∈ I

Proof state:
case intro.intro.intro
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e : J = ker (toSpanSingleton R (R ⧸ I) ((Ideal.Quotient.mkₐ R I) x))
this : (Ideal.Quotient.mkₐ R I) x ≠ 0
⊢ J = I.radical

Tactic:
replace e : ∀ {y}, y ∈ J ↔ x * y ∈ I := by
  intro y
  rw [e, mem_ker, toSpanSingleton_apply, ← map_smul, smul_eq_mul, mul_comm,
    Ideal.Quotient.mkₐ_eq_mk, ← Ideal.Quotient.mk_eq_mk, Submodule.Quotient.mk_eq_zero]

Result:
case intro.intro.intro
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
this : (Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ J = I.radical

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R ⧸ I
e : J = ker (toSpanSingleton R (R ⧸ I) x)
this : x ≠ 0
⊢ J = I.radical

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mkₐ_surjective R _ x

Result:
case intro.intro.intro
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e : J = ker (toSpanSingleton R (R ⧸ I) ((Ideal.Quotient.mkₐ R I) x))
this : (Ideal.Quotient.mkₐ R I) x ≠ 0
⊢ J = I.radical

Proof state:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
h : IsAssociatedPrime J (R ⧸ I)
⊢ J = I.radical

Tactic:
obtain ⟨hJ, x, e⟩ := h

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R ⧸ I
e : J = ker (toSpanSingleton R (R ⧸ I) x)
⊢ J = I.radical

Proof state:
case intro.intro.intro.a
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
this : (Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
y : R
hy : y ∈ J
⊢ y ∈ I.radical

Tactic:
exact ((Ideal.isPrimary_iff.1 hI).2 <| e.mp hy).resolve_left
  ((Submodule.Quotient.mk_eq_zero I).not.mp this)

Result:
no goals

Proof state:
case intro.intro.intro
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
this : (Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ J = I.radical

Tactic:
apply le_antisymm

Result:
case intro.intro.intro.a
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
this : (Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ J ≤ I.radical

case intro.intro.intro.a
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
this : (Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ I.radical ≤ J

Proof state:
case intro.intro.intro.a
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
this : (Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ I ≤ J

Tactic:
intro y hy

Result:
case intro.intro.intro.a
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
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

Proof state:
case intro.intro.intro.a
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
this : (Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ I.radical ≤ J

Tactic:
rw [hJ.radical_le_iff]

Result:
case intro.intro.intro.a
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
this : (Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ I ≤ J

Proof state:
case intro.intro.intro.a
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
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

Tactic:
exact e.mpr (I.mul_mem_left x hy)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e : J = ker (toSpanSingleton R (R ⧸ I) ((Ideal.Quotient.mkₐ R I) x))
this : (Ideal.Quotient.mkₐ R I) x ≠ 0
y : R
⊢ y ∈ J ↔ x * y ∈ I

Tactic:
rw [e, mem_ker, toSpanSingleton_apply, ← map_smul, smul_eq_mul, mul_comm,
  Ideal.Quotient.mkₐ_eq_mk, ← Ideal.Quotient.mk_eq_mk, Submodule.Quotient.mk_eq_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
e : J = ker (toSpanSingleton R (R ⧸ I) 0)
⊢ J = ⊤

Tactic:
rwa [toSpanSingleton_zero, ker_zero] at e

Result:
no goals