awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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}
hi : ¬i = 0
⊢ IsInitial.{v_2, u_2}
    ((((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))

Tactic:
exact mapBifunctorObjSingle₀ObjIsInitial _ _ _ _ hi

Premises used: CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIsInitial
-- 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 : 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)
m :
  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
hm :
  ∀ (j_1 : (↑(p ⁻¹' {j}) : Type (max u_3 u_4))),
    Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j) j_1 ≫ m = s.inj j_1
⊢ m =
    (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

Tactic:
simp [← hm ⟨⟨0, j⟩, hp j⟩]

Premises used: Prod.mk, Subtype.mk, OfNat.ofNat
-- 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 : 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 : GradedObject J D
⊢ (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).HasMap p

Tactic:
CofanMapObjFun.hasMap _ _ _ (mapBifunctorLeftUnitorCofanIsColimit F X e p hp Y)

Premises used: CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofanIsColimit, CategoryTheory.GradedObject.CofanMapObjFun.hasMap
-- 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 : 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 : GradedObject J D
inst_6 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).HasMap p
j : J
dsimp :
  Eq (α := (F.obj (Functor.obj (single₀ I) X 0)).obj (Y j) ⟶ Y j)
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y j)
        (ιMapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y 0 j j ⋯)
        (Iso.inv (CofanMapObjFun.iso (mapBifunctorLeftUnitorCofanIsColimit F X e p hp Y j))) :
      (F.obj (Functor.obj (single₀ I) X 0)).obj (Y j) ⟶ Y j)
    (NatTrans.app (F.map (Iso.hom (singleObjApplyIso 0 X))) (Y j) ≫ e.hom.app (Y j) :
      (F.obj (Functor.obj (single 0) X 0)).obj (Y j) ⟶ Y j)
⊢ Eq (α := (F.obj (Functor.obj (single₀ I) X 0)).obj (Y j) ⟶ Y j)
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y j)
      (ιMapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y 0 j j ⋯) (Iso.hom (mapBifunctorLeftUnitor F X e p hp Y) j))
    (NatTrans.app (F.map (Iso.hom (singleObjApplyIso 0 X))) (Y j) ≫ e.hom.app (Y j))

Tactic:
dsimp [mapBifunctorLeftUnitor]

Premises used: CategoryTheory.GradedObject.mapBifunctorLeftUnitor
-- 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 : 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 : GradedObject J D
inst_6 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).HasMap p
j : J
erw :
  Eq (α := (F.obj (Functor.obj (single₀ I) X 0)).obj (Y j) ⟶ Y j)
    (Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j)
        (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (0, j) ⋯) :
      (((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}) (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))
    (NatTrans.app (F.map (Iso.hom (singleObjApplyIso 0 X))) (Y j) ≫ e.hom.app (Y j))
⊢ Eq (α := (F.obj (Functor.obj (single₀ I) X 0)).obj (Y j) ⟶ Y j)
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y j)
        (ιMapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y 0 j j ⋯)
        (Iso.inv (CofanMapObjFun.iso (mapBifunctorLeftUnitorCofanIsColimit F X e p hp Y j))) :
      (F.obj (Functor.obj (single₀ I) X 0)).obj (Y j) ⟶ Y j)
    (NatTrans.app (F.map (Iso.hom (singleObjApplyIso 0 X))) (Y j) ≫ e.hom.app (Y j) :
      (F.obj (Functor.obj (single 0) X 0)).obj (Y j) ⟶ Y j)

Tactic:
erw [CofanMapObjFun.ιMapObj_iso_inv]

Premises used: CategoryTheory.GradedObject.CofanMapObjFun.ιMapObj_iso_inv
-- 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 : 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 : GradedObject J D
inst_6 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).HasMap p
j : J
rw rw₁ :
  Eq (α := (F.obj (Functor.obj (single₀ I) X 0)).obj (Y j) ⟶ Y j)
    (NatTrans.app (F.map (Iso.hom (singleObjApplyIso 0 X))) (Y j) ≫ e.hom.app (Y j))
    (NatTrans.app (F.map (Iso.hom (singleObjApplyIso 0 X))) (Y j) ≫ e.hom.app (Y j))
