ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1}) C} (θ : X ⟶ Y), CategoryTheory.Functor.equiv.functor.map θ = θ.app { as := PUnit.unit }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>Nonempty (C ≌ CategoryTheory.Discrete PUnit.{w + 1}) ↔ Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))
<VAR>w : CategoryTheory.uliftFunctor.{u, v}.EssSurj<GOAL>UnivLE.{max u v, v}
<GOAL>UnivLE.{max u v, v} ↔ CategoryTheory.uliftFunctor.{u, v}.EssSurj
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>R₁ R₂ : CategoryTheory.ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.map' 0 2 ⋯ ⋯ = 0<VAR>hR₁' : (CategoryTheory.ComposableArrows.mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (CategoryTheory.ComposableArrows.mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>h₀ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 0 ⋯)<VAR>h₁ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 1 ⋯)<VAR>h₃ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 3 ⋯)<GOAL>CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 2 ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>R₁ R₂ : CategoryTheory.ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.Exact<VAR>hR₂ : R₂.Exact<VAR>h₀ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 0 ⋯)<VAR>h₁ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 1 ⋯)<VAR>h₃ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 3 ⋯)<GOAL>CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 2 ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>R₁ R₂ : CategoryTheory.ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : (CategoryTheory.ComposableArrows.mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (CategoryTheory.ComposableArrows.mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>hR₂' : R₂.map' 1 3 ⋯ ⋯ = 0<VAR>h₀ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 0 ⋯)<VAR>h₂ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 2 ⋯)<VAR>h₃ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 3 ⋯)<GOAL>CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 1 ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>R₁ R₂ : CategoryTheory.ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.Exact<VAR>hR₂ : R₂.Exact<VAR>h₀ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 0 ⋯)<VAR>h₂ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 2 ⋯)<VAR>h₃ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 3 ⋯)<GOAL>CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 1 ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>R₁ R₂ : CategoryTheory.ComposableArrows C 4<VAR>hR₁ : R₁.Exact<VAR>hR₂ : R₂.Exact<VAR>φ : R₁ ⟶ R₂<VAR>h₀ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 0 ⋯)<VAR>h₁ : CategoryTheory.IsIso (CategoryTheory.ComposableArrows.app' φ 1 ⋯)<VAR>h₂ : CategoryTheory.IsIso (CategoryTheory.ComposableArrows.app' φ 3 ⋯)<VAR>h₃ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 4 ⋯)<GOAL>CategoryTheory.IsIso (CategoryTheory.ComposableArrows.app' φ 2 ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>R₁ R₂ : CategoryTheory.ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.map' 0 2 ⋯ ⋯ = 0<VAR>hR₁' : CategoryTheory.Epi (R₁.map' 1 2 ⋯ ⋯)<VAR>hR₂ : R₂.Exact<VAR>h₀ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 0 ⋯)<VAR>h₁ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 1 ⋯)<GOAL>CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 2 ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>R₁ R₂ : CategoryTheory.ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.Exact<VAR>hR₂ : R₂.Exact<VAR>hR₁' : CategoryTheory.Epi (R₁.map' 1 2 ⋯ ⋯)<VAR>h₀ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 0 ⋯)<VAR>h₁ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 1 ⋯)<GOAL>CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 2 ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>R₁ R₂ : CategoryTheory.ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.Exact<VAR>hR₂ : R₂.map' 0 2 ⋯ ⋯ = 0<VAR>hR₂' : CategoryTheory.Mono (R₂.map' 0 1 ⋯ ⋯)<VAR>h₀ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 1 ⋯)<VAR>h₁ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 2 ⋯)<GOAL>CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 0 ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>R₁ R₂ : CategoryTheory.ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.Exact<VAR>hR₂ : R₂.Exact<VAR>hR₂' : CategoryTheory.Mono (R₂.map' 0 1 ⋯ ⋯)<VAR>h₀ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 1 ⋯)<VAR>h₁ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 2 ⋯)<GOAL>CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 0 ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>R₁ R₂ : CategoryTheory.ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.Exact<VAR>hR₂' : CategoryTheory.Mono (R₂.map' 0 1 ⋯ ⋯)<VAR>h₀ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 0 ⋯)<VAR>h₁ : CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 2 ⋯)<GOAL>CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 1 ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>R₁ R₂ : CategoryTheory.ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₂ : R₂.Exact<VAR>hR₁' : CategoryTheory.Epi (R₁.map' 1 2 ⋯ ⋯)<VAR>h₀ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 0 ⋯)<VAR>h₁ : CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 2 ⋯)<GOAL>CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 1 ⋯)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} J<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>P : CategoryTheory.Idempotents.Karoubi (J ⥤ C)<VAR>X : J<GOAL>P.p.app X ≫ P.p.app X = P.p.app X
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} J<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>P Q : CategoryTheory.Idempotents.Karoubi (J ⥤ C)<VAR>f : P ⟶ Q<VAR>X : J<GOAL>P.p.app X ≫ f.f.app X = f.f.app X
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} J<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>P Q : CategoryTheory.Idempotents.Karoubi (J ⥤ C)<VAR>f : P ⟶ Q<VAR>X : J<GOAL>f.f.app X ≫ Q.p.app X = f.f.app X
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} J<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>P Q : CategoryTheory.Idempotents.Karoubi (J ⥤ C)<VAR>f : P ⟶ Q<VAR>X : J<GOAL>P.p.app X ≫ f.f.app X = f.f.app X ≫ Q.p.app X
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>P : CategoryTheory.Idempotents.Karoubi (J ⥤ C)<VAR>j : J<GOAL>((CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P).obj j).X = P.X.obj j
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>P : CategoryTheory.Idempotents.Karoubi (J ⥤ C)<VAR>j j' : J<VAR>φ : j ⟶ j'<GOAL>((CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P).map φ).f = P.p.app j ≫ P.X.map φ
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>P : CategoryTheory.Idempotents.Karoubi (J ⥤ C)<VAR>j : J<GOAL>((CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P).obj j).p = P.p.app j
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>P Q : CategoryTheory.Idempotents.Karoubi (J ⥤ C)<VAR>f : P ⟶ Q<VAR>j : J<GOAL>((CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.map f).app j).f = f.f.app j
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>P : CategoryTheory.Idempotents.Karoubi (J ⥤ C)<GOAL>(CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding J C).obj P = CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<GOAL>∀ {X Y : CategoryTheory.Idempotents.Karoubi (J ⥤ C)} (f : X ⟶ Y), (CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding J C).map f = CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.map f
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<GOAL>CategoryTheory.Idempotents.toKaroubi (J ⥤ C) ⋙ CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding J C = (CategoryTheory.whiskeringRight J C (CategoryTheory.Idempotents.Karoubi C)).obj (CategoryTheory.Idempotents.toKaroubi C)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β : Type w<GOAL>∀ {X Y Z : (i : β) → (fun x => C) i} (f : X ⟶ Y) (g : Y ⟶ Z) (i : β), CategoryTheory.CategoryStruct.comp f g i = CategoryTheory.CategoryStruct.comp (f i) (g i)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β : Type w<VAR>X : (i : β) → (fun x => C) i<VAR>i : β<GOAL>CategoryTheory.CategoryStruct.id X i = CategoryTheory.CategoryStruct.id (X i)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β : Type u_1<VAR>X Y : CategoryTheory.GradedObject β C<VAR>f g : X ⟶ Y<VAR>h : ∀ (x : β), f x = g x<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β : Type w<VAR>b : β<VAR>X : CategoryTheory.GradedObject β C<GOAL>(CategoryTheory.GradedObject.eval b).obj X = X b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β : Type w<VAR>b : β<GOAL>∀ {X Y : CategoryTheory.GradedObject β C} (f : X ⟶ Y), (CategoryTheory.GradedObject.eval b).map f = f b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β : Type u_1<VAR>X Y : CategoryTheory.GradedObject β C<VAR>e : (i : β) → X i ≅ Y i<VAR>i : β<GOAL>(X.isoMk Y e).inv i = (e i).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β : Type u_1<VAR>X Y : CategoryTheory.GradedObject β C<VAR>e : (i : β) → X i ≅ Y i<VAR>i : β<GOAL>(X.isoMk Y e).hom i = (e i).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β : Type u_1<VAR>X Y : CategoryTheory.GradedObject β C<VAR>f : X ⟶ Y<VAR>hf : ∀ (i : β), CategoryTheory.IsIso (f i)<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u_1<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>X Y : CategoryTheory.GradedObject J C<VAR>e : X ≅ Y<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (e.hom j) (e.inv j) = CategoryTheory.CategoryStruct.id (X j)
<VAR>C : Type u_1<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>X Y : CategoryTheory.GradedObject J C<VAR>e : X ≅ Y<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (e.inv j) (e.hom j) = CategoryTheory.CategoryStruct.id (Y j)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>X Y : CategoryTheory.GradedObject J C<VAR>e : X ≅ Y<VAR>F : CategoryTheory.Functor C D<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (F.map (e.hom j)) (F.map (e.inv j)) = CategoryTheory.CategoryStruct.id (F.obj (X j))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>X Y : CategoryTheory.GradedObject J C<VAR>e : X ≅ Y<VAR>F : CategoryTheory.Functor C D<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (F.map (e.inv j)) (F.map (e.hom j)) = CategoryTheory.CategoryStruct.id (F.obj (Y j))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>X Y : CategoryTheory.GradedObject J C<VAR>e : X ≅ Y<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D E)<VAR>j : J<GOAL>∀ (Y_1 : D), CategoryTheory.CategoryStruct.comp ((F.map (e.hom j)).app Y_1) ((F.map (e.inv j)).app Y_1) = CategoryTheory.CategoryStruct.id ((F.obj (X j)).obj Y_1)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>X Y : CategoryTheory.GradedObject J C<VAR>e : X ≅ Y<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D E)<VAR>j : J<GOAL>∀ (Y_1 : D), CategoryTheory.CategoryStruct.comp ((F.map (e.inv j)).app Y_1) ((F.map (e.hom j)).app Y_1) = CategoryTheory.CategoryStruct.id ((F.obj (Y j)).obj Y_1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type u_1<VAR>x x' : CategoryTheory.GradedObject I C<VAR>h : x = x'<VAR>i : I<GOAL>CategoryTheory.eqToHom h i = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β γ : Type w<VAR>f g : β → γ<VAR>h : f = g<VAR>X : CategoryTheory.GradedObject γ C<VAR>b : β<GOAL>(CategoryTheory.GradedObject.comapEq C h).hom.app X b = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β γ : Type w<VAR>f g : β → γ<VAR>h : f = g<VAR>X : CategoryTheory.GradedObject γ C<VAR>b : β<GOAL>(CategoryTheory.GradedObject.comapEq C h).inv.app X b = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β γ : Type w<VAR>f g : β → γ<VAR>h : f = g<GOAL>CategoryTheory.GradedObject.comapEq C ⋯ = (CategoryTheory.GradedObject.comapEq C h).symm
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β γ : Type w<VAR>f g h : β → γ<VAR>k : f = g<VAR>l : g = h<GOAL>CategoryTheory.GradedObject.comapEq C ⋯ = CategoryTheory.GradedObject.comapEq C k ≪≫ CategoryTheory.GradedObject.comapEq C l
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β : Type w<VAR>X Y : β → C<VAR>h : X = Y<VAR>b : β<GOAL>CategoryTheory.eqToHom h b = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β γ : Type w<VAR>e : β ≃ γ<GOAL>(CategoryTheory.GradedObject.comapEquiv C e).inverse = CategoryTheory.GradedObject.comap C ⇑e
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β γ : Type w<VAR>e : β ≃ γ<GOAL>(CategoryTheory.GradedObject.comapEquiv C e).functor = CategoryTheory.GradedObject.comap C ⇑e.symm
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β γ : Type w<VAR>e : β ≃ γ<GOAL>(CategoryTheory.GradedObject.comapEquiv C e).unitIso = CategoryTheory.GradedObject.comapEq C ⋯ ≪≫ (CategoryTheory.Pi.comapComp (fun x => C) ⇑e ⇑e.symm).symm
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β γ : Type w<VAR>e : β ≃ γ<GOAL>(CategoryTheory.GradedObject.comapEquiv C e).counitIso = CategoryTheory.Pi.comapComp (fun x => C) ⇑e.symm ⇑e ≪≫ CategoryTheory.GradedObject.comapEq C ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>s : β<VAR>X : β → C<VAR>t : β<VAR>n : ℤ<GOAL>(CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift s C) n).obj X t = X (t + n • s)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>s : β<VAR>X Y : CategoryTheory.GradedObjectWithShift s C<VAR>f : X ⟶ Y<VAR>t : β<VAR>n : ℤ<GOAL>(CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift s C) n).map f t = f (t + n • s)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>β : Type w<VAR>X Y : CategoryTheory.GradedObject β C<VAR>b : β<GOAL>0 b = 0
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>X Y : CategoryTheory.GradedObject I C<VAR>e : X ≅ Y<VAR>p : I → J<VAR>X.HasMap p<GOAL>Y.HasMap p
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>X : CategoryTheory.GradedObject I C<VAR>p : I → J<VAR>X.HasMap p<VAR>A : C<VAR>j : J<VAR>f g : X.mapObj p j ⟶ A<VAR>hfg : ∀ (i : I) (hij : p i = j), CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) f = CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) g<GOAL>f = g
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>X : CategoryTheory.GradedObject I C<VAR>p : I → J<VAR>X.HasMap p<VAR>A : C<VAR>j : J<VAR>φ : (i : I) → p i = j → (X i ⟶ A)<VAR>i : I<VAR>hi : p i = j<GOAL>CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hi) (X.descMapObj p φ) = φ i hi
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>X : CategoryTheory.GradedObject I C<VAR>p : I → J<VAR>c : (j : J) → X.CofanMapObjFun p j<VAR>hc : (j : J) → CategoryTheory.Limits.IsColimit (c j)<GOAL>X.HasMap p
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>X : CategoryTheory.GradedObject I C<VAR>p : I → J<VAR>j : J<VAR>c : X.CofanMapObjFun p j<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>X.HasMap p<VAR>i : I<VAR>hi : p i = j<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj c ⟨i, hi⟩) (CategoryTheory.GradedObject.CofanMapObjFun.iso hc).hom = X.ιMapObj p i j hi
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>X : CategoryTheory.GradedObject I C<VAR>p : I → J<VAR>j : J<VAR>c : X.CofanMapObjFun p j<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>X.HasMap p<VAR>i : I<VAR>hi : p i = j<GOAL>CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hi) (CategoryTheory.GradedObject.CofanMapObjFun.iso hc).inv = CategoryTheory.Limits.Cofan.inj c ⟨i, hi⟩
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>X Y : CategoryTheory.GradedObject I C<VAR>φ : X ⟶ Y<VAR>p : I → J<VAR>X.HasMap p<VAR>Y.HasMap p<VAR>i : I<VAR>j : J<VAR>hij : p i = j<GOAL>CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) (CategoryTheory.GradedObject.mapMap φ p j) = CategoryTheory.CategoryStruct.comp (φ i) (Y.ιMapObj p i j hij)
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>X Y : CategoryTheory.GradedObject I C<VAR>p : I → J<VAR>X.HasMap p<VAR>Y.HasMap p<VAR>φ₁ φ₂ : X ⟶ Y<VAR>h : φ₁ = φ₂<GOAL>CategoryTheory.GradedObject.mapMap φ₁ p = CategoryTheory.GradedObject.mapMap φ₂ p
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>X : CategoryTheory.GradedObject I C<VAR>p : I → J<VAR>X.HasMap p<GOAL>CategoryTheory.GradedObject.mapMap (CategoryTheory.CategoryStruct.id X) p = CategoryTheory.CategoryStruct.id (X.mapObj p)
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>X Y Z : CategoryTheory.GradedObject I C<VAR>φ : X ⟶ Y<VAR>ψ : Y ⟶ Z<VAR>p : I → J<VAR>X.HasMap p<VAR>Y.HasMap p<VAR>Z.HasMap p<GOAL>CategoryTheory.GradedObject.mapMap (CategoryTheory.CategoryStruct.comp φ ψ) p = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap φ p) (CategoryTheory.GradedObject.mapMap ψ p)
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>X Y : CategoryTheory.GradedObject I C<VAR>e : X ≅ Y<VAR>p : I → J<VAR>X.HasMap p<VAR>Y.HasMap p<VAR>i : J<GOAL>(CategoryTheory.GradedObject.mapIso e p).hom i = CategoryTheory.GradedObject.mapMap e.hom p i
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>X Y : CategoryTheory.GradedObject I C<VAR>e : X ≅ Y<VAR>p : I → J<VAR>X.HasMap p<VAR>Y.HasMap p<VAR>i : J<GOAL>(CategoryTheory.GradedObject.mapIso e p).inv i = CategoryTheory.GradedObject.mapMap e.inv p i
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>p : I → J<VAR>∀ (j : J), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ↑(p ⁻¹' {j})) C<VAR>X : CategoryTheory.GradedObject I C<GOAL>(CategoryTheory.GradedObject.map C p).obj X = X.mapObj p
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>p : I → J<VAR>∀ (j : J), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ↑(p ⁻¹' {j})) C<GOAL>∀ {X Y : CategoryTheory.GradedObject I C} (φ : X ⟶ Y) (i : J), (CategoryTheory.GradedObject.map C p).map φ i = CategoryTheory.GradedObject.mapMap φ p i
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>K : Type u_3<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>X : CategoryTheory.GradedObject I C<VAR>p : I → J<VAR>q : J → K<VAR>r : I → K<VAR>hpqr : ∀ (i : I), q (p i) = r i<VAR>X.HasMap p<VAR>(X.mapObj p).HasMap q<GOAL>X.HasMap r
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>X : CategoryTheory.GradedObject I C<VAR>p : I → J<VAR>X.HasMap p<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>DecidableEq J<VAR>i : I<VAR>j : J<VAR>h : p i = j<GOAL>X.ιMapObjOrZero p i j = X.ιMapObj p i j h
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>X : CategoryTheory.GradedObject I C<VAR>p : I → J<VAR>X.HasMap p<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>DecidableEq J<VAR>i : I<VAR>j : J<VAR>h : p i ≠ j<GOAL>X.ιMapObjOrZero p i j = 0
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>X Y : CategoryTheory.GradedObject I C<VAR>φ : X ⟶ Y<VAR>p : I → J<VAR>X.HasMap p<VAR>Y.HasMap p<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>DecidableEq J<VAR>i : I<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (X.ιMapObjOrZero p i j) (CategoryTheory.GradedObject.mapMap φ p j) = CategoryTheory.CategoryStruct.comp (φ i) (Y.ιMapObjOrZero p i j)
<VAR>C : Type u<VAR>CategoryTheory.CategoryStruct.{v, u} C<VAR>X : C<GOAL>1 = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u<VAR>CategoryTheory.CategoryStruct.{v, u} C<VAR>X : C<VAR>xs ys : CategoryTheory.End X<GOAL>xs * ys = CategoryTheory.CategoryStruct.comp ys xs
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>r : CategoryTheory.End Y<VAR>f : X ⟶ Y<GOAL>r • f = CategoryTheory.CategoryStruct.comp f r
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : Cᵒᵖ<VAR>Y : C<VAR>r : CategoryTheory.End X<VAR>f : Opposite.unop X ⟶ Y<GOAL>r • f = CategoryTheory.CategoryStruct.comp (Quiver.Hom.unop r) f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>f : CategoryTheory.End X<GOAL>IsUnit f ↔ CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>φ₁ φ₂ : CategoryTheory.Aut X<VAR>h : φ₁.hom = φ₂.hom<GOAL>φ₁ = φ₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>f g : CategoryTheory.Aut X<GOAL>f * g = g ≪≫ f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>f : CategoryTheory.Aut X<GOAL>f⁻¹ = CategoryTheory.Iso.symm f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<GOAL>∀ (a : CategoryTheory.Aut X), (CategoryTheory.Aut.toEnd X) a = ↑((CategoryTheory.Aut.unitsEndEquivAut X).symm a)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>f : CategoryTheory.Functor C D<GOAL>∀ (a : X ⟶ X), (CategoryTheory.Functor.mapEnd X f) a = f.map a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>f : CategoryTheory.Functor C D<VAR>hf : f.FullyFaithful<VAR>X : C<GOAL>∀ (a : X ⟶ X), (hf.mulEquivEnd X) a = f.map a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>f : CategoryTheory.Functor C D<VAR>hf : f.FullyFaithful<VAR>X : C<GOAL>∀ (f_1 : f.obj X ⟶ f.obj X), (hf.mulEquivEnd X).symm f_1 = hf.preimage f_1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>f : CategoryTheory.Functor C D<VAR>hf : f.FullyFaithful<VAR>X : C<VAR>i : X ≅ X<GOAL>((hf.autMulEquivOfFullyFaithful X) i).inv = f.map i.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>f : CategoryTheory.Functor C D<VAR>hf : f.FullyFaithful<VAR>X : C<VAR>i : X ≅ X<GOAL>((hf.autMulEquivOfFullyFaithful X) i).hom = f.map i.hom