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.791790
rcg : RingHomClass G S R
ι : Sort ?u.791824
s : Set (Ideal S)
⊢ (⨅ (I : Ideal S) (_ : I ∈ s), comap f I) = ⨅ (I : Ideal R) (_ : I ∈ comap f '' s), I
rw [iInf_image]