no goals
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
hIJ : I ≤ J
x : R
⊢ ↑(Quotient.mk I) x ∈ map (Quotient.mk I) J ↔ x ∈ J
rw [mem_quotient_iff_mem_sup, sup_eq_left.mpr hIJ]