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>E : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} E<VAR>F : CategoryTheory.Functor C D<VAR>hF : F.FullyFaithful<VAR>G : CategoryTheory.Functor D E<VAR>hG : G.FullyFaithful<GOAL>∀ {X Y : C} (f : (F.comp G).obj X ⟶ (F.comp G).obj Y), (hF.comp hG).preimage f = hF.preimage (hG.preimage f)
<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>F.Full<VAR>F.Faithful<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso (F.map f)<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<VAR>(F.comp G).Faithful<GOAL>F.Faithful
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F F' : CategoryTheory.Functor C D<VAR>F.Full<VAR>α : F ≅ F'<GOAL>F'.Full
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F F' : CategoryTheory.Functor C D<VAR>F.Faithful<VAR>α : F ≅ F'<GOAL>F'.Faithful
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<VAR>H : CategoryTheory.Functor C E<VAR>H.Faithful<VAR>h : F.comp G ≅ H<GOAL>F.Faithful
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<VAR>H : CategoryTheory.Functor C E<VAR>ℋ : H.Faithful<VAR>h : F.comp G = H<GOAL>F.Faithful
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C E<VAR>F.Faithful<VAR>G : CategoryTheory.Functor D E<VAR>G.Faithful<VAR>obj : C → D<VAR>h_obj : ∀ (X : C), G.obj (obj X) = F.obj X<VAR>map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)<VAR>h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)<GOAL>(CategoryTheory.Functor.Faithful.div F G obj h_obj map h_map).comp G = F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C E<VAR>F.Faithful<VAR>G : CategoryTheory.Functor D E<VAR>G.Faithful<VAR>obj : C → D<VAR>h_obj : ∀ (X : C), G.obj (obj X) = F.obj X<VAR>map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)<VAR>h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)<GOAL>(CategoryTheory.Functor.Faithful.div F G obj h_obj map h_map).Faithful
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<VAR>(F.comp G).Full<VAR>G.Faithful<GOAL>F.Full
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<VAR>H : CategoryTheory.Functor C E<VAR>H.Full<VAR>G.Faithful<VAR>h : F.comp G ≅ H<GOAL>F.Full
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F G : CategoryTheory.Functor C D<VAR>H : CategoryTheory.Functor D E<VAR>H.Full<VAR>H.Faithful<VAR>comp_iso : F.comp H ≅ G.comp H<VAR>X : C<GOAL>(CategoryTheory.Functor.fullyFaithfulCancelRight H comp_iso).hom.app X = H.preimage (comp_iso.hom.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F G : CategoryTheory.Functor C D<VAR>H : CategoryTheory.Functor D E<VAR>H.Full<VAR>H.Faithful<VAR>comp_iso : F.comp H ≅ G.comp H<VAR>X : C<GOAL>(CategoryTheory.Functor.fullyFaithfulCancelRight H comp_iso).inv.app X = H.preimage (comp_iso.inv.app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.EssentiallySmall.{w, v, u} C<GOAL>∃ S x, Nonempty (C ≌ S)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>S : Type w<VAR>CategoryTheory.SmallCategory S<VAR>e : C ≌ S<GOAL>CategoryTheory.EssentiallySmall.{w, v, u} C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>e : C ≌ D<GOAL>CategoryTheory.EssentiallySmall.{w, v, u} C ↔ CategoryTheory.EssentiallySmall.{w, v', u'} D
<VAR>α : Type u<VAR>Small.{w, u} α<GOAL>CategoryTheory.EssentiallySmall.{w, u, u} (CategoryTheory.Discrete α)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.EssentiallySmall.{max w v u, v, u} C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.LocallySmall.{w, v, u} C<VAR>X Y : C<GOAL>Small.{w, v} (X ⟶ Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>F : C ⥤ D<VAR>F.Faithful<VAR>CategoryTheory.LocallySmall.{w, v', u'} D<GOAL>CategoryTheory.LocallySmall.{w, v, u} C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>e : C ≌ D<GOAL>CategoryTheory.LocallySmall.{w, v, u} C ↔ CategoryTheory.LocallySmall.{w, v', u'} D
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.LocallySmall.{max v w, v, u} C
<VAR>C' : Type u_1<VAR>X : C'<GOAL>(CategoryTheory.ShrinkHoms.toShrinkHoms X).fromShrinkHoms = X
<VAR>C' : Type u_1<VAR>X : CategoryTheory.ShrinkHoms.{u_1} C'<GOAL>CategoryTheory.ShrinkHoms.toShrinkHoms X.fromShrinkHoms = X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.LocallySmall.{w, v, u} C<GOAL>∀ {X Y Z : CategoryTheory.ShrinkHoms.{u} C} (f : X ⟶ Y) (g : Y ⟶ Z), f ≫ g = (equivShrink (X.fromShrinkHoms ⟶ Z.fromShrinkHoms)) ((equivShrink (X.fromShrinkHoms ⟶ Y.fromShrinkHoms)).symm f ≫ (equivShrink (Y.fromShrinkHoms ⟶ Z.fromShrinkHoms)).symm g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.LocallySmall.{w, v, u} C<VAR>X : CategoryTheory.ShrinkHoms.{u} C<GOAL>𝟙 X = (equivShrink (X.fromShrinkHoms ⟶ X.fromShrinkHoms)) (𝟙 X.fromShrinkHoms)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.LocallySmall.{w, v, u} C<VAR>X : C<GOAL>(CategoryTheory.ShrinkHoms.functor C).obj X = CategoryTheory.ShrinkHoms.toShrinkHoms X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.LocallySmall.{w, v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.ShrinkHoms.functor C).map f = (equivShrink (X ⟶ Y)) f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.LocallySmall.{w, v, u} C<VAR>X : CategoryTheory.ShrinkHoms.{u} C<GOAL>(CategoryTheory.ShrinkHoms.inverse C).obj X = X.fromShrinkHoms
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.LocallySmall.{w, v, u} C<VAR>X Y : CategoryTheory.ShrinkHoms.{u} C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.ShrinkHoms.inverse C).map f = (equivShrink (X.fromShrinkHoms ⟶ Y.fromShrinkHoms)).symm f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.LocallySmall.{w, v, u} C<VAR>X : C<GOAL>(CategoryTheory.ShrinkHoms.equivalence C).unitIso.hom.app X = 𝟙 X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.LocallySmall.{w, v, u} C<VAR>X : CategoryTheory.ShrinkHoms.{u} C<GOAL>(CategoryTheory.ShrinkHoms.equivalence C).counitIso.hom.app X = (equivShrink (X.fromShrinkHoms ⟶ X.fromShrinkHoms)) (𝟙 X.fromShrinkHoms)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.LocallySmall.{w, v, u} C<VAR>X : CategoryTheory.ShrinkHoms.{u} C<GOAL>(CategoryTheory.ShrinkHoms.equivalence C).counitIso.inv.app X = (equivShrink (X.fromShrinkHoms ⟶ X.fromShrinkHoms)) (𝟙 X.fromShrinkHoms)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.LocallySmall.{w, v, u} C<VAR>X : CategoryTheory.ShrinkHoms.{u} C<GOAL>(CategoryTheory.ShrinkHoms.equivalence C).inverse.obj X = X.fromShrinkHoms
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.LocallySmall.{w, v, u} C<VAR>X : C<GOAL>(CategoryTheory.ShrinkHoms.equivalence C).functor.obj X = CategoryTheory.ShrinkHoms.toShrinkHoms X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.LocallySmall.{w, v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.ShrinkHoms.equivalence C).functor.map f = (equivShrink (X ⟶ Y)) f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.LocallySmall.{w, v, u} C<VAR>X Y : CategoryTheory.ShrinkHoms.{u} C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.ShrinkHoms.equivalence C).inverse.map f = (equivShrink (X.fromShrinkHoms ⟶ Y.fromShrinkHoms)).symm f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.LocallySmall.{w, v, u} C<VAR>X : C<GOAL>(CategoryTheory.ShrinkHoms.equivalence C).unitIso.inv.app X = 𝟙 X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.EssentiallySmall.{w, v, u} C ↔ Small.{w, u} (CategoryTheory.Skeleton C) ∧ CategoryTheory.LocallySmall.{w, v, u} C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>Small.{w, u} C<VAR>CategoryTheory.LocallySmall.{w, v, u} C<GOAL>CategoryTheory.EssentiallySmall.{w, v, u} C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>Quiver.IsThin C<GOAL>CategoryTheory.EssentiallySmall.{w, v, u} C ↔ Small.{w, u} (CategoryTheory.Skeleton C)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>RF : CategoryTheory.Functor D H<VAR>F : CategoryTheory.Functor C H<VAR>L : CategoryTheory.Functor C D<VAR>α : F ⟶ L.comp RF<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>self : RF.IsRightDerivedFunctor α W<GOAL>RF.IsLeftKanExtension α
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_5<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Category.{u_6, u_5} H<VAR>RF : CategoryTheory.Functor D H<VAR>F : CategoryTheory.Functor C H<VAR>L : CategoryTheory.Functor C D<VAR>α : F ⟶ L.comp RF<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>RF.IsRightDerivedFunctor α W<GOAL>RF.IsLeftKanExtension α
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_5<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Category.{u_6, u_5} H<VAR>RF : CategoryTheory.Functor D H<VAR>F : CategoryTheory.Functor C H<VAR>L : CategoryTheory.Functor C D<VAR>α : F ⟶ L.comp RF<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<GOAL>RF.IsRightDerivedFunctor α W ↔ RF.IsLeftKanExtension α
<VAR>C : Type u_1<VAR>D : Type u_6<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_6} D<VAR>CategoryTheory.Category.{u_2, u_3} H<VAR>RF RF' : CategoryTheory.Functor D H<VAR>F : CategoryTheory.Functor C H<VAR>L : CategoryTheory.Functor C D<VAR>α : F ⟶ L.comp RF<VAR>α' : F ⟶ L.comp RF'<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>e : RF ≅ RF'<VAR>comm : CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L e.hom) = α'<GOAL>RF.IsRightDerivedFunctor α W ↔ RF'.IsRightDerivedFunctor α' W
<VAR>C : Type u_5<VAR>D : Type u_3<VAR>H : Type u_4<VAR>CategoryTheory.Category.{u_6, u_5} C<VAR>CategoryTheory.Category.{u_1, u_3} D<VAR>CategoryTheory.Category.{u_2, u_4} H<VAR>RF : CategoryTheory.Functor D H<VAR>F : CategoryTheory.Functor C H<VAR>L : CategoryTheory.Functor C D<VAR>α : F ⟶ L.comp RF<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>RF.IsRightDerivedFunctor α W<VAR>G : CategoryTheory.Functor D H<VAR>β : F ⟶ L.comp G<GOAL>CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L (RF.rightDerivedDesc α W G β)) = β
<VAR>C : Type u_5<VAR>D : Type u_3<VAR>H : Type u_4<VAR>CategoryTheory.Category.{u_6, u_5} C<VAR>CategoryTheory.Category.{u_1, u_3} D<VAR>CategoryTheory.Category.{u_2, u_4} H<VAR>RF : CategoryTheory.Functor D H<VAR>F : CategoryTheory.Functor C H<VAR>L : CategoryTheory.Functor C D<VAR>α : F ⟶ L.comp RF<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>RF.IsRightDerivedFunctor α W<VAR>G : CategoryTheory.Functor D H<VAR>β : F ⟶ L.comp G<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (α.app X) ((RF.rightDerivedDesc α W G β).app (L.obj X)) = β.app X
<VAR>C : Type u_5<VAR>D : Type u_3<VAR>H : Type u_4<VAR>CategoryTheory.Category.{u_6, u_5} C<VAR>CategoryTheory.Category.{u_1, u_3} D<VAR>CategoryTheory.Category.{u_2, u_4} H<VAR>RF : CategoryTheory.Functor D H<VAR>F : CategoryTheory.Functor C H<VAR>L : CategoryTheory.Functor C D<VAR>α : F ⟶ L.comp RF<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>RF.IsRightDerivedFunctor α W<VAR>G : CategoryTheory.Functor D H<VAR>γ₁ γ₂ : RF ⟶ G<VAR>hγ : CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L γ₁) = CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L γ₂)<GOAL>γ₁ = γ₂
<VAR>C : Type u_1<VAR>D : Type u_6<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_6} D<VAR>CategoryTheory.Category.{u_2, u_3} H<VAR>RF RF' : CategoryTheory.Functor D H<VAR>F F' : CategoryTheory.Functor C H<VAR>L : CategoryTheory.Functor C D<VAR>α : F ⟶ L.comp RF<VAR>α' : F' ⟶ L.comp RF'<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>RF.IsRightDerivedFunctor α W<VAR>τ : F ⟶ F'<GOAL>CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L (RF.rightDerivedNatTrans RF' α α' W τ)) = CategoryTheory.CategoryStruct.comp τ α'
<VAR>C : Type u_1<VAR>D : Type u_6<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_6} D<VAR>CategoryTheory.Category.{u_2, u_3} H<VAR>RF RF' : CategoryTheory.Functor D H<VAR>F F' : CategoryTheory.Functor C H<VAR>L : CategoryTheory.Functor C D<VAR>α : F ⟶ L.comp RF<VAR>α' : F' ⟶ L.comp RF'<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>RF.IsRightDerivedFunctor α W<VAR>τ : F ⟶ F'<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (α.app X) ((RF.rightDerivedNatTrans RF' α α' W τ).app (L.obj X)) = CategoryTheory.CategoryStruct.comp (τ.app X) (α'.app X)
<VAR>C : Type u_5<VAR>D : Type u_1<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_6, u_5} C<VAR>CategoryTheory.Category.{u_4, u_1} D<VAR>CategoryTheory.Category.{u_2, u_3} H<VAR>RF : CategoryTheory.Functor D H<VAR>F : CategoryTheory.Functor C H<VAR>L : CategoryTheory.Functor C D<VAR>α : F ⟶ L.comp RF<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>RF.IsRightDerivedFunctor α W<GOAL>RF.rightDerivedNatTrans RF α α W (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id RF
<VAR>C : Type u_1<VAR>D : Type u_5<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_6, u_5} D<VAR>CategoryTheory.Category.{u_2, u_3} H<VAR>RF RF' RF'' : CategoryTheory.Functor D H<VAR>F F' F'' : CategoryTheory.Functor C H<VAR>L : CategoryTheory.Functor C D<VAR>α : F ⟶ L.comp RF<VAR>α' : F' ⟶ L.comp RF'<VAR>α'' : F'' ⟶ L.comp RF''<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>RF.IsRightDerivedFunctor α W<VAR>RF'.IsRightDerivedFunctor α' W<VAR>τ : F ⟶ F'<VAR>τ' : F' ⟶ F''<GOAL>CategoryTheory.CategoryStruct.comp (RF.rightDerivedNatTrans RF' α α' W τ) (RF'.rightDerivedNatTrans RF'' α' α'' W τ') = RF.rightDerivedNatTrans RF'' α α'' W (CategoryTheory.CategoryStruct.comp τ τ')
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>RF RF' : CategoryTheory.Functor D H<VAR>F F' : CategoryTheory.Functor C H<VAR>L : CategoryTheory.Functor C D<VAR>α : F ⟶ L.comp RF<VAR>α' : F' ⟶ L.comp RF'<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>RF.IsRightDerivedFunctor α W<VAR>RF'.IsRightDerivedFunctor α' W<VAR>τ : F ≅ F'<GOAL>(RF.rightDerivedNatIso RF' α α' W τ).hom = RF.rightDerivedNatTrans RF' α α' W τ.hom
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>RF RF' : CategoryTheory.Functor D H<VAR>F F' : CategoryTheory.Functor C H<VAR>L : CategoryTheory.Functor C D<VAR>α : F ⟶ L.comp RF<VAR>α' : F' ⟶ L.comp RF'<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>RF.IsRightDerivedFunctor α W<VAR>RF'.IsRightDerivedFunctor α' W<VAR>τ : F ≅ F'<GOAL>(RF.rightDerivedNatIso RF' α α' W τ).inv = RF'.rightDerivedNatTrans RF α' α W τ.inv
<VAR>C : Type u_5<VAR>D : Type u_3<VAR>H : Type u_4<VAR>CategoryTheory.Category.{u_6, u_5} C<VAR>CategoryTheory.Category.{u_1, u_3} D<VAR>CategoryTheory.Category.{u_2, u_4} H<VAR>RF : CategoryTheory.Functor D H<VAR>F : CategoryTheory.Functor C H<VAR>L : CategoryTheory.Functor C D<VAR>α : F ⟶ L.comp RF<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>RF.IsRightDerivedFunctor α W<VAR>G : CategoryTheory.Functor D H<VAR>β : F ⟶ L.comp G<GOAL>G.IsRightDerivedFunctor β W ↔ CategoryTheory.IsIso (RF.rightDerivedDesc α W G β)
<VAR>C : Type u_1<VAR>H : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} H<VAR>F : CategoryTheory.Functor C H<VAR>W : CategoryTheory.MorphismProperty C<VAR>self : F.HasRightDerivedFunctor W<GOAL>W.Q.HasLeftKanExtension F
<VAR>C : Type u_1<VAR>D : Type u_5<VAR>H : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_6, u_5} D<VAR>CategoryTheory.Category.{u_4, u_2} H<VAR>F : CategoryTheory.Functor C H<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<GOAL>F.HasRightDerivedFunctor W ↔ L.HasLeftKanExtension F
<VAR>C : Type u_1<VAR>H : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} H<VAR>F F' : CategoryTheory.Functor C H<VAR>e : F ≅ F'<VAR>W : CategoryTheory.MorphismProperty C<GOAL>F.HasRightDerivedFunctor W ↔ F'.HasRightDerivedFunctor W
<VAR>C : Type u_1<VAR>D : Type u_5<VAR>H : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_6, u_5} D<VAR>CategoryTheory.Category.{u_4, u_2} H<VAR>F : CategoryTheory.Functor C H<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>F.HasRightDerivedFunctor W<GOAL>L.HasLeftKanExtension F
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} H<VAR>RF : CategoryTheory.Functor D H<VAR>F : CategoryTheory.Functor C H<VAR>L : CategoryTheory.Functor C D<VAR>α : F ⟶ L.comp RF<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>RF.IsRightDerivedFunctor α W<GOAL>F.HasRightDerivedFunctor W
<VAR>α : Type u_1<VAR>x : α<GOAL>AddOpposite.unop (AddOpposite.op x) = x
<VAR>α : Type u_1<VAR>x : α<GOAL>MulOpposite.unop (MulOpposite.op x) = x
<VAR>α : Type u_1<VAR>x : αᵐᵒᵖ<GOAL>MulOpposite.op (MulOpposite.unop x) = x
<VAR>α : Type u_1<VAR>x : αᵃᵒᵖ<GOAL>AddOpposite.op (AddOpposite.unop x) = x
<VAR>α : Type u_1<GOAL>MulOpposite.op ∘ MulOpposite.unop = id
<VAR>α : Type u_1<GOAL>AddOpposite.op ∘ AddOpposite.unop = id
<VAR>α : Type u_1<GOAL>AddOpposite.unop ∘ AddOpposite.op = id
<VAR>α : Type u_1<GOAL>MulOpposite.unop ∘ MulOpposite.op = id
<VAR>α : Type u_1<GOAL>⇑MulOpposite.opEquiv = MulOpposite.op
<VAR>α : Type u_1<GOAL>⇑AddOpposite.opEquiv = AddOpposite.op
<VAR>α : Type u_1<GOAL>⇑AddOpposite.opEquiv.symm = AddOpposite.unop
<VAR>α : Type u_1<GOAL>⇑MulOpposite.opEquiv.symm = MulOpposite.unop
<VAR>α : Type u_1<GOAL>Function.Bijective MulOpposite.op
<VAR>α : Type u_1<GOAL>Function.Bijective AddOpposite.op
<VAR>α : Type u_1<GOAL>Function.Bijective AddOpposite.unop
<VAR>α : Type u_1<GOAL>Function.Bijective MulOpposite.unop
<VAR>α : Type u_1<GOAL>Function.Injective MulOpposite.op
<VAR>α : Type u_1<GOAL>Function.Injective AddOpposite.op
<VAR>α : Type u_1<GOAL>Function.Surjective AddOpposite.op
<VAR>α : Type u_1<GOAL>Function.Surjective MulOpposite.op
<VAR>α : Type u_1<GOAL>Function.Injective AddOpposite.unop
<VAR>α : Type u_1<GOAL>Function.Injective MulOpposite.unop
<VAR>α : Type u_1<GOAL>Function.Surjective AddOpposite.unop
<VAR>α : Type u_1<GOAL>Function.Surjective MulOpposite.unop
<VAR>α : Type u_1<VAR>x y : α<GOAL>AddOpposite.op x = AddOpposite.op y ↔ x = y
<VAR>α : Type u_1<VAR>x y : α<GOAL>MulOpposite.op x = MulOpposite.op y ↔ x = y
<VAR>α : Type u_1<VAR>x y : αᵃᵒᵖ<GOAL>AddOpposite.unop x = AddOpposite.unop y ↔ x = y
<VAR>α : Type u_1<VAR>x y : αᵐᵒᵖ<GOAL>MulOpposite.unop x = MulOpposite.unop y ↔ x = y
<VAR>α : Type u_1<VAR>Zero α<GOAL>MulOpposite.op 0 = 0
<VAR>α : Type u_1<VAR>Zero α<GOAL>MulOpposite.unop 0 = 0
<VAR>α : Type u_1<VAR>Zero α<GOAL>AddOpposite.op 0 = 0
<VAR>α : Type u_1<VAR>One α<GOAL>MulOpposite.op 1 = 1
<VAR>α : Type u_1<VAR>Zero α<GOAL>AddOpposite.unop 0 = 0
<VAR>α : Type u_1<VAR>One α<GOAL>MulOpposite.unop 1 = 1
<VAR>α : Type u_1<VAR>Add α<VAR>x y : α<GOAL>MulOpposite.op (x + y) = MulOpposite.op x + MulOpposite.op y
<VAR>α : Type u_1<VAR>Add α<VAR>x y : αᵐᵒᵖ<GOAL>MulOpposite.unop (x + y) = MulOpposite.unop x + MulOpposite.unop y
<VAR>α : Type u_1<VAR>Neg α<VAR>x : α<GOAL>MulOpposite.op (-x) = -MulOpposite.op x
<VAR>α : Type u_1<VAR>Neg α<VAR>x : αᵐᵒᵖ<GOAL>MulOpposite.unop (-x) = -MulOpposite.unop x
<VAR>α : Type u_1<VAR>Add α<VAR>x y : α<GOAL>AddOpposite.op (x + y) = AddOpposite.op y + AddOpposite.op x
<VAR>α : Type u_1<VAR>Mul α<VAR>x y : α<GOAL>MulOpposite.op (x * y) = MulOpposite.op y * MulOpposite.op x
<VAR>α : Type u_1<VAR>Mul α<VAR>x y : αᵐᵒᵖ<GOAL>MulOpposite.unop (x * y) = MulOpposite.unop y * MulOpposite.unop x
<VAR>α : Type u_1<VAR>Add α<VAR>x y : αᵃᵒᵖ<GOAL>AddOpposite.unop (x + y) = AddOpposite.unop y + AddOpposite.unop x
<VAR>α : Type u_1<VAR>Neg α<VAR>x : α<GOAL>AddOpposite.op (-x) = -AddOpposite.op x
<VAR>α : Type u_1<VAR>Inv α<VAR>x : α<GOAL>MulOpposite.op x⁻¹ = (MulOpposite.op x)⁻¹
<VAR>α : Type u_1<VAR>Inv α<VAR>x : αᵐᵒᵖ<GOAL>MulOpposite.unop x⁻¹ = (MulOpposite.unop x)⁻¹
<VAR>α : Type u_1<VAR>Neg α<VAR>x : αᵃᵒᵖ<GOAL>AddOpposite.unop (-x) = -AddOpposite.unop x
<VAR>α : Type u_1<VAR>Sub α<VAR>x y : α<GOAL>MulOpposite.op (x - y) = MulOpposite.op x - MulOpposite.op y
<VAR>α : Type u_1<VAR>Sub α<VAR>x y : αᵐᵒᵖ<GOAL>MulOpposite.unop (x - y) = MulOpposite.unop x - MulOpposite.unop y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>a : α<VAR>b : β<GOAL>MulOpposite.op (a • b) = a • MulOpposite.op b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>VAdd α β<VAR>a : α<VAR>b : β<GOAL>AddOpposite.op (a +ᵥ b) = a +ᵥ AddOpposite.op b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>VAdd α β<VAR>a : α<VAR>b : βᵃᵒᵖ<GOAL>AddOpposite.unop (a +ᵥ b) = a +ᵥ AddOpposite.unop b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>a : α<VAR>b : βᵐᵒᵖ<GOAL>MulOpposite.unop (a • b) = a • MulOpposite.unop b
<VAR>α : Type u_1<VAR>Zero α<VAR>a : αᵐᵒᵖ<GOAL>MulOpposite.unop a = 0 ↔ a = 0
<VAR>α : Type u_1<VAR>Zero α<VAR>a : α<GOAL>MulOpposite.op a = 0 ↔ a = 0
<VAR>α : Type u_1<VAR>Zero α<VAR>a : αᵐᵒᵖ<GOAL>MulOpposite.unop a ≠ 0 ↔ a ≠ 0
<VAR>α : Type u_1<VAR>Zero α<VAR>a : α<GOAL>MulOpposite.op a ≠ 0 ↔ a ≠ 0
<VAR>α : Type u_1<VAR>Zero α<VAR>a : αᵃᵒᵖ<GOAL>AddOpposite.unop a = 0 ↔ a = 0
<VAR>α : Type u_1<VAR>One α<VAR>a : αᵐᵒᵖ<GOAL>MulOpposite.unop a = 1 ↔ a = 1
<VAR>α : Type u_1<VAR>Zero α<VAR>a : α<GOAL>AddOpposite.op a = 0 ↔ a = 0
<VAR>α : Type u_1<VAR>One α<VAR>a : α<GOAL>MulOpposite.op a = 1 ↔ a = 1
<VAR>α : Type u_1<VAR>One α<GOAL>AddOpposite.op 1 = 1
<VAR>α : Type u_1<VAR>One α<GOAL>AddOpposite.unop 1 = 1
<VAR>α : Type u_1<VAR>One α<VAR>a : α<GOAL>AddOpposite.op a = 1 ↔ a = 1
<VAR>α : Type u_1<VAR>One α<VAR>a : αᵃᵒᵖ<GOAL>AddOpposite.unop a = 1 ↔ a = 1
<VAR>α : Type u_1<VAR>Mul α<VAR>a b : α<GOAL>AddOpposite.op (a * b) = AddOpposite.op a * AddOpposite.op b