-- Mathlib/RingTheory/Jacobson/Ideal.lean
theorem radical_eq_jacobson_iff_radical_quotient_eq_jacobson_bot :
    I.radical = I.jacobson ↔ radical (⊥ : Ideal (R ⧸ I)) = jacobson ⊥

Proof state:
case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : ⊥.radical = ⊥.jacobson
⊢ I.radical = I.jacobson

Tactic:
have := congr_arg (comap (Ideal.Quotient.mk I)) h

Result:
case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : ⊥.radical = ⊥.jacobson
this : comap (Quotient.mk I) ⊥.radical = comap (Quotient.mk I) ⊥.jacobson
⊢ I.radical = I.jacobson

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ I.radical = I.jacobson ↔ ⊥.radical = ⊥.jacobson

Tactic:
have hf : Function.Surjective (Ideal.Quotient.mk I) := Submodule.Quotient.mk_surjective I

Result:
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
⊢ I.radical = I.jacobson ↔ ⊥.radical = ⊥.jacobson

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
⊢ I.radical = I.jacobson ↔ ⊥.radical = ⊥.jacobson

Tactic:
constructor

Result:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
⊢ I.radical = I.jacobson → ⊥.radical = ⊥.jacobson

case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
⊢ ⊥.radical = ⊥.jacobson → I.radical = I.jacobson

Proof state:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : I.radical = I.jacobson
this : (map (Quotient.mk I) I).radical = (map (Quotient.mk I) I).jacobson
⊢ ⊥.radical = ⊥.jacobson

Tactic:
simpa using this

Result:
no goals

Proof state:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : I.radical = I.jacobson
this : map (Quotient.mk I) I.radical = map (Quotient.mk I) I.jacobson
⊢ ⊥.radical = ⊥.jacobson

Tactic:
rw [map_radical_of_surjective hf (le_of_eq mk_ker),
  map_jacobson_of_surjective hf (le_of_eq mk_ker)] at this

Result:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : I.radical = I.jacobson
this : (map (Quotient.mk I) I).radical = (map (Quotient.mk I) I).jacobson
⊢ ⊥.radical = ⊥.jacobson

Proof state:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
⊢ I.radical = I.jacobson → ⊥.radical = ⊥.jacobson

Tactic:
intro h

Result:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : I.radical = I.jacobson
⊢ ⊥.radical = ⊥.jacobson

Proof state:
case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
⊢ ⊥.radical = ⊥.jacobson → I.radical = I.jacobson

Tactic:
intro h

Result:
case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : ⊥.radical = ⊥.jacobson
⊢ I.radical = I.jacobson

Proof state:
case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : ⊥.radical = ⊥.jacobson
this : comap (Quotient.mk I) ⊥.radical = comap (Quotient.mk I) ⊥.jacobson
⊢ I.radical = I.jacobson

Tactic:
rw [comap_radical, comap_jacobson_of_surjective hf,
  ← RingHom.ker_eq_comap_bot (Ideal.Quotient.mk I)] at this

Result:
case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : ⊥.radical = ⊥.jacobson
this : (RingHom.ker (Quotient.mk I)).radical = (RingHom.ker (Quotient.mk I)).jacobson
⊢ I.radical = I.jacobson

Proof state:
case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : ⊥.radical = ⊥.jacobson
this : (RingHom.ker (Quotient.mk I)).radical = (RingHom.ker (Quotient.mk I)).jacobson
⊢ I.radical = I.jacobson

Tactic:
simpa using this

Result:
no goals

Proof state:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : I.radical = I.jacobson
⊢ ⊥.radical = ⊥.jacobson

Tactic:
have := congr_arg (map (Ideal.Quotient.mk I)) h

Result:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : I.radical = I.jacobson
this : map (Quotient.mk I) I.radical = map (Quotient.mk I) I.jacobson
⊢ ⊥.radical = ⊥.jacobson