no goals
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
x : R
⊢ ↑(Quotient.mk I) x ∈ map (Quotient.mk I) J ↔ x ∈ J ⊔ I
rw [← mem_comap, comap_map_of_surjective (Quotient.mk I) Quotient.mk_surjective, ←
  RingHom.ker_eq_comap_bot, mk_ker]