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.781465
rcg : RingHomClass G S R
I : Ideal S
h : I = ⊤
⊢ comap f I = ⊤
rw [h, comap_top]