-- Module: Mathlib.CategoryTheory.GradedObject.Unitor
Goal:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Zero I
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
F : D ⥤ Functor.{v_1, v_2, u_1, u_2} C D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst_5 : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
j : J
s : Cofan ((((mapBifunctor F J I).obj X).obj (Functor.obj (single₀ I) Y)).mapObjFun p j)
j' : J
h_1 : (j', 0) ∈ p ⁻¹' {j}
h : j' = j
pos :
  ∀ (s : Cofan ((((mapBifunctor F J I).obj X).obj (Functor.obj (single₀ I) Y)).mapObjFun p j'))
    (h : (j', 0) ∈ p ⁻¹' {j'}),
    Eq (α :=
      (((mapBifunctor F J I).obj X).obj (Functor.obj (single₀ I) Y)).mapObjFun p j'
          (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j'}) (j', 0) h) ⟶
        s.pt)
      (CategoryStruct.comp (Y :=
        Cocone.pt (F :=
          Discrete.functor ((((mapBifunctor F J I).obj X).obj (Functor.obj (single₀ I) Y)).mapObjFun p j'))
          (mapBifunctorRightUnitorCofan F Y e p hp X j'))
        (Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j')
          (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j'}) (j', 0) h))
        ((fun (s : Cofan ((((mapBifunctor F J I).obj X).obj (Functor.obj (single₀ I) Y)).mapObjFun p j')) ↦
            (e.inv.app (X j') ≫
                CategoryStruct.comp (Y := (F.obj (X j')).obj (Functor.obj (single 0) Y 0))
                  ((F.obj (X j')).map (Iso.inv (singleObjApplyIso 0 Y)))
                  (s.inj (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j'}) (j', 0) ⋯)) :
              Cocone.pt (F :=
                  Discrete.functor ((((mapBifunctor F J I).obj X).obj (Functor.obj (single₀ I) Y)).mapObjFun p j'))
                  (mapBifunctorRightUnitorCofan F Y e p hp X j') ⟶
                s.pt))
          s))
      (s.inj (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j'}) (j', 0) h))
⊢ Eq (α :=
    (((mapBifunctor F J I).obj X).obj (Functor.obj (single₀ I) Y)).mapObjFun p j
        (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j}) (j', 0) h_1) ⟶
      s.pt)
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := Discrete.functor ((((mapBifunctor F J I).obj X).obj (Functor.obj (single₀ I) Y)).mapObjFun p j))
        (mapBifunctorRightUnitorCofan F Y e p hp X j))
      (Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j)
        (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j}) (j', 0) h_1))
      ((fun (s : Cofan ((((mapBifunctor F J I).obj X).obj (Functor.obj (single₀ I) Y)).mapObjFun p j)) ↦
          (e.inv.app (X j) ≫
              CategoryStruct.comp (Y := (F.obj (X j)).obj (Functor.obj (single 0) Y 0))
                ((F.obj (X j)).map (Iso.inv (singleObjApplyIso 0 Y)))
                (s.inj (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j}) (j, 0) ⋯)) :
            Cocone.pt (F :=
                Discrete.functor ((((mapBifunctor F J I).obj X).obj (Functor.obj (single₀ I) Y)).mapObjFun p j))
                (mapBifunctorRightUnitorCofan F Y e p hp X j) ⟶
              s.pt))
        s))
    (s.inj (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j}) (j', 0) h_1))

Tactic:
subst h