∀ {A : Type u_3} {B : Type u_4} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  (hI : DividedPowers I) (hJ : DividedPowers J) {f : hI.DPMorphism hJ} {a : A}, f.toRingHom a = f a