R : Type u_1
S : Type u_2
F : Type ?u.1989731
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 ∧ IsPrime J}) = sInf {J | map f I ≤ J ∧ IsPrime J}
R : Type u_1
S : Type u_2
F : Type ?u.1989731
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal R
h : RingHom.ker f ≤ I
⊢ map f (radical I) = radical (map f I)
rw [radical_eq_sInf, radical_eq_sInf]
R : Type u_1
S : Type u_2
F : Type ?u.1989731
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsPrime J} → RingHom.ker f ≤ J
⊢ map f (sInf {J | I ≤ J ∧ IsPrime J}) = sInf {J | map f I ≤ J ∧ IsPrime J}
R : Type u_1
S : Type u_2
F : Type ?u.1989731
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 ∧ IsPrime J}) = sInf {J | map f I ≤ J ∧ IsPrime J}
have : ∀ J ∈ {J : Ideal R | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J := fun J hJ => h.trans hJ.left
case h.e'_3.h.e'_3
R : Type u_1
S : Type u_2
F : Type ?u.1989731
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsPrime J} → RingHom.ker f ≤ J
⊢ {J | map f I ≤ J ∧ IsPrime J} = map f '' {J | I ≤ J ∧ IsPrime J}
R : Type u_1
S : Type u_2
F : Type ?u.1989731
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsPrime J} → RingHom.ker f ≤ J
⊢ map f (sInf {J | I ≤ J ∧ IsPrime J}) = sInf {J | map f I ≤ J ∧ IsPrime J}
convert map_sInf hf this
case h.e'_3.h.e'_3.refine'_1
R : Type u_1
S : Type u_2
F : Type ?u.1989731
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsPrime J} → RingHom.ker f ≤ J
j : Ideal S
⊢ setOf (fun J => map f I ≤ J ∧ IsPrime J) j → (map f '' {J | I ≤ J ∧ IsPrime J}) j

case h.e'_3.h.e'_3.refine'_2
R : Type u_1
S : Type u_2
F : Type ?u.1989731
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsPrime J} → RingHom.ker f ≤ J
j : Ideal S
⊢ (map f '' {J | I ≤ J ∧ IsPrime J}) j → setOf (fun J => map f I ≤ J ∧ IsPrime J) j
case h.e'_3.h.e'_3
R : Type u_1
S : Type u_2
F : Type ?u.1989731
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsPrime J} → RingHom.ker f ≤ J
⊢ {J | map f I ≤ J ∧ IsPrime J} = map f '' {J | I ≤ J ∧ IsPrime J}
refine' funext fun j => propext ⟨_, _⟩
case h.e'_3.h.e'_3.refine'_1.intro
R : Type u_1
S : Type u_2
F : Type ?u.1989731
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsPrime J} → RingHom.ker f ≤ J
j : Ideal S
hj : map f I ≤ j
hj' : IsPrime j
⊢ (map f '' {J | I ≤ J ∧ IsPrime J}) j
case h.e'_3.h.e'_3.refine'_1
R : Type u_1
S : Type u_2
F : Type ?u.1989731
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsPrime J} → RingHom.ker f ≤ J
j : Ideal S
⊢ setOf (fun J => map f I ≤ J ∧ IsPrime J) j → (map f '' {J | I ≤ J ∧ IsPrime J}) j
rintro ⟨hj, hj'⟩
case h.e'_3.h.e'_3.refine'_1.intro
R : Type u_1
S : Type u_2
F : Type ?u.1989731
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal R
h : RingHom.ker f ≤ I
this✝ : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsPrime J} → RingHom.ker f ≤ J
j : Ideal S
hj : map f I ≤ j
hj' this : IsPrime j
⊢ (map f '' {J | I ≤ J ∧ IsPrime J}) j
case h.e'_3.h.e'_3.refine'_1.intro
R : Type u_1
S : Type u_2
F : Type ?u.1989731
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsPrime J} → RingHom.ker f ≤ J
j : Ideal S
hj : map f I ≤ j
hj' : IsPrime j
⊢ (map f '' {J | I ≤ J ∧ IsPrime J}) j
haveI : j.IsPrime := hj'
no goals
case h.e'_3.h.e'_3.refine'_1.intro
R : Type u_1
S : Type u_2
F : Type ?u.1989731
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal R
h : RingHom.ker f ≤ I
this✝ : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsPrime J} → RingHom.ker f ≤ J
j : Ideal S
hj : map f I ≤ j
hj' this : IsPrime j
⊢ (map f '' {J | I ≤ J ∧ IsPrime J}) j
exact
  ⟨comap f j, ⟨⟨map_le_iff_le_comap.1 hj, comap_isPrime f j⟩, map_comap_of_surjective f hf j⟩⟩
case h.e'_3.h.e'_3.refine'_2.intro.intro
R : Type u_1
S : Type u_2
F : Type ?u.1989731
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsPrime J} → RingHom.ker f ≤ J
j : Ideal S
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ IsPrime J}
hJ' : map f J = j
⊢ setOf (fun J => map f I ≤ J ∧ IsPrime J) j
case h.e'_3.h.e'_3.refine'_2
R : Type u_1
S : Type u_2
F : Type ?u.1989731
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsPrime J} → RingHom.ker f ≤ J
j : Ideal S
⊢ (map f '' {J | I ≤ J ∧ IsPrime J}) j → setOf (fun J => map f I ≤ J ∧ IsPrime J) j
rintro ⟨J, ⟨hJ, hJ'⟩⟩
case h.e'_3.h.e'_3.refine'_2.intro.intro
R : Type u_1
S : Type u_2
F : Type ?u.1989731
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal R
h : RingHom.ker f ≤ I
this✝ : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsPrime J} → RingHom.ker f ≤ J
j : Ideal S
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ IsPrime J}
hJ' : map f J = j
this : IsPrime J
⊢ setOf (fun J => map f I ≤ J ∧ IsPrime J) j
case h.e'_3.h.e'_3.refine'_2.intro.intro
R : Type u_1
S : Type u_2
F : Type ?u.1989731
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsPrime J} → RingHom.ker f ≤ J
j : Ideal S
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ IsPrime J}
hJ' : map f J = j
⊢ setOf (fun J => map f I ≤ J ∧ IsPrime J) j
haveI : J.IsPrime := hJ.right
no goals
case h.e'_3.h.e'_3.refine'_2.intro.intro
R : Type u_1
S : Type u_2
F : Type ?u.1989731
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal R
h : RingHom.ker f ≤ I
this✝ : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsPrime J} → RingHom.ker f ≤ J
j : Ideal S
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ IsPrime J}
hJ' : map f J = j
this : IsPrime J
⊢ setOf (fun J => map f I ≤ J ∧ IsPrime J) j
refine' ⟨hJ' ▸ map_mono hJ.left, hJ' ▸ map_isPrime_of_surjective hf (le_trans h hJ.left)⟩