R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
⊢ radical I = jacobson I ↔ radical ⊥ = jacobson ⊥
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
⊢ radical I = jacobson I ↔ radical ⊥ = jacobson ⊥
have hf : Function.Surjective (Ideal.Quotient.mk I) := Submodule.Quotient.mk_surjective I
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
⊢ radical I = jacobson I → radical ⊥ = jacobson ⊥

case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
⊢ radical ⊥ = jacobson ⊥ → radical I = jacobson I
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
⊢ radical I = jacobson I ↔ radical ⊥ = jacobson ⊥
constructor
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : radical I = jacobson I
⊢ radical ⊥ = jacobson ⊥
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
⊢ radical I = jacobson I → radical ⊥ = jacobson ⊥
intro h
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : radical I = jacobson I
this : map (Quotient.mk I) (radical I) = map (Quotient.mk I) (jacobson I)
⊢ radical ⊥ = jacobson ⊥
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : radical I = jacobson I
⊢ radical ⊥ = jacobson ⊥
have := congr_arg (map (Ideal.Quotient.mk I)) h
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : radical I = jacobson I
this : radical (map (Quotient.mk I) I) = jacobson (map (Quotient.mk I) I)
⊢ radical ⊥ = jacobson ⊥
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : radical I = jacobson I
this : map (Quotient.mk I) (radical I) = map (Quotient.mk I) (jacobson I)
⊢ radical ⊥ = jacobson ⊥
rw [map_radical_of_surjective hf (le_of_eq mk_ker),
  map_jacobson_of_surjective hf (le_of_eq mk_ker)] at this
no goals
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : radical I = jacobson I
this : radical (map (Quotient.mk I) I) = jacobson (map (Quotient.mk I) I)
⊢ radical ⊥ = jacobson ⊥
simpa using this
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : radical ⊥ = jacobson ⊥
⊢ radical I = jacobson I
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
⊢ radical ⊥ = jacobson ⊥ → radical I = jacobson I
intro h
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : radical ⊥ = jacobson ⊥
this : comap (Quotient.mk I) (radical ⊥) = comap (Quotient.mk I) (jacobson ⊥)
⊢ radical I = jacobson I
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : radical ⊥ = jacobson ⊥
⊢ radical I = jacobson I
have := congr_arg (comap (Ideal.Quotient.mk I)) h
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : radical ⊥ = jacobson ⊥
this : radical (RingHom.ker (Quotient.mk I)) = jacobson (RingHom.ker (Quotient.mk I))
⊢ radical I = jacobson I
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : radical ⊥ = jacobson ⊥
this : comap (Quotient.mk I) (radical ⊥) = comap (Quotient.mk I) (jacobson ⊥)
⊢ radical I = jacobson I
rw [comap_radical, comap_jacobson_of_surjective hf,
  ← RingHom.ker_eq_comap_bot (Ideal.Quotient.mk I)] at this
no goals
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : radical ⊥ = jacobson ⊥
this : radical (RingHom.ker (Quotient.mk I)) = jacobson (RingHom.ker (Quotient.mk I))
⊢ radical I = jacobson I
simpa using this