ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>self : CategoryTheory.BasedFunctor 𝒳 𝒴<GOAL>self.comp 𝒴.p = 𝒳.p
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<GOAL>(CategoryTheory.BasedFunctor.id 𝒳).toFunctor = CategoryTheory.Functor.id 𝒳.obj
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>𝒵 : CategoryTheory.BasedCategory 𝒮<VAR>F : CategoryTheory.BasedFunctor 𝒳 𝒴<VAR>G : CategoryTheory.BasedFunctor 𝒴 𝒵<GOAL>(F.comp G).toFunctor = F.comp G.toFunctor
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>F : CategoryTheory.BasedFunctor 𝒳 𝒴<GOAL>F.comp (CategoryTheory.BasedFunctor.id 𝒴) = F
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>F : CategoryTheory.BasedFunctor 𝒳 𝒴<GOAL>(CategoryTheory.BasedFunctor.id 𝒳).comp F = F
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>𝒵 : CategoryTheory.BasedCategory 𝒮<VAR>𝒜 : CategoryTheory.BasedCategory 𝒮<VAR>F : CategoryTheory.BasedFunctor 𝒳 𝒴<VAR>G : CategoryTheory.BasedFunctor 𝒴 𝒵<VAR>H : CategoryTheory.BasedFunctor 𝒵 𝒜<GOAL>(F.comp G).comp H = F.comp (G.comp H)
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>F : CategoryTheory.BasedFunctor 𝒳 𝒴<VAR>a : 𝒳.obj<GOAL>𝒴.p.obj (F.obj a) = 𝒳.p.obj a
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>F : CategoryTheory.BasedFunctor 𝒳 𝒴<VAR>R S : 𝒮<VAR>a b : 𝒳.obj<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>𝒴.p.IsHomLift f (F.map φ)<GOAL>𝒳.p.IsHomLift f φ
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>F : CategoryTheory.BasedFunctor 𝒳 𝒴<VAR>R S : 𝒮<VAR>a b : 𝒳.obj<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<GOAL>𝒴.p.IsHomLift f (F.map φ) ↔ 𝒳.p.IsHomLift f φ
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>F G : CategoryTheory.BasedFunctor 𝒳 𝒴<VAR>self : CategoryTheory.BasedNatTrans F G<VAR>a : 𝒳.obj<GOAL>𝒴.p.IsHomLift (CategoryTheory.CategoryStruct.id (𝒳.p.obj a)) (self.app a)
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>F G : CategoryTheory.BasedFunctor 𝒳 𝒴<VAR>α β : CategoryTheory.BasedNatTrans F G<VAR>h : α.toNatTrans = β.toNatTrans<GOAL>α = β
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>F G : CategoryTheory.BasedFunctor 𝒳 𝒴<VAR>α : CategoryTheory.BasedNatTrans F G<VAR>a : 𝒳.obj<VAR>S : 𝒮<VAR>ha : 𝒳.p.obj a = S<GOAL>𝒴.p.IsHomLift (CategoryTheory.CategoryStruct.id S) (α.app a)
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>F : CategoryTheory.BasedFunctor 𝒳 𝒴<GOAL>(CategoryTheory.BasedNatTrans.id F).toNatTrans = CategoryTheory.NatTrans.id F.toFunctor
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>F G H : CategoryTheory.BasedFunctor 𝒳 𝒴<VAR>α : CategoryTheory.BasedNatTrans F G<VAR>β : CategoryTheory.BasedNatTrans G H<GOAL>(α.comp β).toNatTrans = α.vcomp β.toNatTrans
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<GOAL>∀ {X Y Z : CategoryTheory.BasedFunctor 𝒳 𝒴} (α : CategoryTheory.BasedNatTrans X Y) (β : CategoryTheory.BasedNatTrans Y Z), CategoryTheory.CategoryStruct.comp α β = α.comp β
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>F : CategoryTheory.BasedFunctor 𝒳 𝒴<GOAL>CategoryTheory.CategoryStruct.id F = CategoryTheory.BasedNatTrans.id F
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>F G : CategoryTheory.BasedFunctor 𝒳 𝒴<VAR>α β : F ⟶ G<VAR>h : α.toNatTrans = β.toNatTrans<GOAL>α = β
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<GOAL>∀ {X Y : CategoryTheory.BasedFunctor 𝒳 𝒴} (α : X ⟶ Y), (CategoryTheory.BasedNatTrans.forgetful 𝒳 𝒴).map α = α.toNatTrans
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>F : CategoryTheory.BasedFunctor 𝒳 𝒴<GOAL>(CategoryTheory.BasedNatTrans.forgetful 𝒳 𝒴).obj F = F.toFunctor
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>F : CategoryTheory.BasedFunctor 𝒳 𝒴<GOAL>(CategoryTheory.BasedNatIso.id F).inv = CategoryTheory.CategoryStruct.id F
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>F : CategoryTheory.BasedFunctor 𝒳 𝒴<GOAL>(CategoryTheory.BasedNatIso.id F).hom = CategoryTheory.CategoryStruct.id F
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>F G : CategoryTheory.BasedFunctor 𝒳 𝒴<VAR>α : F ⟶ G<VAR>CategoryTheory.IsIso α.toNatTrans<GOAL>CategoryTheory.IsIso α
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>𝒵 : CategoryTheory.BasedCategory 𝒮<VAR>F : CategoryTheory.BasedFunctor 𝒳 𝒴<VAR>G H : CategoryTheory.BasedFunctor 𝒴 𝒵<VAR>α : G ⟶ H<GOAL>(CategoryTheory.BasedCategory.whiskerLeft F α).toNatTrans = CategoryTheory.whiskerLeft F.toFunctor α.toNatTrans
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<VAR>𝒴 : CategoryTheory.BasedCategory 𝒮<VAR>𝒵 : CategoryTheory.BasedCategory 𝒮<VAR>F G : CategoryTheory.BasedFunctor 𝒳 𝒴<VAR>α : F ⟶ G<VAR>H : CategoryTheory.BasedFunctor 𝒴 𝒵<GOAL>(CategoryTheory.BasedCategory.whiskerRight α H).toNatTrans = CategoryTheory.whiskerRight α.toNatTrans H.toFunctor
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>𝒳 : CategoryTheory.BasedCategory 𝒮<GOAL>CategoryTheory.CategoryStruct.id 𝒳 = CategoryTheory.BasedFunctor.id 𝒳
<VAR>𝒮 : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<GOAL>∀ {X Y Z : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor X Y) (G : CategoryTheory.BasedFunctor Y Z), CategoryTheory.CategoryStruct.comp F G = F.comp G
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsConnected J<VAR>B : C<VAR>F : J ⥤ CategoryTheory.Over B<VAR>c : CategoryTheory.Limits.Cone (F ⋙ CategoryTheory.Over.forget B)<GOAL>(CategoryTheory.Over.CreatesConnected.raiseCone c).pt = CategoryTheory.Over.mk (c.π.app (Classical.arbitrary J) ≫ (F.obj (Classical.arbitrary J)).hom)
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsConnected J<VAR>B : C<VAR>F : J ⥤ CategoryTheory.Over B<VAR>c : CategoryTheory.Limits.Cone (F ⋙ CategoryTheory.Over.forget B)<VAR>j : J<GOAL>(CategoryTheory.Over.CreatesConnected.raiseCone c).π.app j = CategoryTheory.Over.homMk (c.π.app j) ⋯
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.IsConnected J<VAR>B : C<VAR>F : J ⥤ CategoryTheory.Over B<VAR>c : CategoryTheory.Limits.Cone (F ⋙ CategoryTheory.Over.forget B)<GOAL>(CategoryTheory.Over.forget B).mapCone (CategoryTheory.Over.CreatesConnected.raiseCone c) = c
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>X : C<GOAL>(CategoryTheory.Functor.CommShift.isoZero F A).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero D A).hom.app (F.obj X)) (F.map ((CategoryTheory.shiftFunctorZero C A).inv.app X))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>X : C<GOAL>(CategoryTheory.Functor.CommShift.isoZero F A).hom.app X = CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorZero C A).hom.app X)) ((CategoryTheory.shiftFunctorZero D A).inv.app (F.obj X))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>a b c : A<VAR>h : a + b = c<VAR>e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)<VAR>e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)<VAR>X : C<GOAL>(CategoryTheory.Functor.CommShift.isoAdd' h e₁ e₂).hom.app X = CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd' C a b c h).hom.app X)) (CategoryTheory.CategoryStruct.comp (e₂.hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (e₁.hom.app X)) ((CategoryTheory.shiftFunctorAdd' D a b c h).inv.app (F.obj X))))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>a b c : A<VAR>h : a + b = c<VAR>e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)<VAR>e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)<VAR>X : C<GOAL>(CategoryTheory.Functor.CommShift.isoAdd' h e₁ e₂).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' D a b c h).hom.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (e₁.inv.app X)) (CategoryTheory.CategoryStruct.comp (e₂.inv.app ((CategoryTheory.shiftFunctor C a).obj X)) (F.map ((CategoryTheory.shiftFunctorAdd' C a b c h).inv.app X))))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>a b : A<VAR>e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)<VAR>e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)<VAR>X : C<GOAL>(CategoryTheory.Functor.CommShift.isoAdd e₁ e₂).hom.app X = CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).hom.app X)) (CategoryTheory.CategoryStruct.comp (e₂.hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (e₁.hom.app X)) ((CategoryTheory.shiftFunctorAdd D a b).inv.app (F.obj X))))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>a b : A<VAR>e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)<VAR>e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)<VAR>X : C<GOAL>(CategoryTheory.Functor.CommShift.isoAdd e₁ e₂).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D a b).hom.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (e₁.inv.app X)) (CategoryTheory.CategoryStruct.comp (e₂.inv.app ((CategoryTheory.shiftFunctor C a).obj X)) (F.map ((CategoryTheory.shiftFunctorAdd C a b).inv.app X))))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>self : F.CommShift A<GOAL>CategoryTheory.Functor.CommShift.iso 0 = CategoryTheory.Functor.CommShift.isoZero F A
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>self : F.CommShift A<VAR>a b : A<GOAL>CategoryTheory.Functor.CommShift.iso (a + b) = CategoryTheory.Functor.CommShift.isoAdd (CategoryTheory.Functor.CommShift.iso a) (CategoryTheory.Functor.CommShift.iso b)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>F.CommShift A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>a : A<GOAL>CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C a).map f)) ((F.commShiftIso a).hom.app Y) = CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).hom.app X) ((CategoryTheory.shiftFunctor D a).map (F.map f))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>F.CommShift A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>a : A<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (F.map f)) ((F.commShiftIso a).inv.app Y) = CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).inv.app X) (F.map ((CategoryTheory.shiftFunctor C a).map f))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>F.CommShift A<GOAL>F.commShiftIso 0 = CategoryTheory.Functor.CommShift.isoZero F A
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>F.CommShift A<VAR>a b : A<GOAL>F.commShiftIso (a + b) = CategoryTheory.Functor.CommShift.isoAdd (F.commShiftIso a) (F.commShiftIso b)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>F.CommShift A<VAR>a b c : A<VAR>h : a + b = c<GOAL>F.commShiftIso c = CategoryTheory.Functor.CommShift.isoAdd' h (F.commShiftIso a) (F.commShiftIso b)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a : A<VAR>X : C<GOAL>((CategoryTheory.Functor.id C).commShiftIso a).hom.app X = CategoryTheory.CategoryStruct.id (((CategoryTheory.shiftFunctor C a).comp (CategoryTheory.Functor.id C)).obj X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a : A<VAR>X : C<GOAL>((CategoryTheory.Functor.id C).commShiftIso a).inv.app X = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.id C).comp (CategoryTheory.shiftFunctor C a)).obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>CategoryTheory.Category.{u_8, u_3} E<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>CategoryTheory.HasShift E A<VAR>F.CommShift A<VAR>G.CommShift A<VAR>a : A<VAR>X : C<GOAL>((F.comp G).commShiftIso a).hom.app X = CategoryTheory.CategoryStruct.comp (G.map ((F.commShiftIso a).hom.app X)) ((G.commShiftIso a).hom.app (F.obj X))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>CategoryTheory.Category.{u_8, u_3} E<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>CategoryTheory.HasShift E A<VAR>F.CommShift A<VAR>G.CommShift A<VAR>a : A<VAR>X : C<GOAL>((F.comp G).commShiftIso a).inv.app X = CategoryTheory.CategoryStruct.comp ((G.commShiftIso a).inv.app (F.obj X)) (G.map ((F.commShiftIso a).inv.app X))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>B : Type u_5<VAR>AddCommMonoid B<VAR>CategoryTheory.HasShift C B<VAR>CategoryTheory.HasShift D B<VAR>F.CommShift B<VAR>X : C<VAR>a b : B<GOAL>F.map ((CategoryTheory.shiftFunctorComm C a b).hom.app X) = CategoryTheory.CategoryStruct.comp ((F.commShiftIso b).hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((F.commShiftIso a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm D a b).hom.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map ((F.commShiftIso b).inv.app X)) ((F.commShiftIso a).inv.app ((CategoryTheory.shiftFunctor C b).obj X)))))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>F.CommShift A<VAR>X : C<VAR>a b : A<VAR>h : a + b = 0<GOAL>F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).hom.app X) = CategoryTheory.CategoryStruct.comp ((F.commShiftIso b).hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((F.commShiftIso a).hom.app X)) ((CategoryTheory.shiftFunctorCompIsoId D a b h).hom.app (F.obj X)))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>F.CommShift A<VAR>X : C<VAR>a b : A<VAR>h : a + b = 0<GOAL>F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).inv.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId D a b h).inv.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((F.commShiftIso a).inv.app X)) ((F.commShiftIso b).inv.app ((CategoryTheory.shiftFunctor C a).obj X)))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>F₁ F₂ : CategoryTheory.Functor C D<VAR>τ : F₁ ⟶ F₂<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>F₁.CommShift A<VAR>F₂.CommShift A<VAR>self : CategoryTheory.NatTrans.CommShift τ A<VAR>a : A<GOAL>CategoryTheory.CategoryStruct.comp (F₁.commShiftIso a).hom (CategoryTheory.whiskerRight τ (CategoryTheory.shiftFunctor D a)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.shiftFunctor C a) τ) (F₂.commShiftIso a).hom
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>F₁ F₂ : CategoryTheory.Functor C D<VAR>τ : F₁ ⟶ F₂<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>F₁.CommShift A<VAR>F₂.CommShift A<VAR>CategoryTheory.NatTrans.CommShift τ A<VAR>a : A<GOAL>CategoryTheory.CategoryStruct.comp (F₁.commShiftIso a).hom (CategoryTheory.whiskerRight τ (CategoryTheory.shiftFunctor D a)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.shiftFunctor C a) τ) (F₂.commShiftIso a).hom
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>F₁ F₂ : CategoryTheory.Functor C D<VAR>τ : F₁ ⟶ F₂<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>F₁.CommShift A<VAR>F₂.CommShift A<VAR>CategoryTheory.NatTrans.CommShift τ A<VAR>a : A<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((F₁.commShiftIso a).hom.app X) ((CategoryTheory.shiftFunctor D a).map (τ.app X)) = CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X)) ((F₂.commShiftIso a).hom.app X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>F₁ F₂ : CategoryTheory.Functor C D<VAR>τ : F₁ ⟶ F₂<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>F₁.CommShift A<VAR>F₂.CommShift A<VAR>CategoryTheory.NatTrans.CommShift τ A<VAR>a : A<VAR>X : C<GOAL>(CategoryTheory.shiftFunctor D a).map (τ.app X) = CategoryTheory.CategoryStruct.comp ((F₁.commShiftIso a).inv.app X) (CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X)) ((F₂.commShiftIso a).hom.app X))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>F₁ F₂ : CategoryTheory.Functor C D<VAR>τ : F₁ ⟶ F₂<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>F₁.CommShift A<VAR>F₂.CommShift A<VAR>CategoryTheory.NatTrans.CommShift τ A<VAR>a : A<VAR>X : C<GOAL>τ.app ((CategoryTheory.shiftFunctor C a).obj X) = CategoryTheory.CategoryStruct.comp ((F₁.commShiftIso a).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (τ.app X)) ((F₂.commShiftIso a).inv.app X))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>F₁ F₂ : CategoryTheory.Functor C D<VAR>τ : F₁ ⟶ F₂<VAR>A : Type u_5<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>F₁.CommShift A<VAR>F₂.CommShift A<VAR>CategoryTheory.IsIso τ<VAR>CategoryTheory.NatTrans.CommShift τ A<GOAL>CategoryTheory.NatTrans.CommShift (CategoryTheory.inv τ) A
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>F G : CategoryTheory.Functor C D<VAR>e : F ≅ G<VAR>A : Type u_4<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>F.CommShift A<GOAL>CategoryTheory.NatTrans.CommShift e.hom A