∀ {C : Type u_6} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{u_5, u_6} C]
  [inst_1 : CategoryTheory.Category.{u_1, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C)
  (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
  (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D) (j : J)
  (s :
    CategoryTheory.Limits.Cofan
      ((((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj
            ((CategoryTheory.GradedObject.single₀ I).obj Y)).mapObjFun
        p j))
  (m : (CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan F Y e p hp X j).pt ⟶ s.pt),
  (∀ (j_1 : ↑(p ⁻¹' {j})),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.Cofan.inj (CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan F Y e p hp X j)
            j_1)
          m =
        s.inj j_1) →
    m =
      (fun s =>
          CategoryTheory.CategoryStruct.comp (e.inv.app (X j))
            (CategoryTheory.CategoryStruct.comp
              ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).inv) (s.inj ⟨(j, 0), ⋯⟩)))
        s