{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} →
                {motive : hI.DPMorphism hJ → Sort u} →
                  (t : hI.DPMorphism hJ) →
                    ((toRingHom : A →+* B) →
                        (ideal_comp : Ideal.map toRingHom I ≤ J) →
                          (dpow_comp : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom a) = toRingHom (hI.dpow n a)) →
                            motive { toRingHom := toRingHom, ideal_comp := ideal_comp, dpow_comp := dpow_comp }) →
                      motive t