awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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 (α := (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))
have 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 sorry)
      (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: dsimp [mapBifunctorRightUnitor]
-- 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 : 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 (α := (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)
have 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) sorry) :
    (((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) sorry) ⟶
      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: erw [CofanMapObjFun.ιMapObj_iso_inv]
-- 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 : 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 (α := (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))
have 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))
Tactic: rw [mapBifunctorRightUnitorCofan_inj]
-- 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 : 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
⊢ 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))))
have 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)
Tactic: ext j
-- 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 : 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
⊢ 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)
have 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))
Tactic: dsimp
-- 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 : 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
⊢ 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))
have 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 sorry)
  (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 sorry))
Tactic: rw [mapBifunctorRightUnitor_inv_apply, mapBifunctorRightUnitor_inv_apply, assoc, assoc,
    ι_mapBifunctorMapMap]
-- 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 : 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
⊢ 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 ⋯))
have 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 sorry)
  (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 sorry))
Tactic: dsimp
-- 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 : 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
⊢ 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 ⋯))
have 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 sorry)
  (e.inv.app (X j) ≫
    (F.map (φ j)).app Y ≫
      (F.obj (X' j)).map (Iso.inv (singleObjApplyIso 0 Y)) ≫
        ιMapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j 0 j sorry)
Tactic: rw [Functor.map_id, id_comp, NatTrans.naturality_assoc]
-- 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 : 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
⊢ 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) ≫
      (F.map (φ j)).app Y ≫
        (F.obj (X' j)).map (Iso.inv (singleObjApplyIso 0 Y)) ≫
          ιMapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j 0 j ⋯)
have 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 sorry)
  (Functor.map (𝟭 D) (φ 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 sorry)
Tactic: erw [← NatTrans.naturality_assoc e.inv]
-- 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 : 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
⊢ Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ X')
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
      (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y))) (Iso.hom (mapBifunctorRightUnitor F Y e p hp X')))
    (Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ)
have rw : Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
  (CategoryStruct.comp (Y := mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
      (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y))) (Iso.hom (mapBifunctorRightUnitor F Y e p hp X')) ≫
    Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
  ((Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ) ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
Tactic: rw [← cancel_mono (mapBifunctorRightUnitor F Y e p hp X').inv, assoc, assoc, Iso.hom_inv_id,
    comp_id, mapBifunctorRightUnitor_inv_naturality, Iso.hom_inv_id_assoc]
-- 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 : 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
rw :
  Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
        (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y))) (Iso.hom (mapBifunctorRightUnitor F Y e p hp X')) ≫
      Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
    ((Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ) ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
⊢ Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ X')
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
      (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y))) (Iso.hom (mapBifunctorRightUnitor F Y e p hp X')))
    (Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ)
have rw₁ : Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
  (CategoryStruct.comp (Y := mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
    (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y)))
    (Iso.hom (mapBifunctorRightUnitor F Y e p hp X') ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X')))
  ((Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ) ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
Tactic: rw [← cancel_mono (mapBifunctorRightUnitor F Y e p hp X').inv, assoc, assoc, Iso.hom_inv_id,
    comp_id, mapBifunctorRightUnitor_inv_naturality, Iso.hom_inv_id_assoc]
-- 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 : 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
rw :
  Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
        (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y))) (Iso.hom (mapBifunctorRightUnitor F Y e p hp X')) ≫
      Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
    ((Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ) ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
rw₁ :
  Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
      (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y)))
      (Iso.hom (mapBifunctorRightUnitor F Y e p hp X') ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X')))
    ((Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ) ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
⊢ Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ X')
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
      (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y))) (Iso.hom (mapBifunctorRightUnitor F Y e p hp X')))
    (Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ)
have rw₂ : Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
  (CategoryStruct.comp (Y := mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
    (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y)))
    (Iso.hom (mapBifunctorRightUnitor F Y e p hp X') ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X')))
  (Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
Tactic: rw [← cancel_mono (mapBifunctorRightUnitor F Y e p hp X').inv, assoc, assoc, Iso.hom_inv_id,
    comp_id, mapBifunctorRightUnitor_inv_naturality, Iso.hom_inv_id_assoc]
-- 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 : 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
rw :
  Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
        (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y))) (Iso.hom (mapBifunctorRightUnitor F Y e p hp X')) ≫
      Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
    ((Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ) ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
rw₁ :
  Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
      (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y)))
      (Iso.hom (mapBifunctorRightUnitor F Y e p hp X') ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X')))
    ((Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ) ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
rw₂ :
  Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
      (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y)))
      (Iso.hom (mapBifunctorRightUnitor F Y e p hp X') ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X')))
    (Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
⊢ Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ X')
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
      (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y))) (Iso.hom (mapBifunctorRightUnitor F Y e p hp X')))
    (Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ)
have rw₃ : Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
  (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y)) ≫ 𝟙 (mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y)))
  (Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
Tactic: rw [← cancel_mono (mapBifunctorRightUnitor F Y e p hp X').inv, assoc, assoc, Iso.hom_inv_id,
    comp_id, mapBifunctorRightUnitor_inv_naturality, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Unitor (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
J : Type u_4
inst : Zero I₂
r : I₁ × I₂ × I₃ → J
π : I₁ × I₃ → J
τ : TriangleIndexData r π
i₁ : I₁
i₃ : I₃
⊢ r (i₁, 0, i₃) = π (i₁, i₃)
have rw : π ((i₁, 0, i₃).1, τ.p₂₃ (i₁, 0, i₃).2) = π (i₁, i₃)
Tactic: rw [← τ.hp₂₃, τ.h₃ i₃]