-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Unitor (goal)
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 : C ⥤ Functor.{v_2, v_2, u_2, u_2} D D
X : C
e : F.obj X ≅ 𝟭 D
inst_5 : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
j : J
s : Cofan ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j)
i : I
j' : J
h : (i, j') ∈ p ⁻¹' {j}
pos :
  ∀ (hi : i = 0),
    Eq (α :=
      (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j
          (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (i, j') h) ⟶
        s.pt)
      (CategoryStruct.comp (Y :=
        Cocone.pt (F := Discrete.functor ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j))
          (mapBifunctorLeftUnitorCofan F X e p hp Y j))
        (Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j)
          (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (i, j') h))
        ((fun (s : Cofan ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j)) ↦
            (e.inv.app (Y j) ≫
                CategoryStruct.comp (Y := (F.obj (Functor.obj (single 0) X 0)).obj (Y j))
                  (NatTrans.app (F.map (Iso.inv (singleObjApplyIso 0 X))) (Y j))
                  (s.inj (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (0, j) ⋯)) :
              Cocone.pt (F :=
                  Discrete.functor ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j))
                  (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟶
                s.pt))
          s))
      (s.inj (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (i, j') h))
⊢ Eq (α :=
    (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j
        (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (i, j') h) ⟶
      s.pt)
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := Discrete.functor ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j))
        (mapBifunctorLeftUnitorCofan F X e p hp Y j))
      (Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j)
        (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (i, j') h))
      ((fun (s : Cofan ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j)) ↦
          (e.inv.app (Y j) ≫
              CategoryStruct.comp (Y := (F.obj (Functor.obj (single 0) X 0)).obj (Y j))
                (NatTrans.app (F.map (Iso.inv (singleObjApplyIso 0 X))) (Y j))
                (s.inj (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (0, j) ⋯)) :
            Cocone.pt (F :=
                Discrete.functor ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j))
                (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟶
              s.pt))
        s))
    (s.inj (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (i, j') h))
have neg : ∀ (hi : ¬i = 0),
  Eq (α :=
    (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j
        (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (i, j') h) ⟶
      s.pt)
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := Discrete.functor ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j))
        (mapBifunctorLeftUnitorCofan F X e p hp Y j))
      (Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j)
        (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (i, j') h))
      ((fun (s : Cofan ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j)) ↦
          (e.inv.app (Y j) ≫
              CategoryStruct.comp (Y := (F.obj (Functor.obj (single 0) X 0)).obj (Y j))
                (NatTrans.app (F.map (Iso.inv (singleObjApplyIso 0 X))) (Y j))
                (s.inj (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (0, j) sorry)) :
            Cocone.pt (F :=
                Discrete.functor ((((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).mapObjFun p j))
                (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟶
              s.pt))
        s))
    (s.inj (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (i, j') h))
Tactic: by_cases hi : i = 0