ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : Tᵒᵖ<GOAL>(CategoryTheory.Under.mapFunctor T).obj X = CategoryTheory.Cat.of (CategoryTheory.Under (Opposite.unop X))
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>f g : CategoryTheory.Under X<VAR>k : f ⟶ g<VAR>hk : CategoryTheory.Mono k.right<GOAL>CategoryTheory.Mono k
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>f g : CategoryTheory.Under X<VAR>k : f ⟶ g<VAR>hk : CategoryTheory.Epi k.right<GOAL>CategoryTheory.Epi k
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : T<VAR>F : CategoryTheory.Functor T D<VAR>Y : CategoryTheory.Under X<GOAL>(CategoryTheory.Under.post F).obj Y = CategoryTheory.Under.mk (F.map Y.hom)
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : T<VAR>F : CategoryTheory.Functor T D<GOAL>∀ {X_1 Y : CategoryTheory.Under X} (f : X_1 ⟶ Y), (CategoryTheory.Under.post F).map f = CategoryTheory.Under.homMk (F.map f.right) ⋯
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : T<VAR>F : CategoryTheory.Functor D T<GOAL>∀ (X_1 : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit X) (F.comp (CategoryTheory.Functor.id T))), ((CategoryTheory.StructuredArrow.toUnder X F).obj X_1).left = X_1.left
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : T<VAR>F : CategoryTheory.Functor D T<GOAL>∀ {X_1 Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit X) (F.comp (CategoryTheory.Functor.id T))} (f : X_1 ⟶ Y), ((CategoryTheory.StructuredArrow.toUnder X F).map f).right = F.map f.right
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : T<VAR>F : CategoryTheory.Functor D T<GOAL>∀ (X_1 : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit X) (F.comp (CategoryTheory.Functor.id T))), ((CategoryTheory.StructuredArrow.toUnder X F).obj X_1).right = F.obj X_1.right
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : T<VAR>F : CategoryTheory.Functor D T<GOAL>∀ (X_1 : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit X) (F.comp (CategoryTheory.Functor.id T))), ((CategoryTheory.StructuredArrow.toUnder X F).obj X_1).hom = X_1.hom
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : T<VAR>F : CategoryTheory.Functor D T<GOAL>∀ {X_1 Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit X) (F.comp (CategoryTheory.Functor.id T))} (f : X_1 ⟶ Y), ((CategoryTheory.StructuredArrow.toUnder X F).map f).left = CategoryTheory.CategoryStruct.id X_1.left
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>S : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} S<VAR>F : CategoryTheory.Functor S T<VAR>X : T<VAR>f : (Y : S) → F.obj Y ⟶ X<VAR>h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y<GOAL>∀ {X_1 Y : S} (g : X_1 ⟶ Y), ((F.toOver X f h).map g).left = F.map g
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>S : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} S<VAR>F : CategoryTheory.Functor S T<VAR>X : T<VAR>f : (Y : S) → F.obj Y ⟶ X<VAR>h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y<VAR>Y : S<GOAL>((F.toOver X f h).obj Y).left = F.obj Y
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>S : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} S<VAR>F : CategoryTheory.Functor S T<VAR>X : T<VAR>f : (Y : S) → F.obj Y ⟶ X<VAR>h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y<GOAL>(F.toOver X f ⋯).comp (CategoryTheory.Over.forget X) = F
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>S : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} S<VAR>F : CategoryTheory.Functor S T<VAR>X : T<VAR>f : (Y : S) → X ⟶ F.obj Y<VAR>h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z<GOAL>∀ {X_1 Y : S} (g : X_1 ⟶ Y), ((F.toUnder X f h).map g).right = F.map g
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>S : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} S<VAR>F : CategoryTheory.Functor S T<VAR>X : T<VAR>f : (Y : S) → X ⟶ F.obj Y<VAR>h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z<VAR>Y : S<GOAL>((F.toUnder X f h).obj Y).right = F.obj Y
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>S : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} S<VAR>F : CategoryTheory.Functor S T<VAR>X : T<VAR>f : (Y : S) → X ⟶ F.obj Y<VAR>h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z<GOAL>(F.toUnder X f ⋯).comp (CategoryTheory.Under.forget X) = F
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>F : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.Category.{v₄, u₄} F<VAR>G : CategoryTheory.Functor C E<VAR>H : CategoryTheory.Functor D F<VAR>L₁ : CategoryTheory.Functor C D<VAR>R₁ : CategoryTheory.Functor D C<VAR>L₂ : CategoryTheory.Functor E F<VAR>R₂ : CategoryTheory.Functor F E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : G.comp L₂ ⟶ L₁.comp H<GOAL>(CategoryTheory.mateEquiv adj₁ adj₂) α = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (R₁.comp G) adj₂.unit) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.whiskerLeft R₁ α) R₂) (CategoryTheory.whiskerRight adj₁.counit (H.comp R₂)))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>F : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.Category.{v₄, u₄} F<VAR>G : CategoryTheory.Functor C E<VAR>H : CategoryTheory.Functor D F<VAR>L₁ : CategoryTheory.Functor C D<VAR>R₁ : CategoryTheory.Functor D C<VAR>L₂ : CategoryTheory.Functor E F<VAR>R₂ : CategoryTheory.Functor F E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>β : R₁.comp G ⟶ H.comp R₂<GOAL>(CategoryTheory.mateEquiv adj₁ adj₂).symm β = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight adj₁.unit (G.comp L₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.whiskerLeft L₁ β) L₂) (CategoryTheory.whiskerLeft (L₁.comp H) adj₂.counit))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>F : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.Category.{v₄, u₄} F<VAR>G : CategoryTheory.Functor C E<VAR>H : CategoryTheory.Functor D F<VAR>L₁ : CategoryTheory.Functor C D<VAR>R₁ : CategoryTheory.Functor D C<VAR>L₂ : CategoryTheory.Functor E F<VAR>R₂ : CategoryTheory.Functor F E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : G.comp L₂ ⟶ L₁.comp H<VAR>d : D<GOAL>CategoryTheory.CategoryStruct.comp (L₂.map (((CategoryTheory.mateEquiv adj₁ adj₂) α).app d)) (adj₂.counit.app (H.obj d)) = CategoryTheory.CategoryStruct.comp (α.app (R₁.obj d)) (H.map (adj₁.counit.app d))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>F : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.Category.{v₄, u₄} F<VAR>G : CategoryTheory.Functor C E<VAR>H : CategoryTheory.Functor D F<VAR>L₁ : CategoryTheory.Functor C D<VAR>R₁ : CategoryTheory.Functor D C<VAR>L₂ : CategoryTheory.Functor E F<VAR>R₂ : CategoryTheory.Functor F E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : R₁.comp G ⟶ H.comp R₂<VAR>d : D<GOAL>CategoryTheory.CategoryStruct.comp (L₂.map (α.app d)) (adj₂.counit.app (H.obj d)) = CategoryTheory.CategoryStruct.comp (((CategoryTheory.mateEquiv adj₁ adj₂).symm α).app (R₁.obj d)) (H.map (adj₁.counit.app d))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>F : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.Category.{v₄, u₄} F<VAR>G : CategoryTheory.Functor C E<VAR>H : CategoryTheory.Functor D F<VAR>L₁ : CategoryTheory.Functor C D<VAR>R₁ : CategoryTheory.Functor D C<VAR>L₂ : CategoryTheory.Functor E F<VAR>R₂ : CategoryTheory.Functor F E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : G.comp L₂ ⟶ L₁.comp H<VAR>c : C<GOAL>CategoryTheory.CategoryStruct.comp (G.map (adj₁.unit.app c)) (((CategoryTheory.mateEquiv adj₁ adj₂) α).app (L₁.obj c)) = CategoryTheory.CategoryStruct.comp (adj₂.unit.app (G.obj ((CategoryTheory.Functor.id C).obj c))) (R₂.map (α.app ((CategoryTheory.Functor.id C).obj c)))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>F : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.Category.{v₄, u₄} F<VAR>G : CategoryTheory.Functor C E<VAR>H : CategoryTheory.Functor D F<VAR>L₁ : CategoryTheory.Functor C D<VAR>R₁ : CategoryTheory.Functor D C<VAR>L₂ : CategoryTheory.Functor E F<VAR>R₂ : CategoryTheory.Functor F E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : R₁.comp G ⟶ H.comp R₂<VAR>c : C<GOAL>CategoryTheory.CategoryStruct.comp (G.map (adj₁.unit.app c)) (α.app (L₁.obj c)) = CategoryTheory.CategoryStruct.comp (adj₂.unit.app (G.obj ((CategoryTheory.Functor.id C).obj c))) (R₂.map (((CategoryTheory.mateEquiv adj₁ adj₂).symm α).app ((CategoryTheory.Functor.id C).obj c)))
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>CategoryTheory.Category.{v₅, u₅} E<VAR>CategoryTheory.Category.{v₆, u₆} F<VAR>G₁ : CategoryTheory.Functor A C<VAR>G₂ : CategoryTheory.Functor C E<VAR>H₁ : CategoryTheory.Functor B D<VAR>H₂ : CategoryTheory.Functor D F<VAR>L₁ : CategoryTheory.Functor A B<VAR>R₁ : CategoryTheory.Functor B A<VAR>L₂ : CategoryTheory.Functor C D<VAR>R₂ : CategoryTheory.Functor D C<VAR>L₃ : CategoryTheory.Functor E F<VAR>R₃ : CategoryTheory.Functor F E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : G₁.comp L₂ ⟶ L₁.comp H₁<VAR>β : G₂.comp L₃ ⟶ L₂.comp H₂<GOAL>(CategoryTheory.mateEquiv adj₁ adj₃) (CategoryTheory.leftAdjointSquare.vcomp α β) = CategoryTheory.rightAdjointSquare.vcomp ((CategoryTheory.mateEquiv adj₁ adj₂) α) ((CategoryTheory.mateEquiv adj₂ adj₃) β)
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>CategoryTheory.Category.{v₅, u₅} E<VAR>CategoryTheory.Category.{v₆, u₆} F<VAR>G : CategoryTheory.Functor A D<VAR>H : CategoryTheory.Functor B E<VAR>K : CategoryTheory.Functor C F<VAR>L₁ : CategoryTheory.Functor A B<VAR>R₁ : CategoryTheory.Functor B A<VAR>L₂ : CategoryTheory.Functor D E<VAR>R₂ : CategoryTheory.Functor E D<VAR>L₃ : CategoryTheory.Functor B C<VAR>R₃ : CategoryTheory.Functor C B<VAR>L₄ : CategoryTheory.Functor E F<VAR>R₄ : CategoryTheory.Functor F E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>adj₄ : L₄ ⊣ R₄<VAR>α : G.comp L₂ ⟶ L₁.comp H<VAR>β : H.comp L₄ ⟶ L₃.comp K<GOAL>(CategoryTheory.mateEquiv (adj₁.comp adj₃) (adj₂.comp adj₄)) (CategoryTheory.leftAdjointSquare.hcomp α β) = CategoryTheory.rightAdjointSquare.hcomp ((CategoryTheory.mateEquiv adj₁ adj₂) α) ((CategoryTheory.mateEquiv adj₃ adj₄) β)
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>X : Type u₇<VAR>Y : Type u₈<VAR>Z : Type u₉<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>CategoryTheory.Category.{v₅, u₅} E<VAR>CategoryTheory.Category.{v₆, u₆} F<VAR>CategoryTheory.Category.{v₇, u₇} X<VAR>CategoryTheory.Category.{v₈, u₈} Y<VAR>CategoryTheory.Category.{v₉, u₉} Z<VAR>G₁ : CategoryTheory.Functor A D<VAR>H₁ : CategoryTheory.Functor B E<VAR>K₁ : CategoryTheory.Functor C F<VAR>G₂ : CategoryTheory.Functor D X<VAR>H₂ : CategoryTheory.Functor E Y<VAR>K₂ : CategoryTheory.Functor F Z<VAR>L₁ : CategoryTheory.Functor A B<VAR>L₂ : CategoryTheory.Functor B C<VAR>L₃ : CategoryTheory.Functor D E<VAR>L₄ : CategoryTheory.Functor E F<VAR>L₅ : CategoryTheory.Functor X Y<VAR>L₆ : CategoryTheory.Functor Y Z<VAR>α : G₁.comp L₃ ⟶ L₁.comp H₁<VAR>β : H₁.comp L₄ ⟶ L₂.comp K₁<VAR>γ : G₂.comp L₅ ⟶ L₃.comp H₂<VAR>δ : H₂.comp L₆ ⟶ L₄.comp K₂<GOAL>CategoryTheory.leftAdjointSquare.comp α β γ δ = CategoryTheory.leftAdjointSquare.vcomp (CategoryTheory.leftAdjointSquare.hcomp α β) (CategoryTheory.leftAdjointSquare.hcomp γ δ)
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>X : Type u₇<VAR>Y : Type u₈<VAR>Z : Type u₉<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>CategoryTheory.Category.{v₅, u₅} E<VAR>CategoryTheory.Category.{v₆, u₆} F<VAR>CategoryTheory.Category.{v₇, u₇} X<VAR>CategoryTheory.Category.{v₈, u₈} Y<VAR>CategoryTheory.Category.{v₉, u₉} Z<VAR>G₁ : CategoryTheory.Functor A D<VAR>H₁ : CategoryTheory.Functor B E<VAR>K₁ : CategoryTheory.Functor C F<VAR>G₂ : CategoryTheory.Functor D X<VAR>H₂ : CategoryTheory.Functor E Y<VAR>K₂ : CategoryTheory.Functor F Z<VAR>L₁ : CategoryTheory.Functor A B<VAR>L₂ : CategoryTheory.Functor B C<VAR>L₃ : CategoryTheory.Functor D E<VAR>L₄ : CategoryTheory.Functor E F<VAR>L₅ : CategoryTheory.Functor X Y<VAR>L₆ : CategoryTheory.Functor Y Z<VAR>α : G₁.comp L₃ ⟶ L₁.comp H₁<VAR>β : H₁.comp L₄ ⟶ L₂.comp K₁<VAR>γ : G₂.comp L₅ ⟶ L₃.comp H₂<VAR>δ : H₂.comp L₆ ⟶ L₄.comp K₂<GOAL>CategoryTheory.leftAdjointSquare.comp α β γ δ = CategoryTheory.leftAdjointSquare.hcomp (CategoryTheory.leftAdjointSquare.vcomp α γ) (CategoryTheory.leftAdjointSquare.vcomp β δ)
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>X : Type u₇<VAR>Y : Type u₈<VAR>Z : Type u₉<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>CategoryTheory.Category.{v₅, u₅} E<VAR>CategoryTheory.Category.{v₆, u₆} F<VAR>CategoryTheory.Category.{v₇, u₇} X<VAR>CategoryTheory.Category.{v₈, u₈} Y<VAR>CategoryTheory.Category.{v₉, u₉} Z<VAR>G₁ : CategoryTheory.Functor A D<VAR>H₁ : CategoryTheory.Functor B E<VAR>K₁ : CategoryTheory.Functor C F<VAR>G₂ : CategoryTheory.Functor D X<VAR>H₂ : CategoryTheory.Functor E Y<VAR>K₂ : CategoryTheory.Functor F Z<VAR>R₁ : CategoryTheory.Functor B A<VAR>R₂ : CategoryTheory.Functor C B<VAR>R₃ : CategoryTheory.Functor E D<VAR>R₄ : CategoryTheory.Functor F E<VAR>R₅ : CategoryTheory.Functor Y X<VAR>R₆ : CategoryTheory.Functor Z Y<VAR>α : R₁.comp G₁ ⟶ H₁.comp R₃<VAR>β : R₂.comp H₁ ⟶ K₁.comp R₄<VAR>γ : R₃.comp G₂ ⟶ H₂.comp R₅<VAR>δ : R₄.comp H₂ ⟶ K₂.comp R₆<GOAL>CategoryTheory.rightAdjointSquare.comp α β γ δ = CategoryTheory.rightAdjointSquare.vcomp (CategoryTheory.rightAdjointSquare.hcomp α β) (CategoryTheory.rightAdjointSquare.hcomp γ δ)
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>X : Type u₇<VAR>Y : Type u₈<VAR>Z : Type u₉<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>CategoryTheory.Category.{v₅, u₅} E<VAR>CategoryTheory.Category.{v₆, u₆} F<VAR>CategoryTheory.Category.{v₇, u₇} X<VAR>CategoryTheory.Category.{v₈, u₈} Y<VAR>CategoryTheory.Category.{v₉, u₉} Z<VAR>G₁ : CategoryTheory.Functor A D<VAR>H₁ : CategoryTheory.Functor B E<VAR>K₁ : CategoryTheory.Functor C F<VAR>G₂ : CategoryTheory.Functor D X<VAR>H₂ : CategoryTheory.Functor E Y<VAR>K₂ : CategoryTheory.Functor F Z<VAR>R₁ : CategoryTheory.Functor B A<VAR>R₂ : CategoryTheory.Functor C B<VAR>R₃ : CategoryTheory.Functor E D<VAR>R₄ : CategoryTheory.Functor F E<VAR>R₅ : CategoryTheory.Functor Y X<VAR>R₆ : CategoryTheory.Functor Z Y<VAR>α : R₁.comp G₁ ⟶ H₁.comp R₃<VAR>β : R₂.comp H₁ ⟶ K₁.comp R₄<VAR>γ : R₃.comp G₂ ⟶ H₂.comp R₅<VAR>δ : R₄.comp H₂ ⟶ K₂.comp R₆<GOAL>CategoryTheory.rightAdjointSquare.comp α β γ δ = CategoryTheory.rightAdjointSquare.hcomp (CategoryTheory.rightAdjointSquare.vcomp α γ) (CategoryTheory.rightAdjointSquare.vcomp β δ)
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>X : Type u₇<VAR>Y : Type u₈<VAR>Z : Type u₉<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>CategoryTheory.Category.{v₅, u₅} E<VAR>CategoryTheory.Category.{v₆, u₆} F<VAR>CategoryTheory.Category.{v₇, u₇} X<VAR>CategoryTheory.Category.{v₈, u₈} Y<VAR>CategoryTheory.Category.{v₉, u₉} Z<VAR>G₁ : CategoryTheory.Functor A D<VAR>H₁ : CategoryTheory.Functor B E<VAR>K₁ : CategoryTheory.Functor C F<VAR>G₂ : CategoryTheory.Functor D X<VAR>H₂ : CategoryTheory.Functor E Y<VAR>K₂ : CategoryTheory.Functor F Z<VAR>L₁ : CategoryTheory.Functor A B<VAR>R₁ : CategoryTheory.Functor B A<VAR>L₂ : CategoryTheory.Functor B C<VAR>R₂ : CategoryTheory.Functor C B<VAR>L₃ : CategoryTheory.Functor D E<VAR>R₃ : CategoryTheory.Functor E D<VAR>L₄ : CategoryTheory.Functor E F<VAR>R₄ : CategoryTheory.Functor F E<VAR>L₅ : CategoryTheory.Functor X Y<VAR>R₅ : CategoryTheory.Functor Y X<VAR>L₆ : CategoryTheory.Functor Y Z<VAR>R₆ : CategoryTheory.Functor Z Y<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>adj₄ : L₄ ⊣ R₄<VAR>adj₅ : L₅ ⊣ R₅<VAR>adj₆ : L₆ ⊣ R₆<VAR>α : G₁.comp L₃ ⟶ L₁.comp H₁<VAR>β : H₁.comp L₄ ⟶ L₂.comp K₁<VAR>γ : G₂.comp L₅ ⟶ L₃.comp H₂<VAR>δ : H₂.comp L₆ ⟶ L₄.comp K₂<GOAL>(CategoryTheory.mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) (CategoryTheory.leftAdjointSquare.comp α β γ δ) = CategoryTheory.rightAdjointSquare.comp ((CategoryTheory.mateEquiv adj₁ adj₃) α) ((CategoryTheory.mateEquiv adj₂ adj₄) β) ((CategoryTheory.mateEquiv adj₃ adj₅) γ) ((CategoryTheory.mateEquiv adj₄ adj₆) δ)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L₁ L₂ : CategoryTheory.Functor C D<VAR>R₁ R₂ : CategoryTheory.Functor D C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : L₂ ⟶ L₁<VAR>d : D<GOAL>CategoryTheory.CategoryStruct.comp (L₂.map (((CategoryTheory.conjugateEquiv adj₁ adj₂) α).app d)) (adj₂.counit.app d) = CategoryTheory.CategoryStruct.comp (α.app (R₁.obj d)) (adj₁.counit.app d)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L₁ L₂ : CategoryTheory.Functor C D<VAR>R₁ R₂ : CategoryTheory.Functor D C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : R₁ ⟶ R₂<VAR>d : D<GOAL>CategoryTheory.CategoryStruct.comp (L₂.map (α.app d)) (adj₂.counit.app d) = CategoryTheory.CategoryStruct.comp (((CategoryTheory.conjugateEquiv adj₁ adj₂).symm α).app (R₁.obj d)) (adj₁.counit.app d)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L₁ L₂ : CategoryTheory.Functor C D<VAR>R₁ R₂ : CategoryTheory.Functor D C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : L₂ ⟶ L₁<VAR>c : C<GOAL>CategoryTheory.CategoryStruct.comp (adj₁.unit.app c) (((CategoryTheory.conjugateEquiv adj₁ adj₂) α).app (L₁.obj c)) = CategoryTheory.CategoryStruct.comp (adj₂.unit.app c) (R₂.map (α.app c))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L₁ L₂ : CategoryTheory.Functor C D<VAR>R₁ R₂ : CategoryTheory.Functor D C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : R₁ ⟶ R₂<VAR>c : C<GOAL>CategoryTheory.CategoryStruct.comp (adj₁.unit.app c) (α.app (L₁.obj c)) = CategoryTheory.CategoryStruct.comp (adj₂.unit.app c) (R₂.map (((CategoryTheory.conjugateEquiv adj₁ adj₂).symm α).app c))
<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>R₁ : CategoryTheory.Functor D C<VAR>adj₁ : L₁ ⊣ R₁<GOAL>(CategoryTheory.conjugateEquiv adj₁ adj₁) (CategoryTheory.CategoryStruct.id L₁) = CategoryTheory.CategoryStruct.id R₁
<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>R₁ : CategoryTheory.Functor D C<VAR>adj₁ : L₁ ⊣ R₁<GOAL>(CategoryTheory.conjugateEquiv adj₁ adj₁).symm (CategoryTheory.CategoryStruct.id R₁) = CategoryTheory.CategoryStruct.id L₁
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>L R : CategoryTheory.Functor C C<VAR>adj : L ⊣ R<VAR>α : CategoryTheory.Functor.id C ⟶ L<VAR>c : C<GOAL>((CategoryTheory.conjugateEquiv adj CategoryTheory.Adjunction.id) α).app c = CategoryTheory.CategoryStruct.comp (α.app (R.obj c)) (adj.counit.app c)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>L R : CategoryTheory.Functor C C<VAR>adj : L ⊣ R<VAR>α : R ⟶ CategoryTheory.Functor.id C<VAR>c : C<GOAL>((CategoryTheory.conjugateEquiv adj CategoryTheory.Adjunction.id).symm α).app c = CategoryTheory.CategoryStruct.comp (adj.unit.app c) (α.app (L.obj c))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L₁ L₂ L₃ : CategoryTheory.Functor C D<VAR>R₁ R₂ R₃ : CategoryTheory.Functor D C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : L₂ ⟶ L₁<VAR>β : L₃ ⟶ L₂<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.conjugateEquiv adj₁ adj₂) α) ((CategoryTheory.conjugateEquiv adj₂ adj₃) β) = (CategoryTheory.conjugateEquiv adj₁ adj₃) (CategoryTheory.CategoryStruct.comp β α)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L₁ L₂ L₃ : CategoryTheory.Functor C D<VAR>R₁ R₂ R₃ : CategoryTheory.Functor D C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : R₁ ⟶ R₂<VAR>β : R₂ ⟶ R₃<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.conjugateEquiv adj₂ adj₃).symm β) ((CategoryTheory.conjugateEquiv adj₁ adj₂).symm α) = (CategoryTheory.conjugateEquiv adj₁ adj₃).symm (CategoryTheory.CategoryStruct.comp α β)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L₁ L₂ : CategoryTheory.Functor C D<VAR>R₁ R₂ : CategoryTheory.Functor D C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : L₂ ⟶ L₁<VAR>β : L₁ ⟶ L₂<VAR>βα : CategoryTheory.CategoryStruct.comp β α = CategoryTheory.CategoryStruct.id L₁<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.conjugateEquiv adj₁ adj₂) α) ((CategoryTheory.conjugateEquiv adj₂ adj₁) β) = CategoryTheory.CategoryStruct.id R₁
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L₁ L₂ : CategoryTheory.Functor C D<VAR>R₁ R₂ : CategoryTheory.Functor D C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : R₁ ⟶ R₂<VAR>β : R₂ ⟶ R₁<VAR>αβ : CategoryTheory.CategoryStruct.comp α β = CategoryTheory.CategoryStruct.id R₁<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.conjugateEquiv adj₂ adj₁).symm β) ((CategoryTheory.conjugateEquiv adj₁ adj₂).symm α) = CategoryTheory.CategoryStruct.id L₁
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L₁ L₂ : CategoryTheory.Functor C D<VAR>R₁ R₂ : CategoryTheory.Functor D C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : L₂ ⟶ L₁<VAR>CategoryTheory.IsIso ((CategoryTheory.conjugateEquiv adj₁ adj₂) α)<GOAL>CategoryTheory.IsIso α
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L₁ L₂ : CategoryTheory.Functor C D<VAR>R₁ R₂ : CategoryTheory.Functor D C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : R₁ ⟶ R₂<VAR>CategoryTheory.IsIso ((CategoryTheory.conjugateEquiv adj₁ adj₂).symm α)<GOAL>CategoryTheory.IsIso α