⊢ Eq (α := (F.obj (Functor.obj (single₀ I) X 0)).obj (Y j) ⟶ Y j)
    (Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j)
        (Subtype.mk (p := fun (x : I × J) ↦ x ∈ p ⁻¹' {j}) (0, j) ⋯) :
      (((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}) (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))
    (NatTrans.app (F.map (Iso.hom (singleObjApplyIso 0 X))) (Y j) ≫ e.hom.app (Y j))

Tactic:
rw [mapBifunctorLeftUnitorCofan_inj]

Premises used: CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan_inj
-- 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 : 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 : GradedObject J D
inst_6 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).HasMap p
j : J
⊢ Eq.{v_2 + 1} (α := Y j ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y j)
    (Iso.inv (mapBifunctorLeftUnitor F X e p hp Y) j : Y j ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y j)
    (e.inv.app (Y j) ≫
        NatTrans.app (F.map (Iso.inv (singleObjApplyIso 0 X))) (Y j) ≫
          ιMapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y 0 j j ⋯ :
      Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) (Y j) ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y j)

Tactic:
rfl

Premises used: CategoryTheory.GradedObject.ιMapBifunctorMapObj, CategoryTheory.GradedObject.mapBifunctorMapObj, CategoryTheory.GradedObject.ιMapObj, CategoryTheory.Limits.colimit, CategoryTheory.GradedObject.mapObj, rfl, CategoryTheory.Limits.colimit.ι
-- 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 : 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'
inst_6 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).HasMap p
inst_7 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y').HasMap p
h :
  ∀ (j : J),
    Eq.{v_2 + 1} (α := Y j ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' j)
      ((φ ≫ Iso.inv (mapBifunctorLeftUnitor F X e p hp Y')) j :
        Y j ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' j)
      (CategoryStruct.comp (Y := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y)
          (Iso.inv (mapBifunctorLeftUnitor F X e p hp Y)) (mapBifunctorMapMap F p (𝟙 (Functor.obj (single₀ I) X)) φ) j :
        Y j ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' j)
⊢ Eq (α := Y ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y')
    (φ ≫ Iso.inv (mapBifunctorLeftUnitor F X e p hp Y'))
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y)
      (Iso.inv (mapBifunctorLeftUnitor F X e p hp Y)) (mapBifunctorMapMap F p (𝟙 (Functor.obj (single₀ I) X)) φ))

Tactic:
ext j
-- 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 : 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'
inst_6 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).HasMap p
inst_7 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y').HasMap p
j : J
h :
  Eq.{v_2 + 1} (α := Y j ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' j)
    (φ j ≫ Iso.inv (mapBifunctorLeftUnitor F X e p hp Y') j)
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y j)
      (Iso.inv (mapBifunctorLeftUnitor F X e p hp Y) j) (mapBifunctorMapMap F p (𝟙 (Functor.obj (single₀ I) X)) φ j))
⊢ Eq.{v_2 + 1} (α := Y j ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' j)
    ((φ ≫ Iso.inv (mapBifunctorLeftUnitor F X e p hp Y')) j :
      Y j ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' j)
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y)
        (Iso.inv (mapBifunctorLeftUnitor F X e p hp Y)) (mapBifunctorMapMap F p (𝟙 (Functor.obj (single₀ I) X)) φ) j :
      Y j ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' j)

Tactic:
dsimp
-- 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 : 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'
inst_6 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).HasMap p
inst_7 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y').HasMap p
j : J
h :
  Eq (α := Y j ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' j)
    (φ j ≫
      e.inv.app (Y' j) ≫
        NatTrans.app (F.map (Iso.inv (singleObjApplyIso 0 X))) (Y' j) ≫
          ιMapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' 0 j 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))
        (NatTrans.app (F.map (𝟙 (Functor.obj (single₀ I) X) 0)) (Y j) ≫
          (F.obj (Functor.obj (single₀ I) X 0)).map (φ j) ≫
            ιMapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' 0 j j ⋯))
⊢ Eq.{v_2 + 1} (α := Y j ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' j)
    (φ j ≫ Iso.inv (mapBifunctorLeftUnitor F X e p hp Y') j)
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y j)
      (Iso.inv (mapBifunctorLeftUnitor F X e p hp Y) j) (mapBifunctorMapMap F p (𝟙 (Functor.obj (single₀ I) X)) φ j))

Tactic:
rw [mapBifunctorLeftUnitor_inv_apply, mapBifunctorLeftUnitor_inv_apply, assoc, assoc,
    ι_mapBifunctorMapMap]

Premises used: CategoryTheory.GradedObject.ι_mapBifunctorMapMap, CategoryTheory.Category.assoc, CategoryTheory.GradedObject.mapBifunctorLeftUnitor_inv_apply
-- 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 : 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'
inst_6 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).HasMap p
inst_7 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y').HasMap p
j : J
h :
  Eq (α := Y j ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' j)
    (φ j ≫
      e.inv.app (Y' j) ≫
        NatTrans.app (F.map (Iso.inv (singleObjApplyIso 0 X))) (Y' j) ≫
          ιMapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' 0 j 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))
        (NatTrans.app (F.map (𝟙 (Functor.obj (single₀ I) X 0))) (Y j) ≫
          (F.obj (Functor.obj (single₀ I) X 0)).map (φ j) ≫
            ιMapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' 0 j j ⋯))
⊢ Eq (α := Y j ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' j)
    (φ j ≫
      e.inv.app (Y' j) ≫
        NatTrans.app (F.map (Iso.inv (singleObjApplyIso 0 X))) (Y' j) ≫
          ιMapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' 0 j 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))
        (NatTrans.app (F.map (𝟙 (Functor.obj (single₀ I) X) 0)) (Y j) ≫
          (F.obj (Functor.obj (single₀ I) X 0)).map (φ j) ≫
            ιMapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' 0 j j ⋯))

Tactic:
dsimp
-- 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 : 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'
inst_6 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).HasMap p
inst_7 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y').HasMap p
j : J
h :
  Eq (α := Y j ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' j)
    (φ j ≫
      e.inv.app (Y' j) ≫
        NatTrans.app (F.map (Iso.inv (singleObjApplyIso 0 X))) (Y' j) ≫
          ιMapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' 0 j j ⋯)
    (Functor.map (𝟭 D) (φ j) ≫
      e.inv.app (Y' j) ≫
        NatTrans.app (F.map (Iso.inv (singleObjApplyIso 0 X))) (Y' j) ≫
          ιMapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' 0 j j ⋯)
⊢ Eq (α := Y j ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' j)
    (φ j ≫
      e.inv.app (Y' j) ≫
        NatTrans.app (F.map (Iso.inv (singleObjApplyIso 0 X))) (Y' j) ≫
          ιMapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' 0 j 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))
        (NatTrans.app (F.map (𝟙 (Functor.obj (single₀ I) X 0))) (Y j) ≫
          (F.obj (Functor.obj (single₀ I) X 0)).map (φ j) ≫
            ιMapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' 0 j j ⋯))

Tactic:
rw [Functor.map_id, NatTrans.id_app, id_comp, ← NatTrans.naturality_assoc,
    ← NatTrans.naturality_assoc]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.id_app, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.Category.id_comp
-- 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 : 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'
inst_6 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).HasMap p
inst_7 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y').HasMap p
j : J
⊢ Eq (α := Y j ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' j)
    (φ j ≫
      e.inv.app (Y' j) ≫
        NatTrans.app (F.map (Iso.inv (singleObjApplyIso 0 X))) (Y' j) ≫
          ιMapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' 0 j j ⋯)
    (Functor.map (𝟭 D) (φ j) ≫
      e.inv.app (Y' j) ≫
        NatTrans.app (F.map (Iso.inv (singleObjApplyIso 0 X))) (Y' j) ≫
          ιMapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y' 0 j j ⋯)

Tactic:
rfl
-- 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_1 : ∀ (j : J), p (j, 0) = j
X_1 X' : GradedObject J D
φ : X_1 ⟶ X'
hp : ∀ (j : J), p (j, 0) = j
X : GradedObject J D
j : J
a : J × I
ha_1 : p a = j
ha : a.2 = 0
⊢ X a.1 = X j

Tactic:
aesop
-- 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 : GradedObject J D
j : 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) ⋯) ⟶
      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) ⋯))
    ((F.obj (X j)).map (Iso.hom (singleObjApplyIso 0 Y)) ≫ e.hom.app (X j))

Tactic:
simp [mapBifunctorRightUnitorCofan]

Premises used: CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan
-- 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
i : I
h : (j', i) ∈ p ⁻¹' {j}
hi : i = 0
pos :
  ∀ (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', i) 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', i) 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', i) h))

Tactic:
subst hi