-- Mathlib/RingTheory/Ideal/Maps.lean
theorem map_radical_of_surjective {f : R →+* S} (hf : Function.Surjective f) {I : Ideal R}
    (h : RingHom.ker f ≤ I) : map f I.radical = (map f I).radical

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
⊢ map f (sInf {J | I ≤ J ∧ J.IsPrime}) = sInf {J | map f I ≤ J ∧ J.IsPrime}

Tactic:
have : ∀ J ∈ {J : Ideal R | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J := fun J hJ => h.trans hJ.left

Result:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
⊢ map f (sInf {J | I ≤ J ∧ J.IsPrime}) = sInf {J | map f I ≤ J ∧ J.IsPrime}

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
⊢ map f (sInf {J | I ≤ J ∧ J.IsPrime}) = sInf {J | map f I ≤ J ∧ J.IsPrime}

Tactic:
convert map_sInf hf this

Result:
case h.e'_3.h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
⊢ {J | map f I ≤ J ∧ J.IsPrime} = map f '' {J | I ≤ J ∧ J.IsPrime}

Proof state:
case h.e'_3.h.e'_3.refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
⊢ (map f '' {J | I ≤ J ∧ J.IsPrime}) j → {J | map f I ≤ J ∧ J.IsPrime} j

Tactic:
rintro ⟨J, ⟨hJ, hJ'⟩⟩

Result:
case h.e'_3.h.e'_3.refine_2.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsPrime}
hJ' : map f J = j
⊢ {J | map f I ≤ J ∧ J.IsPrime} j

Proof state:
case h.e'_3.h.e'_3.refine_1.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this✝ : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
hj : map f I ≤ j
hj' this : j.IsPrime
⊢ (map f '' {J | I ≤ J ∧ J.IsPrime}) j

Tactic:
exact
  ⟨comap f j, ⟨⟨map_le_iff_le_comap.1 hj, comap_isPrime f j⟩, map_comap_of_surjective f hf j⟩⟩

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
⊢ map f I.radical = (map f I).radical

Tactic:
rw [radical_eq_sInf, radical_eq_sInf]

Result:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
⊢ map f (sInf {J | I ≤ J ∧ J.IsPrime}) = sInf {J | map f I ≤ J ∧ J.IsPrime}

Proof state:
case h.e'_3.h.e'_3.refine_2.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this✝ : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsPrime}
hJ' : map f J = j
this : J.IsPrime
⊢ {J | map f I ≤ J ∧ J.IsPrime} j

Tactic:
exact ⟨hJ' ▸ map_mono hJ.left, hJ' ▸ map_isPrime_of_surjective hf (le_trans h hJ.left)⟩

Result:
no goals

Proof state:
case h.e'_3.h.e'_3.refine_1.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
hj : map f I ≤ j
hj' : j.IsPrime
⊢ (map f '' {J | I ≤ J ∧ J.IsPrime}) j

Tactic:
haveI : j.IsPrime := hj'

Result:
case h.e'_3.h.e'_3.refine_1.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this✝ : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
hj : map f I ≤ j
hj' this : j.IsPrime
⊢ (map f '' {J | I ≤ J ∧ J.IsPrime}) j

Proof state:
case h.e'_3.h.e'_3.refine_2.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsPrime}
hJ' : map f J = j
⊢ {J | map f I ≤ J ∧ J.IsPrime} j

Tactic:
haveI : J.IsPrime := hJ.right

Result:
case h.e'_3.h.e'_3.refine_2.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this✝ : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsPrime}
hJ' : map f J = j
this : J.IsPrime
⊢ {J | map f I ≤ J ∧ J.IsPrime} j

Proof state:
case h.e'_3.h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
⊢ {J | map f I ≤ J ∧ J.IsPrime} = map f '' {J | I ≤ J ∧ J.IsPrime}

Tactic:
refine funext fun j => propext ⟨?_, ?_⟩

Result:
case h.e'_3.h.e'_3.refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
⊢ {J | map f I ≤ J ∧ J.IsPrime} j → (map f '' {J | I ≤ J ∧ J.IsPrime}) j

case h.e'_3.h.e'_3.refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
⊢ (map f '' {J | I ≤ J ∧ J.IsPrime}) j → {J | map f I ≤ J ∧ J.IsPrime} j

Proof state:
case h.e'_3.h.e'_3.refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
⊢ {J | map f I ≤ J ∧ J.IsPrime} j → (map f '' {J | I ≤ J ∧ J.IsPrime}) j

Tactic:
rintro ⟨hj, hj'⟩

Result:
case h.e'_3.h.e'_3.refine_1.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
hj : map f I ≤ j
hj' : j.IsPrime
⊢ (map f '' {J | I ≤ J ∧ J.IsPrime}) j