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 : 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 : (j', 0) ∈ p ⁻¹' {j}
⊢ j' = j

Tactic:
simp only [Set.mem_preimage, hp, Set.mem_singleton_iff] at h

Premises used: Set.mem_singleton_iff, Set.mem_preimage
-- 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)
    (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)
⊢ 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))

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 : 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
neg :
  IsInitial.{v_2, u_2}
    ((((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))
⊢ 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:
apply IsInitial.hom_ext

Premises used: CategoryTheory.Limits.IsInitial.hom_ext
-- 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
⊢ IsInitial.{v_2, u_2}
    ((((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))

Tactic:
exact mapBifunctorObjObjSingle₀IsInitial _ _ _ _ hi

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

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 : 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)
m :
  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
hm :
  ∀ (j_1 : (↑(p ⁻¹' {j}) : Type (max u_3 u_4))),
    Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) j_1 ≫ m = s.inj j_1
rw :
  m =
    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)))
        (Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j)
            (Subtype.mk (p := fun (x : J × I) ↦ x ∈ p ⁻¹' {j}) (j, 0) ⋯) ≫
          m)
rw₁ :
  m =
    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)))
        (((F.obj (X j)).map (Iso.hom (singleObjApplyIso 0 Y)) ≫ e.hom.app (X j)) ≫ m)
rw₂ :
  m =
    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)))
        ((F.obj (X j)).map (Iso.hom (singleObjApplyIso 0 Y)) ≫ e.hom.app (X j) ≫ m)
rw₃ :
  m =
    e.inv.app (X j) ≫
      (F.obj (X j)).map
          (CategoryStruct.comp (Y := Functor.obj (single 0) Y 0) (Iso.inv (singleObjApplyIso 0 Y))
            (Iso.hom (singleObjApplyIso 0 Y))) ≫
        e.hom.app (X j) ≫ m
rw₄ : m = e.inv.app (X j) ≫ (F.obj (X j)).map (𝟙 Y) ≫ e.hom.app (X j) ≫ m
rw₅ : m = e.inv.app (X j) ≫ 𝟙 ((F.obj (X j)).obj Y) ≫ e.hom.app (X j) ≫ m
rw₆ : m = e.inv.app (X j) ≫ e.hom.app (X j) ≫ m
rw₇ rw₈ : m = m
⊢ m =
    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) ⋯))

Tactic:
rw [← hm ⟨⟨j, 0⟩, hp j⟩, mapBifunctorRightUnitorCofan_inj, assoc, ← Functor.map_comp_assoc,
        Iso.inv_hom_id, Functor.map_id, id_comp, Iso.inv_hom_id_app_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan_inj, Prod.mk, Subtype.mk, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, OfNat.ofNat, CategoryTheory.Iso.inv_hom_id_app_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 : 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
⊢ (((mapBifunctor F J I).obj X).obj (Functor.obj (single₀ I) Y)).HasMap p

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

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

Tactic:
dsimp [mapBifunctorRightUnitor]

Premises used: CategoryTheory.GradedObject.mapBifunctorRightUnitor
-- 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
inst_6 : (((mapBifunctor F J I).obj X).obj (Functor.obj (single₀ I) Y)).HasMap p
j : J
erw :
  Eq (α := (F.obj (X j)).obj (Functor.obj (single₀ I) Y 0) ⟶ X j)
    (Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j)
        (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) ⋯) ⟶
        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))
    ((F.obj (X j)).map (Iso.hom (singleObjApplyIso 0 Y)) ≫ e.hom.app (X j))
⊢ Eq (α := (F.obj (X j)).obj (Functor.obj (single₀ I) Y 0) ⟶ X j)
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) j)
        (ιMapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) j 0 j ⋯)
        (Iso.inv (CofanMapObjFun.iso (mapBifunctorRightUnitorCofanIsColimit F Y e p hp X j))) :
      (F.obj (X j)).obj (Functor.obj (single₀ I) Y 0) ⟶ X j)
    ((F.obj (X j)).map (Iso.hom (singleObjApplyIso 0 Y)) ≫ e.hom.app (X j) :
      (F.obj (X j)).obj (Functor.obj (single 0) Y 0) ⟶ X 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 : 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
inst_6 : (((mapBifunctor F J I).obj X).obj (Functor.obj (single₀ I) Y)).HasMap p
j : J
rw rw₁ :
  Eq (α := (F.obj (X j)).obj (Functor.obj (single₀ I) Y 0) ⟶ X j)
    ((F.obj (X j)).map (Iso.hom (singleObjApplyIso 0 Y)) ≫ e.hom.app (X j))
    ((F.obj (X j)).map (Iso.hom (singleObjApplyIso 0 Y)) ≫ e.hom.app (X j))
⊢ Eq (α := (F.obj (X j)).obj (Functor.obj (single₀ I) Y 0) ⟶ X j)
    (Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j)
        (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) ⋯) ⟶
        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))
    ((F.obj (X j)).map (Iso.hom (singleObjApplyIso 0 Y)) ≫ e.hom.app (X j))

Tactic:
rw [mapBifunctorRightUnitorCofan_inj]

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

Tactic:
rfl

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

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

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

Premises used: CategoryTheory.GradedObject.ι_mapBifunctorMapMap, CategoryTheory.Category.assoc, CategoryTheory.GradedObject.mapBifunctorRightUnitor_inv_apply