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

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

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

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

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

Tactic:
replace h := congr_arg (Ideal.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 : map (Quotient.mk I) I.jacobson = map (Quotient.mk I) I
⊢ ⊥.jacobson = ⊥

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

Tactic:
simpa using h

Result:
no goals

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

Tactic:
simpa using h

Result:
no goals

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

Tactic:
intro h

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

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ I.jacobson = I ↔ ⊥.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.jacobson = I ↔ ⊥.jacobson = ⊥

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

Tactic:
intro h

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

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

Tactic:
constructor

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

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

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

Tactic:
replace h := 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 : comap (Quotient.mk I) ⊥.jacobson = comap (Quotient.mk I) ⊥
⊢ I.jacobson = I

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

Tactic:
rw [map_jacobson_of_surjective hf (le_of_eq mk_ker)] at h

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