∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  (hI : DividedPowers I) (hJ : DividedPowers J) (h h' : hI.DPMorphism hJ),
  (fun h => ⇑h.toRingHom) h = (fun h => ⇑h.toRingHom) h' → h = h'