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₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>e : C ≌ D<VAR>F : CategoryTheory.Functor C E<VAR>X : C<GOAL>(e.funInvIdAssoc F).inv.app X = F.map (e.unit.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>e : C ≌ D<VAR>F : CategoryTheory.Functor D E<VAR>X : D<GOAL>(e.invFunIdAssoc F).hom.app X = F.map (e.counit.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>e : C ≌ D<VAR>F : CategoryTheory.Functor D E<VAR>X : D<GOAL>(e.invFunIdAssoc F).inv.app X = F.map (e.counitInv.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>e : C ≌ D<GOAL>e.congrLeft.functor = (CategoryTheory.whiskeringLeft D C E).obj e.inverse
<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>e : C ≌ D<GOAL>e.congrLeft.unitIso = CategoryTheory.Equivalence.adjointifyη (CategoryTheory.NatIso.ofComponents (fun F => (e.funInvIdAssoc F).symm) ⋯) (CategoryTheory.NatIso.ofComponents (fun F => e.invFunIdAssoc 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>e : C ≌ D<GOAL>e.congrLeft.counitIso = CategoryTheory.NatIso.ofComponents (fun F => e.invFunIdAssoc 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>e : C ≌ D<GOAL>e.congrLeft.inverse = (CategoryTheory.whiskeringLeft C D E).obj e.functor
<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>e : C ≌ D<GOAL>e.congrRight.counitIso = CategoryTheory.NatIso.ofComponents (fun F => F.associator e.inverse e.functor ≪≫ CategoryTheory.isoWhiskerLeft F e.counitIso ≪≫ F.rightUnitor) ⋯
<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>e : C ≌ D<GOAL>e.congrRight.unitIso = CategoryTheory.Equivalence.adjointifyη (CategoryTheory.NatIso.ofComponents (fun F => F.rightUnitor.symm ≪≫ CategoryTheory.isoWhiskerLeft F e.unitIso ≪≫ F.associator e.functor e.inverse) ⋯) (CategoryTheory.NatIso.ofComponents (fun F => F.associator e.inverse e.functor ≪≫ CategoryTheory.isoWhiskerLeft F e.counitIso ≪≫ F.rightUnitor) ⋯)
<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>e : C ≌ D<GOAL>e.congrRight.inverse = (CategoryTheory.whiskeringRight E D C).obj e.inverse
<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>e : C ≌ D<GOAL>e.congrRight.functor = (CategoryTheory.whiskeringRight E C D).obj e.functor
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X Y : C<VAR>f f' : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp f (e.unit.app Y) = CategoryTheory.CategoryStruct.comp f' (e.unit.app Y) ↔ f = f'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X Y : C<VAR>f f' : X ⟶ e.inverse.obj (e.functor.obj Y)<GOAL>CategoryTheory.CategoryStruct.comp f (e.unitInv.app Y) = CategoryTheory.CategoryStruct.comp f' (e.unitInv.app Y) ↔ f = f'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X Y : D<VAR>f f' : X ⟶ e.functor.obj (e.inverse.obj Y)<GOAL>CategoryTheory.CategoryStruct.comp f (e.counit.app Y) = CategoryTheory.CategoryStruct.comp f' (e.counit.app Y) ↔ f = f'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X Y : D<VAR>f f' : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp f (e.counitInv.app Y) = CategoryTheory.CategoryStruct.comp f' (e.counitInv.app Y) ↔ f = f'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>W X X' Y : C<VAR>f : W ⟶ X<VAR>g : X ⟶ Y<VAR>f' : W ⟶ X'<VAR>g' : X' ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (e.unit.app Y)) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (e.unit.app Y)) ↔ CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>W X X' Y : D<VAR>f : W ⟶ X<VAR>g : X ⟶ Y<VAR>f' : W ⟶ X'<VAR>g' : X' ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (e.counitInv.app Y)) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (e.counitInv.app Y)) ↔ CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>W X X' Y Y' Z : C<VAR>f : W ⟶ X<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<VAR>f' : W ⟶ X'<VAR>g' : X' ⟶ Y'<VAR>h' : Y' ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp h (e.unit.app Z))) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (CategoryTheory.CategoryStruct.comp h' (e.unit.app Z))) ↔ CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h')
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>W X X' Y Y' Z : D<VAR>f : W ⟶ X<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<VAR>f' : W ⟶ X'<VAR>g' : X' ⟶ Y'<VAR>h' : Y' ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp h (e.counitInv.app Z))) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (CategoryTheory.CategoryStruct.comp h' (e.counitInv.app Z))) ↔ CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h')
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>e : C ≌ C<GOAL>e ^ 0 = CategoryTheory.Equivalence.refl
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>e : C ≌ C<GOAL>e ^ 1 = e
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>e : C ≌ C<GOAL>e ^ (-1) = e.symm
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>G : CategoryTheory.Functor C D<VAR>iso : e.functor ≅ G<VAR>X : C<GOAL>(e.changeFunctor iso).unitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app X) (e.inverse.map (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 : C ≌ D<VAR>G : CategoryTheory.Functor C D<VAR>iso : e.functor ≅ G<VAR>X : C<GOAL>(e.changeFunctor iso).unitIso.inv.app X = CategoryTheory.CategoryStruct.comp (e.inverse.map (iso.inv.app X)) (e.unitIso.inv.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>G : CategoryTheory.Functor C D<VAR>iso : e.functor ≅ G<GOAL>(e.changeFunctor iso).inverse = e.inverse
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>G : CategoryTheory.Functor C D<VAR>iso : e.functor ≅ G<VAR>X : D<GOAL>(e.changeFunctor iso).counitIso.inv.app X = CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app X) (iso.hom.app (e.inverse.obj X))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>G : CategoryTheory.Functor C D<VAR>iso : e.functor ≅ G<VAR>X : D<GOAL>(e.changeFunctor iso).counitIso.hom.app X = CategoryTheory.CategoryStruct.comp (iso.inv.app (e.inverse.obj X)) (e.counitIso.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 : C ≌ D<VAR>G : CategoryTheory.Functor C D<VAR>iso : e.functor ≅ G<GOAL>(e.changeFunctor iso).functor = G
<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>e.changeFunctor (CategoryTheory.Iso.refl e.functor) = e
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>G G' : CategoryTheory.Functor C D<VAR>iso₁ : e.functor ≅ G<VAR>iso₂ : G ≅ G'<GOAL>(e.changeFunctor iso₁).changeFunctor iso₂ = e.changeFunctor (iso₁ ≪≫ iso₂)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>G : CategoryTheory.Functor D C<VAR>iso : e.inverse ≅ G<GOAL>(e.changeInverse iso).functor = e.functor
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>G : CategoryTheory.Functor D C<VAR>iso : e.inverse ≅ G<VAR>X : C<GOAL>(e.changeInverse iso).unitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app X) (iso.hom.app (e.functor.obj X))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>G : CategoryTheory.Functor D C<VAR>iso : e.inverse ≅ G<VAR>X : C<GOAL>(e.changeInverse iso).unitIso.inv.app X = CategoryTheory.CategoryStruct.comp (iso.inv.app (e.functor.obj X)) (e.unitIso.inv.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>G : CategoryTheory.Functor D C<VAR>iso : e.inverse ≅ G<VAR>X : D<GOAL>(e.changeInverse iso).counitIso.inv.app X = CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app X) (e.functor.map (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 : C ≌ D<VAR>G : CategoryTheory.Functor D C<VAR>iso : e.inverse ≅ G<VAR>X : D<GOAL>(e.changeInverse iso).counitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.functor.map (iso.inv.app X)) (e.counitIso.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 : C ≌ D<VAR>G : CategoryTheory.Functor D C<VAR>iso : e.inverse ≅ G<GOAL>(e.changeInverse iso).inverse = G
<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>self : F.IsEquivalence<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 : CategoryTheory.Functor C D<VAR>self : F.IsEquivalence<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 : CategoryTheory.Functor C D<VAR>self : F.IsEquivalence<GOAL>F.EssSurj
<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>G : CategoryTheory.Functor D C<VAR>η : CategoryTheory.Functor.id C ≅ F.comp G<VAR>ε : G.comp F ≅ CategoryTheory.Functor.id D<GOAL>F.IsEquivalence
<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.IsEquivalence<GOAL>F.asEquivalence.functor = 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.IsEquivalence<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>F.map (F.inv.map f) = CategoryTheory.CategoryStruct.comp (F.asEquivalence.counit.app X) (CategoryTheory.CategoryStruct.comp f (F.asEquivalence.counitInv.app Y))
<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.IsEquivalence<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>F.inv.map (F.map f) = CategoryTheory.CategoryStruct.comp (F.asEquivalence.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (F.asEquivalence.unit.app Y))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor C D<VAR>e : F ≅ G<VAR>F.IsEquivalence<GOAL>G.IsEquivalence
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor C D<VAR>e : F ≅ G<GOAL>F.IsEquivalence ↔ G.IsEquivalence
<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>G : CategoryTheory.Functor D E<VAR>G.IsEquivalence<VAR>(F.comp G).IsEquivalence<GOAL>F.IsEquivalence
<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>G : CategoryTheory.Functor D E<VAR>F.IsEquivalence<VAR>(F.comp G).IsEquivalence<GOAL>G.IsEquivalence
<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>G : CategoryTheory.Functor C D<VAR>H : D ≌ E<VAR>i : F ≅ G.comp H.functor<VAR>X : C<GOAL>i.compInverseIso.inv.app X = CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.obj X)) (H.inverse.map (i.inv.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 : CategoryTheory.Functor C E<VAR>G : CategoryTheory.Functor C D<VAR>H : D ≌ E<VAR>i : F ≅ G.comp H.functor<VAR>X : C<GOAL>i.compInverseIso.hom.app X = CategoryTheory.CategoryStruct.comp (H.inverse.map (i.hom.app X)) (H.unitIso.inv.app (G.obj 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 : CategoryTheory.Functor C E<VAR>G : CategoryTheory.Functor C D<VAR>H : D ≌ E<VAR>i : G.comp H.functor ≅ F<VAR>X : C<GOAL>i.isoCompInverse.hom.app X = CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.obj X)) (H.inverse.map (i.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 : CategoryTheory.Functor C E<VAR>G : CategoryTheory.Functor C D<VAR>H : D ≌ E<VAR>i : G.comp H.functor ≅ F<VAR>X : C<GOAL>i.isoCompInverse.inv.app X = CategoryTheory.CategoryStruct.comp (H.inverse.map (i.inv.app X)) (H.unitIso.inv.app (G.obj 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 : CategoryTheory.Functor C E<VAR>H : CategoryTheory.Functor D E<VAR>G : C ≌ D<VAR>i : F ≅ G.functor.comp H<VAR>X : D<GOAL>i.inverseCompIso.inv.app X = CategoryTheory.CategoryStruct.comp (H.map (G.counitIso.inv.app X)) (i.inv.app (G.inverse.obj 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 : CategoryTheory.Functor C E<VAR>H : CategoryTheory.Functor D E<VAR>G : C ≌ D<VAR>i : F ≅ G.functor.comp H<VAR>X : D<GOAL>i.inverseCompIso.hom.app X = CategoryTheory.CategoryStruct.comp (i.hom.app (G.inverse.obj X)) (H.map (G.counitIso.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 : CategoryTheory.Functor C E<VAR>H : CategoryTheory.Functor D E<VAR>G : C ≌ D<VAR>i : G.functor.comp H ≅ F<VAR>X : D<GOAL>i.isoInverseComp.hom.app X = CategoryTheory.CategoryStruct.comp (H.map (G.counitIso.inv.app X)) (i.hom.app (G.inverse.obj 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 : CategoryTheory.Functor C E<VAR>H : CategoryTheory.Functor D E<VAR>G : C ≌ D<VAR>i : G.functor.comp H ≅ F<VAR>X : D<GOAL>i.isoInverseComp.inv.app X = CategoryTheory.CategoryStruct.comp (i.inv.app (G.inverse.obj X)) (H.map (G.counitIso.hom.app X))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Precoherent C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>(∃ α, ∃ (_ : Finite α), ∃ Y π, CategoryTheory.EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) → S ∈ (CategoryTheory.coherentTopology C).sieves X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Precoherent C<VAR>X : C<VAR>α : Type<VAR>Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>h : CategoryTheory.EffectiveEpiFamily Y π<VAR>β : α → Type<VAR>∀ (a : α), Finite (β a)<VAR>Y_n : (a : α) → β a → C<VAR>π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a<VAR>H : ∀ (a : α), CategoryTheory.EffectiveEpiFamily (Y_n a) (π_n a)<GOAL>CategoryTheory.EffectiveEpiFamily (fun c => Y_n c.fst c.snd) fun c => CategoryTheory.CategoryStruct.comp (π_n c.fst c.snd) (π c.fst)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Precoherent C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>S ∈ (CategoryTheory.coherentTopology C).sieves X ↔ ∃ α, ∃ (_ : Finite α), ∃ Y π, CategoryTheory.EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesEffectiveEpis<VAR>F.ReflectsEffectiveEpis<VAR>F.EffectivelyEnough<VAR>CategoryTheory.Preregular D<VAR>F.Full<VAR>F.Faithful<GOAL>CategoryTheory.Preregular C
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_4} D₁<VAR>CategoryTheory.Category.{u_10, u_5} D₂<VAR>T : CategoryTheory.Functor C₁ D₁<VAR>L : CategoryTheory.Functor C₁ C₂<VAR>R : CategoryTheory.Functor D₁ D₂<VAR>B : CategoryTheory.Functor C₂ D₂<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>L' : CategoryTheory.Functor C₁ C₂<VAR>R' : CategoryTheory.Functor D₁ D₂<VAR>α : L ⟶ L'<VAR>β : R' ⟶ R<VAR>X : C₁<GOAL>(w.whiskerVertical α β).app X = CategoryTheory.CategoryStruct.comp (β.app (T.obj X)) (CategoryTheory.CategoryStruct.comp (w.app X) (B.map (α.app X)))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_9, u_2} C₂<VAR>CategoryTheory.Category.{u_8, u_4} D₁<VAR>CategoryTheory.Category.{u_10, u_5} D₂<VAR>T : CategoryTheory.Functor C₁ D₁<VAR>L : CategoryTheory.Functor C₁ C₂<VAR>R : CategoryTheory.Functor D₁ D₂<VAR>B : CategoryTheory.Functor C₂ D₂<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>L' : CategoryTheory.Functor C₁ C₂<VAR>R' : CategoryTheory.Functor D₁ D₂<VAR>w.GuitartExact<VAR>α : L ≅ L'<VAR>β : R ≅ R'<GOAL>(w.whiskerVertical α.hom β.inv).GuitartExact
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>CategoryTheory.Category.{u_8, u_1} C₁<VAR>CategoryTheory.Category.{u_7, u_2} C₂<VAR>CategoryTheory.Category.{u_10, u_4} D₁<VAR>CategoryTheory.Category.{u_9, u_5} D₂<VAR>T : CategoryTheory.Functor C₁ D₁<VAR>L : CategoryTheory.Functor C₁ C₂<VAR>R : CategoryTheory.Functor D₁ D₂<VAR>B : CategoryTheory.Functor C₂ D₂<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>L' : CategoryTheory.Functor C₁ C₂<VAR>R' : CategoryTheory.Functor D₁ D₂<VAR>α : L ≅ L'<VAR>β : R ≅ R'<GOAL>(w.whiskerVertical α.hom β.inv).GuitartExact ↔ w.GuitartExact
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>D₃ : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} D₁<VAR>CategoryTheory.Category.{u_11, u_5} D₂<VAR>CategoryTheory.Category.{u_12, u_6} D₃<VAR>H₁ : CategoryTheory.Functor C₁ D₁<VAR>L₁ : CategoryTheory.Functor C₁ C₂<VAR>R₁ : CategoryTheory.Functor D₁ D₂<VAR>H₂ : CategoryTheory.Functor C₂ D₂<VAR>w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂<VAR>L₂ : CategoryTheory.Functor C₂ C₃<VAR>R₂ : CategoryTheory.Functor D₂ D₃<VAR>H₃ : CategoryTheory.Functor C₃ D₃<VAR>w' : CategoryTheory.TwoSquare H₂ L₂ R₂ H₃<VAR>X : C₁<GOAL>(w.vComp w').app X = CategoryTheory.CategoryStruct.comp (R₂.map (w.app X)) (w'.app (L₁.obj X))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>D₃ : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} D₁<VAR>CategoryTheory.Category.{u_11, u_5} D₂<VAR>CategoryTheory.Category.{u_12, u_6} D₃<VAR>H₁ : CategoryTheory.Functor C₁ D₁<VAR>L₁ : CategoryTheory.Functor C₁ C₂<VAR>R₁ : CategoryTheory.Functor D₁ D₂<VAR>H₂ : CategoryTheory.Functor C₂ D₂<VAR>w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂<VAR>L₂ : CategoryTheory.Functor C₂ C₃<VAR>R₂ : CategoryTheory.Functor D₂ D₃<VAR>H₃ : CategoryTheory.Functor C₃ D₃<VAR>w' : CategoryTheory.TwoSquare H₂ L₂ R₂ H₃<VAR>L₁₂ : CategoryTheory.Functor C₁ C₃<VAR>R₁₂ : CategoryTheory.Functor D₁ D₃<VAR>eL : L₁.comp L₂ ≅ L₁₂<VAR>eR : R₁.comp R₂ ≅ R₁₂<VAR>X : C₁<GOAL>(w.vComp' w' eL eR).app X = CategoryTheory.CategoryStruct.comp (eR.inv.app (H₁.obj X)) (CategoryTheory.CategoryStruct.comp (R₂.map (w.app X)) (CategoryTheory.CategoryStruct.comp (w'.app (L₁.obj X)) (H₃.map (eL.hom.app X))))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>D₃ : Type u_6<VAR>CategoryTheory.Category.{u_11, u_1} C₁<VAR>CategoryTheory.Category.{u_7, u_2} C₂<VAR>CategoryTheory.Category.{u_8, u_3} C₃<VAR>CategoryTheory.Category.{u_12, u_4} D₁<VAR>CategoryTheory.Category.{u_9, u_5} D₂<VAR>CategoryTheory.Category.{u_10, u_6} D₃<VAR>H₁ : CategoryTheory.Functor C₁ D₁<VAR>L₁ : CategoryTheory.Functor C₁ C₂<VAR>R₁ : CategoryTheory.Functor D₁ D₂<VAR>H₂ : CategoryTheory.Functor C₂ D₂<VAR>w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂<VAR>H₃ : CategoryTheory.Functor C₃ D₃<VAR>eL : C₂ ≌ C₃<VAR>eR : D₂ ≌ D₃<VAR>w' : H₂.comp eR.functor ≅ eL.functor.comp H₃<GOAL>(w.vComp w'.hom).GuitartExact ↔ w.GuitartExact
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>D₃ : Type u_6<VAR>CategoryTheory.Category.{u_11, u_1} C₁<VAR>CategoryTheory.Category.{u_7, u_2} C₂<VAR>CategoryTheory.Category.{u_8, u_3} C₃<VAR>CategoryTheory.Category.{u_12, u_4} D₁<VAR>CategoryTheory.Category.{u_9, u_5} D₂<VAR>CategoryTheory.Category.{u_10, u_6} D₃<VAR>H₁ : CategoryTheory.Functor C₁ D₁<VAR>L₁ : CategoryTheory.Functor C₁ C₂<VAR>R₁ : CategoryTheory.Functor D₁ D₂<VAR>H₂ : CategoryTheory.Functor C₂ D₂<VAR>w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂<VAR>H₃ : CategoryTheory.Functor C₃ D₃<VAR>E : C₂ ≌ C₃<VAR>E' : D₂ ≌ D₃<VAR>w' : H₂.comp E'.functor ≅ E.functor.comp H₃<VAR>L₁₂ : CategoryTheory.Functor C₁ C₃<VAR>R₁₂ : CategoryTheory.Functor D₁ D₃<VAR>eL : L₁.comp E.functor ≅ L₁₂<VAR>eR : R₁.comp E'.functor ≅ R₁₂<GOAL>(w.vComp' w'.hom eL eR).GuitartExact ↔ w.GuitartExact