∀ {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} {x y : hI.DPMorphism hJ},
  (↑↑x.toRingHom).toFun = (↑↑y.toRingHom).toFun → x = y