-- 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')
h : (j', 0) ∈ p ⁻¹' {j'}
pos :
  Eq (α := (F.obj (X j')).obj (Functor.obj (single₀ I) Y 0) ⟶ s.pt)
    (((F.obj (X j')).map (Iso.hom (singleObjApplyIso 0 Y)) ≫ e.hom.app (X 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) ⋯)))
    (s.inj (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j'}) (j', 0) h))
pos₁ :
  Eq (α := (F.obj (X j')).obj (Functor.obj (single₀ I) Y 0) ⟶ s.pt)
    ((F.obj (X j')).map (Iso.hom (singleObjApplyIso 0 Y)) ≫
      e.hom.app (X 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) ⋯)))
    (s.inj (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j'}) (j', 0) h))
pos₂ :
  Eq (α := (F.obj (X j')).obj (Functor.obj (single₀ I) Y 0) ⟶ s.pt)
    ((F.obj (X j')).map (Iso.hom (singleObjApplyIso 0 Y)) ≫
      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) ⋯)))
    (s.inj (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j'}) (j', 0) h))
pos₃ :
  Eq (α := (F.obj (X j')).obj (Functor.obj (single₀ I) Y 0) ⟶ s.pt)
    (CategoryStruct.comp (Y := (F.obj (X j')).obj (Functor.obj (single 0) Y 0))
      ((F.obj (X j')).map (Iso.hom (singleObjApplyIso 0 Y) ≫ Iso.inv (singleObjApplyIso 0 Y)))
      (s.inj (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j'}) (j', 0) ⋯)))
    (s.inj (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j'}) (j', 0) h))
pos₄ :
  Eq (α := (F.obj (X j')).obj (Functor.obj (single₀ I) Y 0) ⟶ s.pt)
    (CategoryStruct.comp (Y := (F.obj (X j')).obj (Functor.obj (single 0) Y 0))
      ((F.obj (X j')).map (𝟙 (Functor.obj (single 0) Y 0)))
      (s.inj (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j'}) (j', 0) ⋯)))
    (s.inj (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j'}) (j', 0) h))
pos₅ :
  Eq.{v_2 + 1} (α := (F.obj (X j')).obj (Functor.obj (single₀ I) Y 0) ⟶ s.pt)
    (𝟙 ((F.obj (X j')).obj (Functor.obj (single 0) Y 0)) ≫
      s.inj (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j'}) (j', 0) ⋯))
    (s.inj (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j'}) (j', 0) h))
pos₆ pos₇ :
  Eq (α := (F.obj (X j')).obj (Functor.obj (single₀ I) Y 0) ⟶ s.pt)
    (s.inj (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j'}) (j', 0) ⋯) :
      (((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) ⋯) ⟶
        s.pt)
    (s.inj (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j'}) (j', 0) h))
⊢ Eq (α := (F.obj (X j')).obj (Functor.obj (single₀ I) Y 0) ⟶ s.pt)
    (Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j')
          (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j'}) (j', 0) h) ≫
        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) ⋯)) :
      (F.obj (X j')).obj (Functor.obj (single₀ I) Y 0) ⟶ s.pt)
    (s.inj (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j'}) (j', 0) h) :
      (((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)

Tactic:
rw [mapBifunctorRightUnitorCofan_inj, assoc, Iso.hom_inv_id_app_assoc,
          ← Functor.map_comp_assoc, Iso.hom_inv_id, Functor.map_id, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan_inj, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp