no goals
R : Type u
S : Type v
T : Type w
F : Type ?u.1721293
G : Type ?u.1721296
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
rcf : RingHomClass F R S
rcg : RingHomClass G T S
f✝ : F
g✝ : G
f : S →+* R
g : T →+* S
⊢ Ideal.comap g (ker f) = ker (comp f g)
rw [RingHom.ker_eq_comap_bot, Ideal.comap_comap, RingHom.ker_eq_comap_bot]