no goals
R : Type u
S : Type v
F : Type u_1
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
G : Type ?u.792741
rcg : RingHomClass G S R
ι : Sort ?u.792775
H : IsPrime K
x y : R
h : x * y ∈ comap f K
⊢ ↑f x * ↑f y ∈ K
rwa [mem_comap, map_mul] at h