∀ {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : CommSemiring A] [inst_1 : CommSemiring B]
  [inst_2 : CommSemiring C] {I : Ideal A} {J : Ideal B} {K : Ideal C} {hI : DividedPowers I} {hJ : DividedPowers J}
  {hK : DividedPowers K} (g : hJ.DPMorphism hK) (f : hI.DPMorphism hJ), (g.comp f).toRingHom = g.comp f.toRingHom