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>F : CategoryTheory.Functor C D<VAR>F.Initial<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<GOAL>(CategoryTheory.Functor.Initial.conesEquiv F G).inverse = CategoryTheory.Limits.Cones.whiskering 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.Initial<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<GOAL>(CategoryTheory.Functor.Initial.conesEquiv F G).functor = CategoryTheory.Functor.Initial.extendCone
<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.Initial<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<GOAL>(CategoryTheory.Functor.Initial.conesEquiv F G).unitIso = CategoryTheory.NatIso.ofComponents (fun c => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone (F.comp G))).obj c).pt) ⋯) ⋯
<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.Initial<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<VAR>t : CategoryTheory.Limits.LimitCone G<GOAL>(CategoryTheory.Functor.Initial.limitConeComp F t).isLimit = (CategoryTheory.Functor.Initial.isLimitWhiskerEquiv F t.cone).symm t.isLimit
<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.Initial<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<VAR>t : CategoryTheory.Limits.LimitCone G<GOAL>(CategoryTheory.Functor.Initial.limitConeComp F t).cone = CategoryTheory.Limits.Cone.whisker F t.cone
<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.Initial<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<VAR>t : CategoryTheory.Limits.LimitCone (F.comp G)<GOAL>(CategoryTheory.Functor.Initial.limitConeOfComp F t).cone = CategoryTheory.Functor.Initial.extendCone.obj t.cone
<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.Initial<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<VAR>t : CategoryTheory.Limits.LimitCone (F.comp G)<GOAL>(CategoryTheory.Functor.Initial.limitConeOfComp F t).isLimit = (CategoryTheory.Functor.Initial.isLimitExtendConeEquiv F t.cone).symm t.isLimit
<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.Initial<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<VAR>CategoryTheory.Limits.HasLimit (F.comp G)<GOAL>CategoryTheory.Limits.HasLimit 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>F.Initial<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.Limits.HasLimitsOfShape C E<GOAL>CategoryTheory.Limits.HasLimitsOfShape D E
<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>G.Full<VAR>G.Faithful<VAR>(F.comp G).Final<GOAL>F.Final
<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>G.Full<VAR>G.Faithful<VAR>(F.comp G).Initial<GOAL>F.Initial
<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.Final<VAR>G.IsEquivalence<GOAL>(F.comp G).Final
<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.Initial<VAR>G.IsEquivalence<GOAL>(F.comp G).Initial
<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.IsEquivalence<VAR>G.Final<GOAL>(F.comp G).Final
<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.IsEquivalence<VAR>G.Initial<GOAL>(F.comp G).Initial
<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.IsEquivalence<VAR>(F.comp G).Final<GOAL>G.Final
<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.IsEquivalence<VAR>(F.comp G).Initial<GOAL>G.Initial
<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>G.IsEquivalence<GOAL>F.Final ↔ (F.comp G).Final
<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.IsEquivalence<GOAL>G.Final ↔ (F.comp G).Final
<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>G.IsEquivalence<GOAL>F.Initial ↔ (F.comp G).Initial
<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.IsEquivalence<GOAL>G.Initial ↔ (F.comp G).Initial
<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>hF : F.Final<VAR>hFG : (F.comp G).Final<GOAL>G.Final
<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.Initial<VAR>(F.comp G).Initial<GOAL>G.Initial
<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>G.Full<VAR>G.Faithful<VAR>(F.comp G).Final<GOAL>G.Final
<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>G.Full<VAR>G.Faithful<VAR>(F.comp G).Initial<GOAL>G.Initial
<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>G.Final<VAR>G.Full<VAR>G.Faithful<GOAL>F.Final ↔ (F.comp G).Final
<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>G.Initial<VAR>G.Full<VAR>G.Faithful<GOAL>F.Initial ↔ (F.comp G).Initial
<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.Final<GOAL>G.Final ↔ (F.comp G).Final
<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.Initial<GOAL>G.Initial ↔ (F.comp G).Initial
<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.Final<VAR>CategoryTheory.IsFilteredOrEmpty C<GOAL>CategoryTheory.IsFilteredOrEmpty D
<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.Final<VAR>CategoryTheory.IsFiltered C<GOAL>CategoryTheory.IsFiltered D
<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.Initial<VAR>CategoryTheory.IsCofilteredOrEmpty C<GOAL>CategoryTheory.IsCofilteredOrEmpty D
<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.Initial<VAR>CategoryTheory.IsCofiltered C<GOAL>CategoryTheory.IsCofiltered D
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<VAR>self : X.Hom Y<GOAL>(CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst self.F)).obj X.rel ≤ (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map self.f (CategoryTheory.CategoryStruct.id Y.tgt))).obj Y.rel
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : CategoryTheory.Dial C<VAR>F : X.Hom Y<VAR>G : Y.Hom Z<GOAL>(CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map F.f (CategoryTheory.CategoryStruct.id Z.tgt)) G.F)) F.F))).obj X.rel ≤ (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.comp F.f G.f) (CategoryTheory.CategoryStruct.id Z.tgt))).obj Z.rel
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>(CategoryTheory.CategoryStruct.id X).F = CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : CategoryTheory.Dial C<VAR>F : X.Hom Y<VAR>G : Y.Hom Z<GOAL>(CategoryTheory.CategoryStruct.comp F G).F = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map F.f (CategoryTheory.CategoryStruct.id Z.tgt)) G.F)) F.F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>(CategoryTheory.CategoryStruct.id X).f = CategoryTheory.CategoryStruct.id X.src
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : CategoryTheory.Dial C<VAR>F : X.Hom Y<VAR>G : Y.Hom Z<GOAL>(CategoryTheory.CategoryStruct.comp F G).f = CategoryTheory.CategoryStruct.comp F.f G.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<VAR>x y : X ⟶ Y<VAR>hf : x.f = y.f<VAR>hF : x.F = y.F<GOAL>x = y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<VAR>e₁ : X.src ≅ Y.src<VAR>e₂ : X.tgt ≅ Y.tgt<VAR>eq : X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel<GOAL>(CategoryTheory.Dial.isoMk e₁ e₂ eq).inv.F = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd e₂.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<VAR>e₁ : X.src ≅ Y.src<VAR>e₂ : X.tgt ≅ Y.tgt<VAR>eq : X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel<GOAL>(CategoryTheory.Dial.isoMk e₁ e₂ eq).hom.f = e₁.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<VAR>e₁ : X.src ≅ Y.src<VAR>e₂ : X.tgt ≅ Y.tgt<VAR>eq : X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel<GOAL>(CategoryTheory.Dial.isoMk e₁ e₂ eq).hom.F = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd e₂.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<VAR>e₁ : X.src ≅ Y.src<VAR>e₂ : X.tgt ≅ Y.tgt<VAR>eq : X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel<GOAL>(CategoryTheory.Dial.isoMk e₁ e₂ eq).inv.f = e₁.inv
<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>∀ (d : D), CategoryTheory.IsFiltered (CategoryTheory.StructuredArrow d F)<GOAL>F.Final
<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>∀ (d : D), CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow F d)<GOAL>F.Initial
<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>CategoryTheory.IsFilteredOrEmpty C<VAR>h₁ : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)<VAR>h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)<VAR>d : D<GOAL>CategoryTheory.IsFiltered (CategoryTheory.StructuredArrow d 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>CategoryTheory.IsCofilteredOrEmpty C<VAR>h₁ : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)<VAR>h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s'<VAR>d : D<GOAL>CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow F d)
<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>CategoryTheory.IsFilteredOrEmpty C<VAR>h₁ : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)<VAR>h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)<GOAL>F.Final
<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>CategoryTheory.IsCofilteredOrEmpty C<VAR>h₁ : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)<VAR>h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s'<GOAL>F.Initial
<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>CategoryTheory.IsFilteredOrEmpty D<VAR>F.Full<VAR>F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)<GOAL>CategoryTheory.IsFilteredOrEmpty C
<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>CategoryTheory.IsCofilteredOrEmpty D<VAR>F.Full<VAR>F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)<GOAL>CategoryTheory.IsCofilteredOrEmpty C
<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>CategoryTheory.IsFiltered D<VAR>F.Full<VAR>F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)<GOAL>CategoryTheory.IsFiltered C
<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>CategoryTheory.IsCofiltered D<VAR>F.Full<VAR>F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)<GOAL>CategoryTheory.IsCofiltered C
<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>CategoryTheory.IsFilteredOrEmpty D<VAR>F.Full<VAR>F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)<GOAL>F.Final
<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>CategoryTheory.IsCofilteredOrEmpty D<VAR>F.Full<VAR>F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)<GOAL>F.Initial
<VAR>C : Type v₁<VAR>CategoryTheory.Category.{v₁, v₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.IsFilteredOrEmpty C<GOAL>F.Final ↔ (∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) ∧ ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)
<VAR>C : Type v₁<VAR>CategoryTheory.Category.{v₁, v₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.IsCofilteredOrEmpty C<GOAL>F.Initial ↔ (∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) ∧ ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s'
<VAR>C : Type v₁<VAR>CategoryTheory.Category.{v₁, v₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.IsFilteredOrEmpty C<VAR>F.Final<VAR>d : D<VAR>c : C<VAR>s s' : d ⟶ F.obj c<GOAL>∃ c' t, CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)
<VAR>C : Type v₁<VAR>CategoryTheory.Category.{v₁, v₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.IsCofilteredOrEmpty C<VAR>F.Initial<VAR>d : D<VAR>c : C<VAR>s s' : F.obj c ⟶ d<GOAL>∃ c' t, CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s'
<VAR>C : Type v₁<VAR>CategoryTheory.Category.{v₁, v₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.IsFilteredOrEmpty C<GOAL>F.Final ↔ ∀ (d : D), CategoryTheory.IsFiltered (CategoryTheory.StructuredArrow d F)
<VAR>C : Type v₁<VAR>CategoryTheory.Category.{v₁, v₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.IsCofilteredOrEmpty C<GOAL>F.Initial ↔ ∀ (d : D), CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow F d)
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>X Y : CategoryTheory.Arrow T<VAR>f g : X ⟶ Y<VAR>h₁ : f.left = g.left<VAR>h₂ : f.right = g.right<GOAL>f = g
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f : CategoryTheory.Arrow T<GOAL>(CategoryTheory.CategoryStruct.id f).left = CategoryTheory.CategoryStruct.id f.left
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f : CategoryTheory.Arrow T<GOAL>(CategoryTheory.CategoryStruct.id f).right = CategoryTheory.CategoryStruct.id f.right
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>X Y Z : CategoryTheory.Arrow T<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.CategoryStruct.comp f g).left = CategoryTheory.CategoryStruct.comp f.left g.left
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>X Y Z : CategoryTheory.Arrow T<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.CategoryStruct.comp f g).right = CategoryTheory.CategoryStruct.comp f.right g.right
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>X Y : T<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Arrow.mk f).right = Y
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>X Y : T<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Arrow.mk f).left = X
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>X Y : T<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Arrow.mk f).hom = f
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f : CategoryTheory.Arrow T<GOAL>CategoryTheory.Arrow.mk f.hom = f
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>A B : T<GOAL>Function.Injective CategoryTheory.Arrow.mk
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>A B : T<VAR>f g : A ⟶ B<GOAL>CategoryTheory.Arrow.mk f = CategoryTheory.Arrow.mk g ↔ f = g
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f g : CategoryTheory.Arrow T<VAR>u : f.left ⟶ g.left<VAR>v : f.right ⟶ g.right<VAR>w : CategoryTheory.CategoryStruct.comp u g.hom = CategoryTheory.CategoryStruct.comp f.hom v<GOAL>(CategoryTheory.Arrow.homMk w).right = v
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f g : CategoryTheory.Arrow T<VAR>u : f.left ⟶ g.left<VAR>v : f.right ⟶ g.right<VAR>w : CategoryTheory.CategoryStruct.comp u g.hom = CategoryTheory.CategoryStruct.comp f.hom v<GOAL>(CategoryTheory.Arrow.homMk w).left = u
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>X Y : T<VAR>f : X ⟶ Y<VAR>P Q : T<VAR>g : P ⟶ Q<VAR>u : X ⟶ P<VAR>v : Y ⟶ Q<VAR>w : CategoryTheory.CategoryStruct.comp u g = CategoryTheory.CategoryStruct.comp f v<GOAL>(CategoryTheory.Arrow.homMk' w).left = u
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>X Y : T<VAR>f : X ⟶ Y<VAR>P Q : T<VAR>g : P ⟶ Q<VAR>u : X ⟶ P<VAR>v : Y ⟶ Q<VAR>w : CategoryTheory.CategoryStruct.comp u g = CategoryTheory.CategoryStruct.comp f v<GOAL>(CategoryTheory.Arrow.homMk' w).right = v
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f g : CategoryTheory.Arrow T<VAR>sq : f ⟶ g<GOAL>CategoryTheory.CategoryStruct.comp sq.left g.hom = CategoryTheory.CategoryStruct.comp f.hom sq.right
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f : CategoryTheory.Arrow T<VAR>X Y : T<VAR>g : X ⟶ Y<VAR>sq : f ⟶ CategoryTheory.Arrow.mk g<GOAL>CategoryTheory.CategoryStruct.comp sq.left g = CategoryTheory.CategoryStruct.comp f.hom sq.right
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f g : CategoryTheory.Arrow T<VAR>ff : f ⟶ g<VAR>CategoryTheory.IsIso ff.left<VAR>CategoryTheory.IsIso ff.right<GOAL>CategoryTheory.IsIso ff
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f g : CategoryTheory.Arrow T<VAR>l : f.left ≅ g.left<VAR>r : f.right ≅ g.right<VAR>h : CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom := by aesop_cat<GOAL>(CategoryTheory.Arrow.isoMk l r h).inv.left = l.inv