ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X Y : FintypeCat.Skeleton<GOAL>X.len = Y.len → X = Y
<VAR>n : ℕ<GOAL>Fintype.card ↑(FintypeCat.Skeleton.incl.obj (FintypeCat.Skeleton.mk n)) = n
<GOAL>CategoryTheory.IsSkeletonOf FintypeCat FintypeCat.Skeleton FintypeCat.Skeleton.incl
<VAR>J : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} J<VAR>self : CategoryTheory.CountableCategory J<GOAL>Countable J
<VAR>J : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} J<VAR>self : CategoryTheory.CountableCategory J<VAR>j j' : J<GOAL>Countable (j ⟶ j')
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>self : CategoryTheory.CommSq f g h i<GOAL>CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>p : CategoryTheory.CommSq f g h i<GOAL>CategoryTheory.CommSq g f i h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.Arrow C<VAR>h : f ⟶ g<GOAL>CategoryTheory.CommSq f.hom h.left h.right g.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>p : CategoryTheory.CommSq f g h i<GOAL>CategoryTheory.CommSq i.op h.op g.op f.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W X Y Z : Cᵒᵖ<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>p : CategoryTheory.CommSq f g h i<GOAL>CategoryTheory.CommSq i.unop h.unop g.unop f.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>i : Y ⟶ Z<VAR>g : W ≅ Y<VAR>h : X ≅ Z<VAR>p : CategoryTheory.CommSq f g.hom h.hom i<GOAL>CategoryTheory.CommSq i g.inv h.inv f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W X Y Z : C<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>f : W ≅ X<VAR>i : Y ≅ Z<VAR>p : CategoryTheory.CommSq f.hom g h i.hom<GOAL>CategoryTheory.CommSq f.inv h g i.inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W X X' Y Z Z' : C<VAR>f : W ⟶ X<VAR>f' : X ⟶ X'<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>h' : X' ⟶ Z'<VAR>i : Y ⟶ Z<VAR>i' : Z ⟶ Z'<VAR>hsq₁ : CategoryTheory.CommSq f g h i<VAR>hsq₂ : CategoryTheory.CommSq f' h h' i'<GOAL>CategoryTheory.CommSq (CategoryTheory.CategoryStruct.comp f f') g h' (CategoryTheory.CategoryStruct.comp i i')
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>W X Y Y' Z Z' : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>g' : Y ⟶ Y'<VAR>h : X ⟶ Z<VAR>h' : Z ⟶ Z'<VAR>i : Y ⟶ Z<VAR>i' : Y' ⟶ Z'<VAR>hsq₁ : CategoryTheory.CommSq f g h i<VAR>hsq₂ : CategoryTheory.CommSq i g' h' i'<GOAL>CategoryTheory.CommSq f (CategoryTheory.CategoryStruct.comp g g') (CategoryTheory.CategoryStruct.comp h h') i'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>s : CategoryTheory.CommSq f g h i<GOAL>CategoryTheory.CommSq (F.map f) (F.map g) (F.map h) (F.map i)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y : C<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CategoryTheory.CommSq f i p g<VAR>self : sq.LiftStruct<GOAL>CategoryTheory.CategoryStruct.comp i self.l = f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y : C<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CategoryTheory.CommSq f i p g<VAR>self : sq.LiftStruct<GOAL>CategoryTheory.CategoryStruct.comp self.l p = g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y : C<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CategoryTheory.CommSq f i p g<VAR>l : sq.LiftStruct<GOAL>l.op.l = l.l.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y : Cᵒᵖ<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CategoryTheory.CommSq f i p g<VAR>l : sq.LiftStruct<GOAL>l.unop.l = l.l.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y : C<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CategoryTheory.CommSq f i p g<VAR>l : sq.LiftStruct<GOAL>(CategoryTheory.CommSq.LiftStruct.opEquiv sq) l = l.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y : C<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CategoryTheory.CommSq f i p g<VAR>l : ⋯.LiftStruct<GOAL>(CategoryTheory.CommSq.LiftStruct.opEquiv sq).symm l = l.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y : C<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CategoryTheory.CommSq f i p g<VAR>self : sq.HasLift<GOAL>Nonempty sq.LiftStruct
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y : C<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CategoryTheory.CommSq f i p g<VAR>l : sq.LiftStruct<GOAL>sq.HasLift
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y : C<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CategoryTheory.CommSq f i p g<GOAL>sq.HasLift ↔ Nonempty sq.LiftStruct
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y : C<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CategoryTheory.CommSq f i p g<GOAL>sq.HasLift ↔ ⋯.HasLift
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y : Cᵒᵖ<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CategoryTheory.CommSq f i p g<GOAL>sq.HasLift ↔ ⋯.HasLift
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y : C<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CategoryTheory.CommSq f i p g<VAR>hsq : sq.HasLift<GOAL>CategoryTheory.CategoryStruct.comp i sq.lift = f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y : C<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CategoryTheory.CommSq f i p g<VAR>hsq : sq.HasLift<GOAL>CategoryTheory.CategoryStruct.comp sq.lift p = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Balanced C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<VAR>CategoryTheory.Epi f<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Balanced C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<VAR>CategoryTheory.Epi f<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Balanced C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.IsIso f ↔ CategoryTheory.Mono f ∧ CategoryTheory.Epi f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Balanced C<GOAL>CategoryTheory.Balanced Cᵒᵖ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategoryStruct D<VAR>F : D ⥤ C<VAR>self : CategoryTheory.Monoidal.InducingFunctorData F<VAR>X₁ X₂ : D<VAR>f : X₁ ⟶ X₂<VAR>Y : D<GOAL>F.map (f ▷ Y) = (self.μIso X₁ Y).inv ≫ F.map f ▷ F.obj Y ≫ (self.μIso X₂ Y).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategoryStruct D<VAR>F : D ⥤ C<VAR>self : CategoryTheory.Monoidal.InducingFunctorData F<VAR>X : D<VAR>Y₁ Y₂ : D<VAR>f : Y₁ ⟶ Y₂<GOAL>F.map (X ◁ f) = (self.μIso X Y₁).inv ≫ F.obj X ◁ F.map f ≫ (self.μIso X Y₂).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategoryStruct D<VAR>F : D ⥤ C<VAR>self : CategoryTheory.Monoidal.InducingFunctorData F<VAR>X : D<GOAL>F.map (λ_ X).hom = (((self.μIso (𝟙_ D) X).symm ≪≫ (self.εIso.symm ⊗ CategoryTheory.Iso.refl (F.obj X))) ≪≫ λ_ (F.obj X)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategoryStruct D<VAR>F : D ⥤ C<VAR>self : CategoryTheory.Monoidal.InducingFunctorData F<VAR>X : D<GOAL>F.map (ρ_ X).hom = (((self.μIso X (𝟙_ D)).symm ≪≫ (CategoryTheory.Iso.refl (F.obj X) ⊗ self.εIso.symm)) ≪≫ ρ_ (F.obj X)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategoryStruct D<VAR>F : D ⥤ C<VAR>self : CategoryTheory.Monoidal.InducingFunctorData F<VAR>X Y Z : D<GOAL>F.map (α_ X Y Z).hom = (((self.μIso (X ⊗ Y) Z).symm ≪≫ ((self.μIso X Y).symm ⊗ CategoryTheory.Iso.refl (F.obj Z))) ≪≫ α_ (F.obj X) (F.obj Y) (F.obj Z) ≪≫ (CategoryTheory.Iso.refl (F.obj X) ⊗ self.μIso Y Z) ≪≫ self.μIso X (Y ⊗ Z)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategoryStruct D<VAR>F : D ⥤ C<VAR>self : CategoryTheory.Monoidal.InducingFunctorData F<VAR>X₁ Y₁ X₂ Y₂ : D<VAR>f : X₁ ⟶ Y₁<VAR>g : X₂ ⟶ Y₂<GOAL>F.map (f ⊗ g) = (self.μIso X₁ X₂).inv ≫ (F.map f ⊗ F.map g) ≫ (self.μIso Y₁ Y₂).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategoryStruct D<VAR>F : D ⥤ C<VAR>F.Faithful<VAR>fData : CategoryTheory.Monoidal.InducingFunctorData F<GOAL>(CategoryTheory.Monoidal.fromInduced F fData).toFunctor = F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategoryStruct D<VAR>F : D ⥤ C<VAR>F.Faithful<VAR>fData : CategoryTheory.Monoidal.InducingFunctorData F<VAR>X Y : D<GOAL>(CategoryTheory.Monoidal.fromInduced F fData).μ X Y = (fData.μIso X Y).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategoryStruct D<VAR>F : D ⥤ C<VAR>F.Faithful<VAR>fData : CategoryTheory.Monoidal.InducingFunctorData F<GOAL>(CategoryTheory.Monoidal.fromInduced F fData).ε = fData.εIso.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X : D<GOAL>λ_ X = e.functor.mapIso (((e.unitIso.app (𝟙_ C)).symm ⊗ CategoryTheory.Iso.refl (e.inverse.obj X)) ≪≫ λ_ (e.inverse.obj X)) ≪≫ e.counitIso.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X : D<GOAL>∀ (x x_1 : D) (f : x ⟶ x_1), X ◁ f = e.functor.map (e.inverse.obj X ◁ e.inverse.map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X : D<GOAL>ρ_ X = e.functor.mapIso ((CategoryTheory.Iso.refl (e.inverse.obj X) ⊗ (e.unitIso.app (𝟙_ C)).symm) ≪≫ ρ_ (e.inverse.obj X)) ≪≫ e.counitIso.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>𝟙_ D = e.functor.obj (𝟙_ C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), f ⊗ g = e.functor.map (e.inverse.map f ⊗ e.inverse.map g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X Y : D<GOAL>X ⊗ Y = e.functor.obj (e.inverse.obj X ⊗ e.inverse.obj Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (X : D), f ▷ X = e.functor.map (e.inverse.map f ▷ e.inverse.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X Y Z : D<GOAL>α_ X Y Z = e.functor.mapIso (((e.unitIso.app (e.inverse.obj X ⊗ e.inverse.obj Y)).symm ⊗ CategoryTheory.Iso.refl (e.inverse.obj Z)) ≪≫ α_ (e.inverse.obj X) (e.inverse.obj Y) (e.inverse.obj Z) ≪≫ (CategoryTheory.Iso.refl (e.inverse.obj X) ⊗ e.unitIso.app (e.inverse.obj Y ⊗ e.inverse.obj Z)))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>(CategoryTheory.Monoidal.fromTransported e).ε = e.unitIso.hom.app (𝟙_ C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>(CategoryTheory.Monoidal.fromTransported e).toFunctor = e.inverse
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X Y : CategoryTheory.Monoidal.Transported e<GOAL>(CategoryTheory.Monoidal.fromTransported e).μ X Y = e.unitIso.hom.app (e.inverse.obj X ⊗ e.inverse.obj Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>(CategoryTheory.Monoidal.toTransported e).toFunctor = e.functor
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>(CategoryTheory.Monoidal.toTransported e).ε = e.symm.unit.app (e.functor.obj (𝟙_ C)) ≫ CategoryTheory.inv (e.functor.map (e.unitIso.hom.app (𝟙_ C)))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X Y : C<GOAL>(CategoryTheory.Monoidal.toTransported e).μ X Y = e.symm.unit.app (e.functor.obj (e.inverse.obj (e.functor.obj X) ⊗ e.inverse.obj (e.functor.obj Y))) ≫ CategoryTheory.inv (e.functor.map (e.unitIso.hom.app (e.inverse.obj (e.functor.obj X) ⊗ e.inverse.obj (e.functor.obj Y)))) ≫ e.functor.map (e.symm.counit.app X ⊗ e.symm.counit.app Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>(CategoryTheory.Monoidal.transportedMonoidalUnitIso e).inv = CategoryTheory.monoidalCounit (CategoryTheory.Monoidal.fromTransported e) e.symm.toAdjunction
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>(CategoryTheory.Monoidal.transportedMonoidalUnitIso e).hom = CategoryTheory.inv (CategoryTheory.monoidalCounit (CategoryTheory.Monoidal.fromTransported e) e.symm.toAdjunction)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>(CategoryTheory.Monoidal.transportedMonoidalCounitIso e).inv = CategoryTheory.monoidalUnit (CategoryTheory.Monoidal.fromTransported e) e.symm.toAdjunction
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>(CategoryTheory.Monoidal.transportedMonoidalCounitIso e).hom = CategoryTheory.inv (CategoryTheory.monoidalUnit (CategoryTheory.Monoidal.fromTransported e) e.symm.toAdjunction)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>n : ℤ<GOAL>∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).map f).hom₃ = (CategoryTheory.shiftFunctor C n).map f.hom₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>n : ℤ<GOAL>∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).map f).hom₁ = (CategoryTheory.shiftFunctor C n).map f.hom₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>n : ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>(CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).obj T = CategoryTheory.Pretriangulated.Triangle.mk (n.negOnePow • (CategoryTheory.shiftFunctor C n).map T.mor₁) (n.negOnePow • (CategoryTheory.shiftFunctor C n).map T.mor₂) (n.negOnePow • CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map T.mor₃) ((CategoryTheory.shiftFunctorComm C 1 n).hom.app T.obj₁))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>n : ℤ<GOAL>∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).map f).hom₂ = (CategoryTheory.shiftFunctor C n).map f.hom₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C).inv.app X).hom₁ = (CategoryTheory.shiftFunctorZero C ℤ).inv.app X.obj₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C).inv.app X).hom₃ = (CategoryTheory.shiftFunctorZero C ℤ).inv.app X.obj₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C).hom.app X).hom₁ = (CategoryTheory.shiftFunctorZero C ℤ).hom.app X.obj₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C).hom.app X).hom₂ = (CategoryTheory.shiftFunctorZero C ℤ).hom.app X.obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C).hom.app X).hom₃ = (CategoryTheory.shiftFunctorZero C ℤ).hom.app X.obj₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C).inv.app X).hom₂ = (CategoryTheory.shiftFunctorZero C ℤ).inv.app X.obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>a b n : ℤ<VAR>h : a + b = n<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h).inv.app X).hom₂ = (CategoryTheory.shiftFunctorAdd' C a b n h).inv.app X.obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>a b n : ℤ<VAR>h : a + b = n<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h).hom.app X).hom₂ = (CategoryTheory.shiftFunctorAdd' C a b n h).hom.app X.obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>a b n : ℤ<VAR>h : a + b = n<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h).hom.app X).hom₁ = (CategoryTheory.shiftFunctorAdd' C a b n h).hom.app X.obj₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>a b n : ℤ<VAR>h : a + b = n<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h).inv.app X).hom₃ = (CategoryTheory.shiftFunctorAdd' C a b n h).inv.app X.obj₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>a b n : ℤ<VAR>h : a + b = n<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h).hom.app X).hom₃ = (CategoryTheory.shiftFunctorAdd' C a b n h).hom.app X.obj₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>a b n : ℤ<VAR>h : a + b = n<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h).inv.app X).hom₁ = (CategoryTheory.shiftFunctorAdd' C a b n h).inv.app X.obj₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>n : ℤ<GOAL>CategoryTheory.shiftFunctor (CategoryTheory.Pretriangulated.Triangle C) n = CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<GOAL>CategoryTheory.shiftFunctorZero (CategoryTheory.Pretriangulated.Triangle C) ℤ = CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>a b : ℤ<GOAL>CategoryTheory.shiftFunctorAdd (CategoryTheory.Pretriangulated.Triangle C) a b = CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b (a + b) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>a b c : ℤ<VAR>h : a + b = c<GOAL>CategoryTheory.shiftFunctorAdd' (CategoryTheory.Pretriangulated.Triangle C) a b c h = CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b c h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<GOAL>(𝟙_ (CategoryTheory.Functor C C)).obj X = X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(𝟙_ (CategoryTheory.Functor C C)).map f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.tensorObj F G).obj X = G.obj (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.MonoidalCategory.tensorObj F G).map f = G.map (F.map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G H K : CategoryTheory.Functor C C<VAR>α : F ⟶ G<VAR>β : H ⟶ K<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.tensorHom α β).app X = CategoryTheory.CategoryStruct.comp (β.app (F.obj X)) (K.map (α.app X))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F H K : CategoryTheory.Functor C C<VAR>β : H ⟶ K<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.whiskerLeft F β).app X = β.app (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G H : CategoryTheory.Functor C C<VAR>α : F ⟶ G<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.whiskerRight α H).app X = H.map (α.app X)