R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.388826
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
⊢ ↑(comap f) '' Set.univ = zeroLocus ↑(ker f)
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.388826
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
⊢ Set.range ↑(comap f) = zeroLocus ↑(ker f)
rw [← Set.image_univ]
case h.e'_2.h.e'_4
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.388826
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
⊢ Set.univ = zeroLocus ↑⊥
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.388826
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
⊢ ↑(comap f) '' Set.univ = zeroLocus ↑(ker f)
convert image_comap_zeroLocus_eq_zeroLocus_comap _ _ hf _
no goals
case h.e'_2.h.e'_4
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.388826
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
⊢ Set.univ = zeroLocus ↑⊥
rw [zeroLocus_bot]