ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.Center.ofBraided C).map f).f = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : C<GOAL>(CategoryTheory.Center.ofBraided C).obj X = CategoryTheory.Center.ofBraidedObj X
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : L.comp F' ⟶ F<GOAL>(CategoryTheory.Functor.RightExtension.mk F' α).hom = α
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : L.comp F' ⟶ F<GOAL>(CategoryTheory.Functor.RightExtension.mk F' α).right.as = PUnit.unit
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : L.comp F' ⟶ F<GOAL>(CategoryTheory.Functor.RightExtension.mk F' α).left = F'
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : F ⟶ L.comp F'<GOAL>(CategoryTheory.Functor.LeftExtension.mk F' α).left.as = PUnit.unit
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : F ⟶ L.comp F'<GOAL>(CategoryTheory.Functor.LeftExtension.mk F' α).right = F'
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : F ⟶ L.comp F'<GOAL>(CategoryTheory.Functor.LeftExtension.mk F' α).hom = α
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : L.comp F' ⟶ F<VAR>self : F'.IsRightKanExtension α<GOAL>Nonempty (CategoryTheory.CostructuredArrow.IsUniversal (CategoryTheory.Functor.RightExtension.mk F' α))
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_7, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : L.comp F' ⟶ F<VAR>F'.IsRightKanExtension α<VAR>G : CategoryTheory.Functor D H<VAR>β : L.comp G ⟶ F<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L (F'.liftOfIsRightKanExtension α G β)) α = β
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_7, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : L.comp F' ⟶ F<VAR>F'.IsRightKanExtension α<VAR>G : CategoryTheory.Functor D H<VAR>β : L.comp G ⟶ F<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((F'.liftOfIsRightKanExtension α G β).app (L.obj X)) (α.app X) = β.app X
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_7, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : L.comp F' ⟶ F<VAR>F'.IsRightKanExtension α<VAR>G : CategoryTheory.Functor D H<VAR>γ₁ γ₂ : G ⟶ F'<VAR>hγ : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L γ₁) α = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L γ₂) α<GOAL>γ₁ = γ₂
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_7, u_5} D<VAR>F' F'' : CategoryTheory.Functor D H<VAR>e : F' ≅ F''<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : L.comp F' ⟶ F<VAR>α' : L.comp F'' ⟶ F<VAR>comm : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L e.hom) α' = α<VAR>F'.IsRightKanExtension α<GOAL>F''.IsRightKanExtension α'
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_7, u_5} D<VAR>F' F'' : CategoryTheory.Functor D H<VAR>e : F' ≅ F''<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : L.comp F' ⟶ F<VAR>α' : L.comp F'' ⟶ F<VAR>comm : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L e.hom) α' = α<GOAL>F'.IsRightKanExtension α ↔ F''.IsRightKanExtension α'
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : L.comp F' ⟶ F<VAR>F'.IsRightKanExtension α<VAR>G : CategoryTheory.Functor C H<VAR>i : F ≅ G<VAR>G' : CategoryTheory.Functor D H<VAR>β : L.comp G' ⟶ G<VAR>G'.IsRightKanExtension β<GOAL>(F'.rightKanExtensionUniqueOfIso α i G' β).inv = F'.liftOfIsRightKanExtension α G' (CategoryTheory.CategoryStruct.comp β i.inv)
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : L.comp F' ⟶ F<VAR>F'.IsRightKanExtension α<VAR>G : CategoryTheory.Functor C H<VAR>i : F ≅ G<VAR>G' : CategoryTheory.Functor D H<VAR>β : L.comp G' ⟶ G<VAR>G'.IsRightKanExtension β<GOAL>(F'.rightKanExtensionUniqueOfIso α i G' β).hom = G'.liftOfIsRightKanExtension β F' (CategoryTheory.CategoryStruct.comp α i.hom)
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : L.comp F' ⟶ F<VAR>F'.IsRightKanExtension α<VAR>F'' : CategoryTheory.Functor D H<VAR>α' : L.comp F'' ⟶ F<VAR>F''.IsRightKanExtension α'<GOAL>(F'.rightKanExtensionUnique α F'' α').hom = F''.liftOfIsRightKanExtension α' F' α
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : L.comp F' ⟶ F<VAR>F'.IsRightKanExtension α<VAR>F'' : CategoryTheory.Functor D H<VAR>α' : L.comp F'' ⟶ F<VAR>F''.IsRightKanExtension α'<GOAL>(F'.rightKanExtensionUnique α F'' α').inv = F'.liftOfIsRightKanExtension α F'' α'
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_7, u_5} D<VAR>F' F'' : CategoryTheory.Functor D H<VAR>φ : F'' ⟶ F'<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : L.comp F' ⟶ F<VAR>α' : L.comp F'' ⟶ F<VAR>comm : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L φ) α = α'<VAR>F'.IsRightKanExtension α<GOAL>F''.IsRightKanExtension α' ↔ CategoryTheory.IsIso φ
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : F ⟶ L.comp F'<VAR>self : F'.IsLeftKanExtension α<GOAL>Nonempty (CategoryTheory.StructuredArrow.IsUniversal (CategoryTheory.Functor.LeftExtension.mk F' α))
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_7, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : F ⟶ L.comp F'<VAR>F'.IsLeftKanExtension α<VAR>G : CategoryTheory.Functor D H<VAR>β : F ⟶ L.comp G<GOAL>CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L (F'.descOfIsLeftKanExtension α G β)) = β
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_7, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : F ⟶ L.comp F'<VAR>F'.IsLeftKanExtension α<VAR>G : CategoryTheory.Functor D H<VAR>β : F ⟶ L.comp G<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (α.app X) ((F'.descOfIsLeftKanExtension α G β).app (L.obj X)) = β.app X
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_7, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : F ⟶ L.comp F'<VAR>F'.IsLeftKanExtension α<VAR>G : CategoryTheory.Functor D H<VAR>γ₁ γ₂ : F' ⟶ G<VAR>hγ : CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L γ₁) = CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L γ₂)<GOAL>γ₁ = γ₂
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_7, u_5} D<VAR>F' F'' : CategoryTheory.Functor D H<VAR>e : F' ≅ F''<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : F ⟶ L.comp F'<VAR>α' : F ⟶ L.comp F''<VAR>comm : CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L e.hom) = α'<VAR>F'.IsLeftKanExtension α<GOAL>F''.IsLeftKanExtension α'
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_7, u_5} D<VAR>F' F'' : CategoryTheory.Functor D H<VAR>e : F' ≅ F''<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : F ⟶ L.comp F'<VAR>α' : F ⟶ L.comp F''<VAR>comm : CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L e.hom) = α'<GOAL>F'.IsLeftKanExtension α ↔ F''.IsLeftKanExtension α'
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : F ⟶ L.comp F'<VAR>F'.IsLeftKanExtension α<VAR>G : CategoryTheory.Functor C H<VAR>i : F ≅ G<VAR>G' : CategoryTheory.Functor D H<VAR>β : G ⟶ L.comp G'<VAR>G'.IsLeftKanExtension β<GOAL>(F'.leftKanExtensionUniqueOfIso α i G' β).inv = G'.descOfIsLeftKanExtension β F' (CategoryTheory.CategoryStruct.comp i.inv α)
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : F ⟶ L.comp F'<VAR>F'.IsLeftKanExtension α<VAR>G : CategoryTheory.Functor C H<VAR>i : F ≅ G<VAR>G' : CategoryTheory.Functor D H<VAR>β : G ⟶ L.comp G'<VAR>G'.IsLeftKanExtension β<GOAL>(F'.leftKanExtensionUniqueOfIso α i G' β).hom = F'.descOfIsLeftKanExtension α G' (CategoryTheory.CategoryStruct.comp i.hom β)
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : F ⟶ L.comp F'<VAR>F'.IsLeftKanExtension α<VAR>F'' : CategoryTheory.Functor D H<VAR>α' : F ⟶ L.comp F''<VAR>F''.IsLeftKanExtension α'<GOAL>(F'.leftKanExtensionUnique α F'' α').hom = F'.descOfIsLeftKanExtension α F'' α'
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : F ⟶ L.comp F'<VAR>F'.IsLeftKanExtension α<VAR>F'' : CategoryTheory.Functor D H<VAR>α' : F ⟶ L.comp F''<VAR>F''.IsLeftKanExtension α'<GOAL>(F'.leftKanExtensionUnique α F'' α').inv = F''.descOfIsLeftKanExtension α' F' α
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_7, u_5} D<VAR>F' F'' : CategoryTheory.Functor D H<VAR>φ : F' ⟶ F''<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : F ⟶ L.comp F'<VAR>α' : F ⟶ L.comp F''<VAR>comm : CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L φ) = α'<VAR>F'.IsLeftKanExtension α<GOAL>F''.IsLeftKanExtension α' ↔ CategoryTheory.IsIso φ
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_7, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : L.comp F' ⟶ F<VAR>F'.IsRightKanExtension α<GOAL>L.HasRightKanExtension F
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_7, u_5} D<VAR>F' : CategoryTheory.Functor D H<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>α : F ⟶ L.comp F'<VAR>F'.IsLeftKanExtension α<GOAL>L.HasLeftKanExtension F
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_7, u_5} D<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>L.HasRightKanExtension F<VAR>G : CategoryTheory.Functor D H<VAR>γ₁ γ₂ : G ⟶ L.rightKanExtension F<VAR>hγ : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L γ₁) (L.rightKanExtensionCounit F) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L γ₂) (L.rightKanExtensionCounit F)<GOAL>γ₁ = γ₂
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_7, u_5} D<VAR>L : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor C H<VAR>L.HasLeftKanExtension F<VAR>G : CategoryTheory.Functor D H<VAR>γ₁ γ₂ : L.leftKanExtension F ⟶ G<VAR>hγ : CategoryTheory.CategoryStruct.comp (L.leftKanExtensionUnit F) (CategoryTheory.whiskerLeft L γ₁) = CategoryTheory.CategoryStruct.comp (L.leftKanExtensionUnit F) (CategoryTheory.whiskerLeft L γ₂)<GOAL>γ₁ = γ₂
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>D' : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>CategoryTheory.Category.{u_10, u_6} D'<VAR>L : CategoryTheory.Functor C D<VAR>L' : CategoryTheory.Functor C D'<VAR>G : CategoryTheory.Functor D D'<VAR>f : L' ⟶ L.comp G<VAR>F : CategoryTheory.Functor C H<VAR>X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.whiskeringLeft C D' H).obj L')<GOAL>∀ (X_1 : C), ((CategoryTheory.Functor.LeftExtension.postcomp₁ G f F).obj X).hom.app X_1 = CategoryTheory.CategoryStruct.comp (X.hom.app X_1) (X.right.map (f.app X_1))
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>D' : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>CategoryTheory.Category.{u_10, u_6} D'<VAR>L : CategoryTheory.Functor C D<VAR>L' : CategoryTheory.Functor C D'<VAR>G : CategoryTheory.Functor D D'<VAR>f : L' ⟶ L.comp G<VAR>F : CategoryTheory.Functor C H<VAR>X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.whiskeringLeft C D' H).obj L')<VAR>φ : X ⟶ Y<GOAL>((CategoryTheory.Functor.LeftExtension.postcomp₁ G f F).map φ).left = CategoryTheory.CategoryStruct.id X.left
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>D' : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>CategoryTheory.Category.{u_10, u_6} D'<VAR>L : CategoryTheory.Functor C D<VAR>L' : CategoryTheory.Functor C D'<VAR>G : CategoryTheory.Functor D D'<VAR>f : L' ⟶ L.comp G<VAR>F : CategoryTheory.Functor C H<VAR>X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.whiskeringLeft C D' H).obj L')<GOAL>((CategoryTheory.Functor.LeftExtension.postcomp₁ G f F).obj X).left = X.left
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>D' : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>CategoryTheory.Category.{u_10, u_6} D'<VAR>L : CategoryTheory.Functor C D<VAR>L' : CategoryTheory.Functor C D'<VAR>G : CategoryTheory.Functor D D'<VAR>f : L' ⟶ L.comp G<VAR>F : CategoryTheory.Functor C H<VAR>X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.whiskeringLeft C D' H).obj L')<GOAL>∀ {X_1 Y : D} (f_1 : X_1 ⟶ Y), ((CategoryTheory.Functor.LeftExtension.postcomp₁ G f F).obj X).right.map f_1 = X.right.map (G.map f_1)
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>D' : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>CategoryTheory.Category.{u_10, u_6} D'<VAR>L : CategoryTheory.Functor C D<VAR>L' : CategoryTheory.Functor C D'<VAR>G : CategoryTheory.Functor D D'<VAR>f : L' ⟶ L.comp G<VAR>F : CategoryTheory.Functor C H<VAR>X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.whiskeringLeft C D' H).obj L')<VAR>φ : X ⟶ Y<GOAL>∀ (X_1 : D), ((CategoryTheory.Functor.LeftExtension.postcomp₁ G f F).map φ).right.app X_1 = φ.right.app (G.obj X_1)
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>D' : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>CategoryTheory.Category.{u_10, u_6} D'<VAR>L : CategoryTheory.Functor C D<VAR>L' : CategoryTheory.Functor C D'<VAR>G : CategoryTheory.Functor D D'<VAR>f : L' ⟶ L.comp G<VAR>F : CategoryTheory.Functor C H<VAR>X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.whiskeringLeft C D' H).obj L')<GOAL>∀ (X_1 : D), ((CategoryTheory.Functor.LeftExtension.postcomp₁ G f F).obj X).right.obj X_1 = X.right.obj (G.obj X_1)
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>D' : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>CategoryTheory.Category.{u_10, u_6} D'<VAR>L : CategoryTheory.Functor C D<VAR>L' : CategoryTheory.Functor C D'<VAR>G : CategoryTheory.Functor D D'<VAR>f : L.comp G ⟶ L'<VAR>F : CategoryTheory.Functor C H<VAR>X : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D' H).obj L') (CategoryTheory.Functor.fromPUnit F)<GOAL>((CategoryTheory.Functor.RightExtension.postcomp₁ G f F).obj X).right = X.right
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>D' : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>CategoryTheory.Category.{u_10, u_6} D'<VAR>L : CategoryTheory.Functor C D<VAR>L' : CategoryTheory.Functor C D'<VAR>G : CategoryTheory.Functor D D'<VAR>f : L.comp G ⟶ L'<VAR>F : CategoryTheory.Functor C H<VAR>X Y : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D' H).obj L') (CategoryTheory.Functor.fromPUnit F)<VAR>φ : X ⟶ Y<GOAL>∀ (X_1 : D), ((CategoryTheory.Functor.RightExtension.postcomp₁ G f F).map φ).left.app X_1 = φ.left.app (G.obj X_1)
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>D' : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>CategoryTheory.Category.{u_10, u_6} D'<VAR>L : CategoryTheory.Functor C D<VAR>L' : CategoryTheory.Functor C D'<VAR>G : CategoryTheory.Functor D D'<VAR>f : L.comp G ⟶ L'<VAR>F : CategoryTheory.Functor C H<VAR>X : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D' H).obj L') (CategoryTheory.Functor.fromPUnit F)<GOAL>∀ (X_1 : D), ((CategoryTheory.Functor.RightExtension.postcomp₁ G f F).obj X).left.obj X_1 = X.left.obj (G.obj X_1)
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>D' : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>CategoryTheory.Category.{u_10, u_6} D'<VAR>L : CategoryTheory.Functor C D<VAR>L' : CategoryTheory.Functor C D'<VAR>G : CategoryTheory.Functor D D'<VAR>f : L.comp G ⟶ L'<VAR>F : CategoryTheory.Functor C H<VAR>X : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D' H).obj L') (CategoryTheory.Functor.fromPUnit F)<GOAL>∀ (X_1 : C), ((CategoryTheory.Functor.RightExtension.postcomp₁ G f F).obj X).hom.app X_1 = CategoryTheory.CategoryStruct.comp (X.left.map (f.app X_1)) (X.hom.app X_1)
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>D' : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>CategoryTheory.Category.{u_10, u_6} D'<VAR>L : CategoryTheory.Functor C D<VAR>L' : CategoryTheory.Functor C D'<VAR>G : CategoryTheory.Functor D D'<VAR>f : L.comp G ⟶ L'<VAR>F : CategoryTheory.Functor C H<VAR>X Y : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D' H).obj L') (CategoryTheory.Functor.fromPUnit F)<VAR>φ : X ⟶ Y<GOAL>((CategoryTheory.Functor.RightExtension.postcomp₁ G f F).map φ).right = CategoryTheory.CategoryStruct.id X.right
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>D' : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_9, u_5} D<VAR>CategoryTheory.Category.{u_10, u_6} D'<VAR>L : CategoryTheory.Functor C D<VAR>L' : CategoryTheory.Functor C D'<VAR>G : CategoryTheory.Functor D D'<VAR>f : L.comp G ⟶ L'<VAR>F : CategoryTheory.Functor C H<VAR>X : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D' H).obj L') (CategoryTheory.Functor.fromPUnit F)<GOAL>∀ {X_1 Y : D} (f_1 : X_1 ⟶ Y), ((CategoryTheory.Functor.RightExtension.postcomp₁ G f F).obj X).left.map f_1 = X.left.map (G.map f_1)
<VAR>C : Type u_1<VAR>H : Type u_3<VAR>D : Type u_5<VAR>D' : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_8, u_3} H<VAR>CategoryTheory.Category.{u_10, u_5} D<VAR>CategoryTheory.Category.{u_9, u_6} D'<VAR>L : CategoryTheory.Functor C D<VAR>L' : CategoryTheory.Functor C D'<VAR>G : CategoryTheory.Functor D D'<VAR>G.IsEquivalence<VAR>e : L.comp G ≅ L'<VAR>F : CategoryTheory.Functor C H<GOAL>L'.HasLeftKanExtension F ↔ L.HasLeftKanExtension F