ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>sq : CategoryTheory.Square C<VAR>F : CategoryTheory.Functor C D<GOAL>(sq.map F).f₂₄ = F.map sq.f₂₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>sq : CategoryTheory.Square C<VAR>F : CategoryTheory.Functor C D<GOAL>(sq.map F).f₁₂ = F.map sq.f₁₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>sq : CategoryTheory.Square C<VAR>F : CategoryTheory.Functor C D<GOAL>(sq.map F).X₃ = F.obj sq.X₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>sq : CategoryTheory.Square C<VAR>F : CategoryTheory.Functor C D<GOAL>(sq.map F).X₁ = F.obj sq.X₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>sq : CategoryTheory.Square C<VAR>F : CategoryTheory.Functor C D<GOAL>(sq.map F).X₄ = F.obj sq.X₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>sq : CategoryTheory.Square C<VAR>F : CategoryTheory.Functor C D<GOAL>(sq.map F).X₂ = F.obj sq.X₂
<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<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), ((CategoryTheory.Functor.mapSquare C F).map φ).τ₁ = F.map φ.τ₁
<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<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), ((CategoryTheory.Functor.mapSquare C F).map φ).τ₂ = F.map φ.τ₂
<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<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), ((CategoryTheory.Functor.mapSquare C F).map φ).τ₃ = F.map φ.τ₃
<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<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), ((CategoryTheory.Functor.mapSquare C F).map φ).τ₄ = F.map φ.τ₄
<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>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Functor.mapSquare C F).obj sq = sq.map F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>Y : Cᵒᵖ<GOAL>(CategoryTheory.yoneda.obj X).obj Y = (Opposite.unop Y ⟶ X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>∀ {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y) (g : Opposite.unop X_1 ⟶ X), (CategoryTheory.yoneda.obj X).map f g = CategoryTheory.CategoryStruct.comp f.unop g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : C} (f : X ⟶ Y) (Y_1 : Cᵒᵖ) (g : ((fun X => { obj := fun Y => Opposite.unop Y ⟶ X, map := fun {X_1 Y} f g => CategoryTheory.CategoryStruct.comp f.unop g, map_id := ⋯, map_comp := ⋯ }) X).obj Y_1), (CategoryTheory.yoneda.map f).app Y_1 g = CategoryTheory.CategoryStruct.comp g f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (Y_1 : C) (g : ((fun X => { obj := fun Y => Opposite.unop X ⟶ Y, map := fun {X_1 Y} f g => CategoryTheory.CategoryStruct.comp g f, map_id := ⋯, map_comp := ⋯ }) X).obj Y_1), (CategoryTheory.coyoneda.map f).app Y_1 g = CategoryTheory.CategoryStruct.comp f.unop g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : Cᵒᵖ<GOAL>∀ {X_1 Y : C} (f : X_1 ⟶ Y) (g : Opposite.unop X ⟶ X_1), (CategoryTheory.coyoneda.obj X).map f g = CategoryTheory.CategoryStruct.comp g f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : Cᵒᵖ<VAR>Y : C<GOAL>(CategoryTheory.coyoneda.obj X).obj Y = (Opposite.unop X ⟶ Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : Opposite.op X ⟶ Opposite.op Y<GOAL>(CategoryTheory.yoneda.obj X).map f (CategoryTheory.CategoryStruct.id X) = (CategoryTheory.yoneda.map f.unop).app (Opposite.op Y) (CategoryTheory.CategoryStruct.id Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>α : CategoryTheory.yoneda.obj X ⟶ CategoryTheory.yoneda.obj Y<VAR>Z Z' : C<VAR>f : Z ⟶ Z'<VAR>h : Z' ⟶ X<GOAL>CategoryTheory.CategoryStruct.comp f (α.app (Opposite.op Z') h) = α.app (Opposite.op Z) (CategoryTheory.CategoryStruct.comp f h)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : CategoryTheory.yoneda.obj X ⟶ CategoryTheory.yoneda.obj Y<GOAL>CategoryTheory.Yoneda.fullyFaithful.preimage f = f.app (Opposite.op X) (CategoryTheory.CategoryStruct.id X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso (CategoryTheory.yoneda.map f)<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : Cᵒᵖ<VAR>α : CategoryTheory.coyoneda.obj X ⟶ CategoryTheory.coyoneda.obj Y<VAR>Z Z' : C<VAR>f : Z' ⟶ Z<VAR>h : Opposite.unop X ⟶ Z'<GOAL>CategoryTheory.CategoryStruct.comp (α.app Z' h) f = α.app Z (CategoryTheory.CategoryStruct.comp h f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : Cᵒᵖ<VAR>f : CategoryTheory.coyoneda.obj X ⟶ CategoryTheory.coyoneda.obj Y<GOAL>CategoryTheory.Coyoneda.fullyFaithful.preimage f = Quiver.Hom.op (f.app (Opposite.unop X) (CategoryTheory.CategoryStruct.id (Opposite.unop X)))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso (CategoryTheory.coyoneda.map f)<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>∀ (X_1 : Cᵒᵖ) (a : (CategoryTheory.yoneda.obj X).obj X_1), (CategoryTheory.Coyoneda.objOpOp X).inv.app X_1 a = (CategoryTheory.opEquiv (Opposite.op X) X_1).symm a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>∀ (X_1 : Cᵒᵖ) (a : (CategoryTheory.coyoneda.obj (Opposite.op (Opposite.op X))).obj X_1), (CategoryTheory.Coyoneda.objOpOp X).hom.app X_1 a = (CategoryTheory.opEquiv (Opposite.op X) X_1) a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>self : F.Representable<GOAL>∃ X, Nonempty (CategoryTheory.yoneda.obj X ≅ F)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>F : CategoryTheory.Functor C (Type v₁)<VAR>self : F.Corepresentable<GOAL>∃ X, Nonempty (CategoryTheory.coyoneda.obj X ≅ F)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>hF : F.Representable<VAR>X : Cᵒᵖ<VAR>f : Opposite.unop X ⟶ F.reprX<GOAL>(F.reprW.app X).hom f = F.map f.op F.reprx
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>F : CategoryTheory.Functor C (Type v₁)<VAR>hF : F.Corepresentable<VAR>X : C<VAR>f : F.coreprX ⟶ X<GOAL>(F.coreprW.app X).hom f = F.map f F.coreprx
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>G : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>i : F ≅ G<VAR>F.Representable<GOAL>G.Representable
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>F : CategoryTheory.Functor C (Type v₁)<VAR>G : CategoryTheory.Functor C (Type v₁)<VAR>i : F ≅ G<VAR>F.Corepresentable<GOAL>G.Corepresentable
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>f : CategoryTheory.yoneda.obj X ⟶ F<GOAL>CategoryTheory.yonedaEquiv f = f.app (Opposite.op X) (CategoryTheory.CategoryStruct.id X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>x : F.obj (Opposite.op X)<VAR>Y : Cᵒᵖ<VAR>f : Opposite.unop Y ⟶ X<GOAL>(CategoryTheory.yonedaEquiv.symm x).app Y f = F.map f.op x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>f : CategoryTheory.yoneda.obj X ⟶ F<VAR>g : Y ⟶ X<GOAL>F.map g.op (CategoryTheory.yonedaEquiv f) = CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map g) f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : Cᵒᵖ<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>f : CategoryTheory.yoneda.obj (Opposite.unop X) ⟶ F<VAR>g : X ⟶ Y<GOAL>F.map g (CategoryTheory.yonedaEquiv f) = CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map g.unop) f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>F G : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>α : CategoryTheory.yoneda.obj X ⟶ F<VAR>β : F ⟶ G<GOAL>CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = β.app (Opposite.op X) (CategoryTheory.yonedaEquiv α)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.yonedaEquiv (CategoryTheory.yoneda.map f) = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>t : F.obj X<GOAL>CategoryTheory.yonedaEquiv.symm (F.map f t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f.unop) (CategoryTheory.yonedaEquiv.symm t)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P Q : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>f g : P ⟶ Q<VAR>h : ∀ (X : C) (p : CategoryTheory.yoneda.obj X ⟶ P), CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp p g<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P Q : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>α : P ⟶ Q<VAR>x : (CategoryTheory.yonedaEvaluation C).obj P<GOAL>((CategoryTheory.yonedaEvaluation C).map α x).down = α.2.app Q.1 (P.2.map α.1 x.down)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>x y : (CategoryTheory.yonedaPairing C).obj X<VAR>w : ∀ (Y : Cᵒᵖ), x.app Y = y.app Y<GOAL>x = y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P Q : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>α : P ⟶ Q<VAR>β : (CategoryTheory.yonedaPairing C).obj P<GOAL>(CategoryTheory.yonedaPairing C).map α β = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map α.1.unop) (CategoryTheory.CategoryStruct.comp β α.2)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : ∀ (T : C), Function.Bijective fun x => CategoryTheory.CategoryStruct.comp x f<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>F : CategoryTheory.Functor C (Type v₁)<VAR>f : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F<GOAL>CategoryTheory.coyonedaEquiv f = f.app X (CategoryTheory.CategoryStruct.id X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>F : CategoryTheory.Functor C (Type v₁)<VAR>x : F.obj X<VAR>Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.coyonedaEquiv.symm x).app Y f = F.map f x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>F : CategoryTheory.Functor C (Type v₁)<VAR>f : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F<VAR>g : X ⟶ Y<GOAL>F.map g (CategoryTheory.coyonedaEquiv f) = CategoryTheory.coyonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map g.op) f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>F G : CategoryTheory.Functor C (Type v₁)<VAR>α : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F<VAR>β : F ⟶ G<GOAL>CategoryTheory.coyonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = β.app X (CategoryTheory.coyonedaEquiv α)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.coyonedaEquiv (CategoryTheory.coyoneda.map f.op) = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : CategoryTheory.Functor C (Type v₁)<VAR>t : F.obj X<GOAL>CategoryTheory.coyonedaEquiv.symm (F.map f t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map f.op) (CategoryTheory.coyonedaEquiv.symm t)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P Q : C × CategoryTheory.Functor C (Type v₁)<VAR>α : P ⟶ Q<VAR>x : (CategoryTheory.coyonedaEvaluation C).obj P<GOAL>((CategoryTheory.coyonedaEvaluation C).map α x).down = α.2.app Q.1 (P.2.map α.1 x.down)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C × CategoryTheory.Functor C (Type v₁)<VAR>x y : (CategoryTheory.coyonedaPairing C).obj X<VAR>w : ∀ (Y : C), x.app Y = y.app Y<GOAL>x = y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P Q : C × CategoryTheory.Functor C (Type v₁)<VAR>α : P ⟶ Q<VAR>β : (CategoryTheory.coyonedaPairing C).obj P<GOAL>(CategoryTheory.coyonedaPairing C).map α β = CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map α.1.op) (CategoryTheory.CategoryStruct.comp β α.2)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : ∀ (T : C), Function.Bijective fun x => CategoryTheory.CategoryStruct.comp f x<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{v₁, u_1} D<VAR>F : CategoryTheory.Functor C D<VAR>Y : C<VAR>X : Cᵒᵖ<VAR>f : Opposite.unop X ⟶ Y<GOAL>(CategoryTheory.yonedaMap F Y).app X f = F.map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>A : Type w<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>self : W.IsCompatibleWithShift A<VAR>a : A<GOAL>W.inverseImage (CategoryTheory.shiftFunctor C a) = W
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>A : Type w<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>W.IsCompatibleWithShift A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>a : A<GOAL>W ((CategoryTheory.shiftFunctor C a).map f) ↔ W f
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>A : Type w<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>W.IsCompatibleWithShift A<VAR>a : A<GOAL>W.IsInvertedBy ((CategoryTheory.shiftFunctor C a).comp L)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>A : Type w<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>F : CategoryTheory.Functor C E<VAR>F' : CategoryTheory.Functor D E<VAR>CategoryTheory.Localization.Lifting L W F F'<VAR>CategoryTheory.HasShift D A<VAR>CategoryTheory.HasShift E A<VAR>L.CommShift A<VAR>F.CommShift A<VAR>a : A<VAR>X : C<GOAL>(CategoryTheory.Functor.commShiftOfLocalization.iso L W F F' a).hom.app (L.obj X) = CategoryTheory.CategoryStruct.comp (F'.map ((L.commShiftIso a).inv.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.Lifting.iso L W F F').hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).hom.app X) ((CategoryTheory.shiftFunctor E a).map ((CategoryTheory.Localization.Lifting.iso L W F F').inv.app X))))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>A : Type w<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>F : CategoryTheory.Functor C E<VAR>F' : CategoryTheory.Functor D E<VAR>CategoryTheory.Localization.Lifting L W F F'<VAR>CategoryTheory.HasShift D A<VAR>CategoryTheory.HasShift E A<VAR>L.CommShift A<VAR>F.CommShift A<VAR>a : A<VAR>X : C<GOAL>(CategoryTheory.Functor.commShiftOfLocalization.iso L W F F' a).inv.app (L.obj X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor E a).map ((CategoryTheory.Localization.Lifting.iso L W F F').hom.app X)) (CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.Lifting.iso L W F F').inv.app ((CategoryTheory.shiftFunctor C a).obj X)) (F'.map ((L.commShiftIso a).hom.app X))))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>A : Type w<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>F : CategoryTheory.Functor C E<VAR>F' : CategoryTheory.Functor D E<VAR>CategoryTheory.Localization.Lifting L W F F'<VAR>CategoryTheory.HasShift D A<VAR>CategoryTheory.HasShift E A<VAR>L.CommShift A<VAR>F.CommShift A<VAR>a : A<VAR>X : C<GOAL>(F'.commShiftIso a).hom.app (L.obj X) = CategoryTheory.CategoryStruct.comp (F'.map ((L.commShiftIso a).inv.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.Lifting.iso L W F F').hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).hom.app X) ((CategoryTheory.shiftFunctor E a).map ((CategoryTheory.Localization.Lifting.iso L W F F').inv.app X))))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>A : Type w<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>F : CategoryTheory.Functor C E<VAR>F' : CategoryTheory.Functor D E<VAR>CategoryTheory.Localization.Lifting L W F F'<VAR>CategoryTheory.HasShift D A<VAR>CategoryTheory.HasShift E A<VAR>L.CommShift A<VAR>F.CommShift A<VAR>a : A<VAR>X : C<GOAL>(F'.commShiftIso a).inv.app (L.obj X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor E a).map ((CategoryTheory.Localization.Lifting.iso L W F F').hom.app X)) (CategoryTheory.CategoryStruct.comp ((F.commShiftIso a).inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.Lifting.iso L W F F').inv.app ((CategoryTheory.shiftFunctor C a).obj X)) (F'.map ((L.commShiftIso a).hom.app X))))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f f) F<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.Mono (F.map f)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan f f) F<VAR>CategoryTheory.Mono (F.map f)<GOAL>CategoryTheory.Mono f
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f f) F<VAR>CategoryTheory.Epi f<GOAL>CategoryTheory.Epi (F.map f)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span f f) F<VAR>CategoryTheory.Epi (F.map f)<GOAL>CategoryTheory.Epi f
<VAR>α : Type u₁<VAR>X : CategoryTheory.Discrete α<GOAL>{ as := X.as } = X
<VAR>α : Type u₁<VAR>as : α<GOAL>(CategoryTheory.discreteEquiv.symm as).as = as
<VAR>α : Type u₁<VAR>self : CategoryTheory.Discrete α<GOAL>CategoryTheory.discreteEquiv self = self.as
<VAR>α : Type u₁<VAR>X Y : CategoryTheory.Discrete α<VAR>i : X ⟶ Y<GOAL>X.as = Y.as
<VAR>α : Type u₁<VAR>X : CategoryTheory.Discrete α<GOAL>{ down := { down := ⋯ } } = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>I : Type u₁<VAR>F : I → C<VAR>i : I<GOAL>(CategoryTheory.Discrete.functor F).obj { as := i } = F i
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>I : Type u₁<VAR>F : I → C<VAR>i : CategoryTheory.Discrete I<VAR>f : i ⟶ i<GOAL>(CategoryTheory.Discrete.functor F).map f = CategoryTheory.CategoryStruct.id (F i.as)
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>I : Type u₁<VAR>F : I → C<VAR>X : CategoryTheory.Discrete I<GOAL>(CategoryTheory.Discrete.functor F).obj X = F X.as
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>I : Type u₁<VAR>J : Type u₁'<VAR>f : J → C<VAR>g : I → J<VAR>X : CategoryTheory.Discrete I<GOAL>(CategoryTheory.Discrete.functorComp f g).hom.app X = CategoryTheory.CategoryStruct.id (f (g X.as))
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>I : Type u₁<VAR>J : Type u₁'<VAR>f : J → C<VAR>g : I → J<VAR>X : CategoryTheory.Discrete I<GOAL>(CategoryTheory.Discrete.functorComp f g).inv.app X = CategoryTheory.CategoryStruct.id (f (g X.as))
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>I : Type u₁<VAR>F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C<VAR>f : (i : CategoryTheory.Discrete I) → F.obj i ⟶ G.obj i<VAR>i : CategoryTheory.Discrete I<GOAL>(CategoryTheory.Discrete.natTrans f).app i = f i
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>I : Type u₁<VAR>F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C<VAR>f : (i : CategoryTheory.Discrete I) → F.obj i ≅ G.obj i<VAR>X : CategoryTheory.Discrete I<GOAL>(CategoryTheory.Discrete.natIso f).inv.app X = (f X).inv
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>I : Type u₁<VAR>F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C<VAR>f : (i : CategoryTheory.Discrete I) → F.obj i ≅ G.obj i<VAR>X : CategoryTheory.Discrete I<GOAL>(CategoryTheory.Discrete.natIso f).hom.app X = (f X).hom
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>I : Type u₁<VAR>F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C<VAR>f : (i : CategoryTheory.Discrete I) → F.obj i ≅ G.obj i<VAR>i : CategoryTheory.Discrete I<GOAL>(CategoryTheory.Discrete.natIso f).app i = f i
<VAR>I : Type u₁<VAR>J : Type u₂<VAR>e : I ≃ J<GOAL>(CategoryTheory.Discrete.equivalence e).functor = CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑e)
<VAR>I : Type u₁<VAR>J : Type u₂<VAR>e : I ≃ J<GOAL>(CategoryTheory.Discrete.equivalence e).counitIso = CategoryTheory.Discrete.natIso fun j => CategoryTheory.eqToIso ⋯
<VAR>I : Type u₁<VAR>J : Type u₂<VAR>e : I ≃ J<GOAL>(CategoryTheory.Discrete.equivalence e).unitIso = CategoryTheory.Discrete.natIso fun i => CategoryTheory.eqToIso ⋯
<VAR>I : Type u₁<VAR>J : Type u₂<VAR>e : I ≃ J<GOAL>(CategoryTheory.Discrete.equivalence e).inverse = CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑e.symm)
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>h : CategoryTheory.Discrete α ≌ CategoryTheory.Discrete β<GOAL>∀ (a : β), (CategoryTheory.Discrete.equivOfEquivalence h).symm a = (CategoryTheory.Discrete.as ∘ h.inverse.obj ∘ CategoryTheory.Discrete.mk) a
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>h : CategoryTheory.Discrete α ≌ CategoryTheory.Discrete β<GOAL>∀ (a : α), (CategoryTheory.Discrete.equivOfEquivalence h) a = (CategoryTheory.Discrete.as ∘ h.functor.obj ∘ CategoryTheory.Discrete.mk) a
<VAR>α : Type u₁<GOAL>∀ (a : CategoryTheory.Discrete α), (CategoryTheory.Discrete.opposite α).inverse.obj a = Opposite.op a
<VAR>α : Type u₁<VAR>X : (CategoryTheory.Discrete α)ᵒᵖ<GOAL>((CategoryTheory.Discrete.opposite α).functor.obj X).as = (Opposite.unop X).as
<VAR>J : Type v₁<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>F : CategoryTheory.Functor (CategoryTheory.Discrete J) C<VAR>j : CategoryTheory.Discrete J<VAR>f : j ⟶ j<GOAL>F.map f = CategoryTheory.CategoryStruct.id (F.obj j)
<VAR>J : Type u₂<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>(CategoryTheory.piEquivalenceFunctorDiscrete J C).counitIso = CategoryTheory.NatIso.ofComponents (fun F => CategoryTheory.NatIso.ofComponents (fun j => CategoryTheory.Iso.refl ((({ obj := fun F j => F.obj { as := j }, map := fun {X Y} f j => f.app { as := j }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun F => CategoryTheory.Discrete.functor F, map := fun {X Y} f => CategoryTheory.Discrete.natTrans fun j => f j.as, map_id := ⋯, map_comp := ⋯ }).obj F).obj j)) ⋯) ⋯