awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Braiding (goal)
Goal:
I : Type u_1
inst : AddCommMonoid I
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : MonoidalCategory.{v_1, u_2} C
X Y : GradedObject I C
inst_3 : SymmetricCategory.{v_1, u_2} C
inst_4 : HasTensor.{u_1, v_1, u_2} X Y
inst_5 : HasTensor.{u_1, v_1, u_2} Y X
⊢ CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} Y X) (Iso.hom (braiding X Y)) (Iso.hom (braiding Y X)) =
    𝟙 (tensorObj.{u_1, v_1, u_2} X Y)
have dsimp : Eq (α := tensorObj.{u_1, v_1, u_2} X Y ⟶ tensorObj.{u_1, v_1, u_2} X Y)
  (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} Y X)
    (fun (k : I) ↦ tensorObjDesc fun (i j : I) (hij : i + j = k) ↦ Iso.hom (β_ (X i) (Y j)) ≫ ιTensorObj Y X j i k sorry)
    fun (k : I) ↦ tensorObjDesc fun (i j : I) (hij : i + j = k) ↦ Iso.hom (β_ (Y i) (X j)) ≫ ιTensorObj X Y j i k sorry)
  (𝟙 (tensorObj.{u_1, v_1, u_2} X Y))
Tactic: dsimp [braiding]
-- 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}
⊢ 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 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) 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
-- 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}
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))
have pos : ∀ (h : (0, j') ∈ p ⁻¹' {j}),
  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}) (0, 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}) (0, 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}) (0, j') h))
Tactic: subst hi
Cleared hypotheses: i, h, hi
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Unitor (hypothesis)
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)
j' : J
h : (0, j') ∈ p ⁻¹' {j}
⊢ 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}) (0, 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}) (0, 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}) (0, j') h))
have h₁ : j' = j
Tactic: simp only [Set.mem_preimage, hp, Set.mem_singleton_iff] at h
-- 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}
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))
have neg : 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: apply IsInitial.hom_ext
-- 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 : GradedObject J D
inst_6 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).HasMap p
j : 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))
have 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 sorry)
      (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: dsimp [mapBifunctorLeftUnitor]
-- 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 : GradedObject J D
inst_6 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).HasMap p
j : 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)
have 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) sorry) :
    (((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) 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))
  (NatTrans.app (F.map (Iso.hom (singleObjApplyIso 0 X))) (Y j) ≫ e.hom.app (Y 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 : 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 (α := (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))
have 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))
Tactic: rw [mapBifunctorLeftUnitorCofan_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 : 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
⊢ 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)) φ))
have 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)
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 : 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.{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)
have 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))
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 : 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.{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))
have 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 sorry)
  (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 sorry))
Tactic: rw [mapBifunctorLeftUnitor_inv_apply, mapBifunctorLeftUnitor_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 : 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 ⋯)
    (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 ⋯))
have 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 sorry)
  (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 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 : 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 ⋯)
    (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 ⋯))
have 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 sorry)
  (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 sorry)
Tactic: rw [Functor.map_id, NatTrans.id_app, id_comp, ← NatTrans.naturality_assoc,
    ← NatTrans.naturality_assoc]