ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X₁ X₂ : Type u<VAR>f : X₁ ⟶ X₂<VAR>Y : Type u<GOAL>∀ (a : (CategoryTheory.Limits.BinaryFan.mk (Prod.fst ≫ f) Prod.snd).pt), (CategoryTheory.Limits.Types.binaryProductFunctor.map f).app Y a = (CategoryTheory.Limits.Types.binaryProductLimit X₂ Y).lift (CategoryTheory.Limits.BinaryFan.mk (Prod.fst ≫ f) Prod.snd) a
<VAR>X Y : Type u<GOAL>(CategoryTheory.Limits.Types.binaryCoproductCocone X Y).pt = (X ⊕ Y)
<VAR>X Y : Type u<GOAL>∀ (x : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (a : (CategoryTheory.Limits.pair X Y).obj x), (CategoryTheory.Limits.Types.binaryCoproductCocone X Y).ι.app x a = (match x.as with | CategoryTheory.Limits.WalkingPair.left => Sum.inl | CategoryTheory.Limits.WalkingPair.right => Sum.inr) a
<VAR>X Y : Type u<VAR>s : CategoryTheory.Limits.BinaryCofan X Y<GOAL>∀ (a : X ⊕ Y), (CategoryTheory.Limits.Types.binaryCoproductColimit X Y).desc s a = Sum.elim s.inl s.inr a
<VAR>X Y : Type u<GOAL>CategoryTheory.Limits.coprod.inl ≫ (CategoryTheory.Limits.Types.binaryCoproductIso X Y).hom = Sum.inl
<VAR>X Y : Type u<GOAL>CategoryTheory.Limits.coprod.inr ≫ (CategoryTheory.Limits.Types.binaryCoproductIso X Y).hom = Sum.inr
<VAR>X Y : Type u<GOAL>↾Sum.inl ≫ (CategoryTheory.Limits.Types.binaryCoproductIso X Y).inv = CategoryTheory.Limits.coprod.inl
<VAR>X Y : Type u<GOAL>↾Sum.inr ≫ (CategoryTheory.Limits.Types.binaryCoproductIso X Y).inv = CategoryTheory.Limits.coprod.inr
<VAR>X Y : Type u<VAR>c : CategoryTheory.Limits.BinaryCofan X Y<GOAL>Nonempty (CategoryTheory.Limits.IsColimit c) ↔ Function.Injective c.inl ∧ Function.Injective c.inr ∧ IsCompl (Set.range c.inl) (Set.range c.inr)
<VAR>J : Type v<VAR>F : J → TypeMax<VAR>j : J<GOAL>((CategoryTheory.Limits.Types.productIso F).hom ≫ fun f => f j) = CategoryTheory.Limits.Pi.π F j
<VAR>J : Type v<VAR>F : J → TypeMax<VAR>j : J<VAR>x : ∏ᶜ F<GOAL>(CategoryTheory.Limits.Types.productIso F).hom x j = CategoryTheory.Limits.Pi.π F j x
<VAR>J : Type v<VAR>F : J → TypeMax<VAR>j : J<GOAL>(CategoryTheory.Limits.Types.productIso F).inv ≫ CategoryTheory.Limits.Pi.π F j = fun f => f j
<VAR>J : Type v<VAR>F : J → Type u<VAR>Small.{u, v} J<VAR>j : J<GOAL>((CategoryTheory.Limits.Types.Small.productIso F).hom ≫ fun f => (equivShrink ((j : J) → F j)).symm f j) = CategoryTheory.Limits.Pi.π F j
<VAR>J : Type v<VAR>F : J → Type u<VAR>Small.{u, v} J<VAR>j : J<VAR>x : ∏ᶜ F<GOAL>(equivShrink ((j : J) → F j)).symm ((CategoryTheory.Limits.Types.Small.productIso F).hom x) j = CategoryTheory.Limits.Pi.π F j x
<VAR>J : Type v<VAR>F : J → Type u<VAR>Small.{u, v} J<VAR>j : J<GOAL>(CategoryTheory.Limits.Types.Small.productIso F).inv ≫ CategoryTheory.Limits.Pi.π F j = fun f => (equivShrink ((j : J) → F j)).symm f j
<VAR>J : Type v<VAR>F : J → TypeMax<VAR>j : J<GOAL>CategoryTheory.Limits.Sigma.ι F j ≫ (CategoryTheory.Limits.Types.coproductIso F).hom = fun x => ⟨j, x⟩
<VAR>J : Type v<VAR>F : J → TypeMax<VAR>j : J<GOAL>(↾fun x => ⟨j, x⟩) ≫ (CategoryTheory.Limits.Types.coproductIso F).inv = CategoryTheory.Limits.Sigma.ι F j
<VAR>X Y Z : Type u<VAR>f : X ⟶ Y<VAR>g h : Y ⟶ Z<VAR>w : f ≫ g = f ≫ h<VAR>t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w)<VAR>y : Y<VAR>hy : g y = h y<GOAL>∃! x, f x = y
<VAR>X Y Z : Type u<VAR>f : X ⟶ Y<VAR>g h : Y ⟶ Z<VAR>w : f ≫ g = f ≫ h<GOAL>Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w)) ↔ ∀ (y : Y), g y = h y → ∃! x, f x = y
<VAR>Y Z : Type u<VAR>g h : Y ⟶ Z<GOAL>(CategoryTheory.Limits.Types.equalizerIso g h).hom ≫ Subtype.val = CategoryTheory.Limits.equalizer.ι g h
<VAR>Y Z : Type u<VAR>g h : Y ⟶ Z<GOAL>(CategoryTheory.Limits.Types.equalizerIso g h).inv ≫ CategoryTheory.Limits.equalizer.ι g h = Subtype.val
<VAR>X Y Z : Type u<VAR>f g : X ⟶ Y<VAR>π : Y ⟶ Z<VAR>e : f ≫ π = g ≫ π<VAR>h : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ π e)<VAR>U : Set Y<VAR>H : f ⁻¹' U = g ⁻¹' U<GOAL>π ⁻¹' (π '' U) = U
<VAR>X Y : Type u<VAR>f g : X ⟶ Y<GOAL>CategoryTheory.Limits.coequalizer.π f g ≫ (CategoryTheory.Limits.Types.coequalizerIso f g).hom = Quot.mk (CategoryTheory.Limits.Types.CoequalizerRel f g)
<VAR>X Y : Type u<VAR>f g : X ⟶ Y<GOAL>↾Quot.mk (CategoryTheory.Limits.Types.CoequalizerRel f g) ≫ (CategoryTheory.Limits.Types.coequalizerIso f g).inv = CategoryTheory.Limits.coequalizer.π f g
<VAR>X Y Z : Type u<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.Types.pullbackLimitCone f g).cone = CategoryTheory.Limits.Types.pullbackCone f g
<VAR>X Y Z : Type u<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.Types.pullbackLimitCone f g).isLimit = (CategoryTheory.Limits.Types.pullbackCone f g).isLimitAux (fun s x => ⟨(s.fst x, s.snd x), ⋯⟩) ⋯ ⋯ ⋯
<VAR>X Y S : Type v<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>c : CategoryTheory.Limits.PullbackCone f g<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>x : c.pt<GOAL>(↑((CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj hc) x)).1 = c.fst x
<VAR>X Y S : Type v<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>c : CategoryTheory.Limits.PullbackCone f g<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>x : c.pt<GOAL>(↑((CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj hc) x)).2 = c.snd x
<VAR>X Y S : Type v<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>c : CategoryTheory.Limits.PullbackCone f g<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>x : CategoryTheory.Limits.Types.PullbackObj f g<GOAL>c.fst ((CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj hc).symm x) = (↑x).1
<VAR>X Y S : Type v<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>c : CategoryTheory.Limits.PullbackCone f g<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>x : CategoryTheory.Limits.Types.PullbackObj f g<GOAL>c.snd ((CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj hc).symm x) = (↑x).2
<VAR>X Y S : Type v<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>c : CategoryTheory.Limits.PullbackCone f g<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>x y : c.pt<VAR>h₁ : c.fst x = c.fst y<VAR>h₂ : c.snd x = c.snd y<GOAL>x = y
<VAR>X Y S : Type v<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>c : CategoryTheory.Limits.PullbackCone f g<VAR>x : c.pt<GOAL>(↑(c.toPullbackObj x)).1 = c.fst x
<VAR>X Y S : Type v<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>c : CategoryTheory.Limits.PullbackCone f g<VAR>x : c.pt<GOAL>(↑(c.toPullbackObj x)).2 = c.snd x
<VAR>X Y Z : Type u<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>p : CategoryTheory.Limits.pullback f g<GOAL>(↑((CategoryTheory.Limits.Types.pullbackIsoPullback f g).hom p)).1 = CategoryTheory.Limits.pullback.fst f g p
<VAR>X Y Z : Type u<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>p : CategoryTheory.Limits.pullback f g<GOAL>(↑((CategoryTheory.Limits.Types.pullbackIsoPullback f g).hom p)).2 = CategoryTheory.Limits.pullback.snd f g p
<VAR>X Y Z : Type u<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>x : (CategoryTheory.Limits.Types.pullbackCone f g).pt<GOAL>CategoryTheory.Limits.pullback.fst f g ((CategoryTheory.Limits.Types.pullbackIsoPullback f g).inv x) = (fun p => (↑p).1) x
<VAR>X Y Z : Type u<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>x : (CategoryTheory.Limits.Types.pullbackCone f g).pt<GOAL>CategoryTheory.Limits.pullback.snd f g ((CategoryTheory.Limits.Types.pullbackIsoPullback f g).inv x) = (fun p => (↑p).2) x
<VAR>X Y Z : Type u<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.Types.pullbackIsoPullback f g).inv ≫ CategoryTheory.Limits.pullback.fst f g = fun p => (↑p).1
<VAR>X Y Z : Type u<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.Types.pullbackIsoPullback f g).inv ≫ CategoryTheory.Limits.pullback.snd f g = fun p => (↑p).2
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<GOAL>f ≫ CategoryTheory.Limits.Types.Pushout.inl f g = g ≫ CategoryTheory.Limits.Types.Pushout.inr f g
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<VAR>j : CategoryTheory.Limits.WalkingSpan<GOAL>∀ (a : (CategoryTheory.Limits.span f g).obj j), (CategoryTheory.Limits.Types.Pushout.cocone f g).ι.app j a = Option.rec (f ≫ CategoryTheory.Limits.Types.Pushout.inl f g) (fun val => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Limits.Types.Pushout.inl f g) (CategoryTheory.Limits.Types.Pushout.inr f g) val) j a
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<GOAL>(CategoryTheory.Limits.Types.Pushout.cocone f g).pt = CategoryTheory.Limits.Types.Pushout f g
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<VAR>x₁ y₁ : X₁<GOAL>CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inl x₁) (Sum.inl y₁) ↔ x₁ = y₁ ∨ ∃ x₀ y₀, ∃ (_ : g x₀ = g y₀), x₁ = f x₀ ∧ y₁ = f y₀
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<VAR>x₁ : X₁<VAR>x₂ : X₂<GOAL>CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inl x₁) (Sum.inr x₂) ↔ ∃ s, x₁ = f s ∧ x₂ = g s
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<VAR>x₂ y₂ : X₂<GOAL>CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inr x₂) (Sum.inr y₂) ↔ x₂ = y₂
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<VAR>x y : X₁ ⊕ X₂<VAR>h : CategoryTheory.Limits.Types.Pushout.Rel' f g x y<GOAL>CategoryTheory.Limits.Types.Pushout.Rel' f g y x
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<VAR>CategoryTheory.Mono f<GOAL>Equivalence (CategoryTheory.Limits.Types.Pushout.Rel' f g)
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<VAR>CategoryTheory.Mono f<VAR>a b : X₁ ⊕ X₂<GOAL>Quot.mk (CategoryTheory.Limits.Types.Pushout.Rel f g) a = Quot.mk (CategoryTheory.Limits.Types.Pushout.Rel f g) b ↔ CategoryTheory.Limits.Types.Pushout.Rel' f g a b
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<VAR>CategoryTheory.Mono f<VAR>x₁ : X₁<VAR>x₂ : X₂<GOAL>CategoryTheory.Limits.Types.Pushout.inl f g x₁ = CategoryTheory.Limits.Types.Pushout.inr f g x₂ ↔ ∃ s, f s = x₁ ∧ g s = x₂
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<VAR>c c' : CategoryTheory.Limits.PushoutCocone f g<VAR>e : c ≅ c'<VAR>x₁ : X₁<VAR>x₂ : X₂<VAR>h : c.inl x₁ = c.inr x₂<GOAL>c'.inl x₁ = c'.inr x₂
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<VAR>c c' : CategoryTheory.Limits.PushoutCocone f g<VAR>e : c ≅ c'<VAR>x₁ : X₁<VAR>x₂ : X₂<GOAL>c.inl x₁ = c.inr x₂ ↔ c'.inl x₁ = c'.inr x₂
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<VAR>c : CategoryTheory.Limits.PushoutCocone f g<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>h₁ : Function.Injective f<VAR>x₁ : X₁<VAR>x₂ : X₂<GOAL>c.inl x₁ = c.inr x₂ ↔ ∃ s, f s = x₁ ∧ g s = x₂
<VAR>I : CategoryTheory.Limits.MulticospanIndex (Type u)<VAR>self : I.sections<VAR>r : I.R<GOAL>I.fst r (self.val (I.fstTo r)) = I.snd r (self.val (I.sndTo r))
<VAR>I : CategoryTheory.Limits.MulticospanIndex (Type u)<VAR>s : ↑I.multicospan.sections<VAR>i : I.L<GOAL>(I.sectionsEquiv.symm s).val i = ↑s (CategoryTheory.Limits.WalkingMulticospan.left i)
<VAR>I : CategoryTheory.Limits.MulticospanIndex (Type u)<VAR>s : I.sections<VAR>i : CategoryTheory.Limits.WalkingMulticospan I.fstTo I.sndTo<GOAL>↑(I.sectionsEquiv s) i = match i with | CategoryTheory.Limits.WalkingMulticospan.left i => s.val i | CategoryTheory.Limits.WalkingMulticospan.right j => I.fst j (s.val (I.fstTo j))
<VAR>I : CategoryTheory.Limits.MulticospanIndex (Type u)<VAR>c : CategoryTheory.Limits.Multifork I<VAR>x : c.pt<VAR>i : I.L<GOAL>(c.toSections x).val i = c.ι i x
<VAR>I : CategoryTheory.Limits.MulticospanIndex (Type u)<VAR>c : CategoryTheory.Limits.Multifork I<GOAL>⇑I.sectionsEquiv.symm ∘ CategoryTheory.Limits.Types.sectionOfCone c = c.toSections
<VAR>I : CategoryTheory.Limits.MulticospanIndex (Type u)<VAR>c : CategoryTheory.Limits.Multifork I<GOAL>Nonempty (CategoryTheory.Limits.IsLimit c) ↔ Function.Bijective c.toSections
<VAR>I : CategoryTheory.Limits.MulticospanIndex (Type u)<VAR>c : CategoryTheory.Limits.Multifork I<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>x : c.pt<VAR>i : I.L<GOAL>((CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv hc).symm x).val i = c.ι i x
<VAR>I : CategoryTheory.Limits.MulticospanIndex (Type u)<VAR>c : CategoryTheory.Limits.Multifork I<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>s : I.sections<VAR>i : I.L<GOAL>c.ι i ((CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv hc) s) = s.val i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} ℰ<VAR>A : CategoryTheory.Functor C ℰ<VAR>X : ℰ<GOAL>∀ (X_1 : Cᵒᵖ), ((CategoryTheory.Presheaf.restrictedYoneda A).obj X).obj X_1 = (A.obj (Opposite.unop X_1) ⟶ X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} ℰ<VAR>A : CategoryTheory.Functor C ℰ<GOAL>∀ {X Y : ℰ} (f : X ⟶ Y) (X_1 : Cᵒᵖ) (a : (CategoryTheory.yoneda.obj X).obj (A.op.obj X_1)), ((CategoryTheory.Presheaf.restrictedYoneda A).map f).app X_1 a = CategoryTheory.CategoryStruct.comp a f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} ℰ<VAR>A : CategoryTheory.Functor C ℰ<VAR>X : ℰ<GOAL>∀ {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y) (a : (CategoryTheory.yoneda.obj X).obj (A.op.obj X_1)), ((CategoryTheory.Presheaf.restrictedYoneda A).obj X).map f a = CategoryTheory.CategoryStruct.comp (A.map f.unop) a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} ℰ<VAR>A : CategoryTheory.Functor C ℰ<VAR>CategoryTheory.yoneda.HasPointwiseLeftKanExtension A<VAR>L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) ℰ<VAR>α : A ⟶ CategoryTheory.yoneda.comp L<VAR>L.IsLeftKanExtension α<GOAL>CategoryTheory.IsIso α
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type v₁)<GOAL>(CategoryTheory.Presheaf.coconeOfRepresentable P).pt = P
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>x : P.Elementsᵒᵖ<GOAL>(CategoryTheory.Presheaf.coconeOfRepresentable P).ι.app x = CategoryTheory.yonedaEquiv.symm (Opposite.unop x).snd
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P₁ P₂ : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>α : P₁ ⟶ P₂<VAR>j : P₁.Elementsᵒᵖ<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.Presheaf.coconeOfRepresentable P₁).ι.app j) α = (CategoryTheory.Presheaf.coconeOfRepresentable P₂).ι.app ((CategoryTheory.CategoryOfElements.map α).op.obj j)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} ℰ<VAR>A : CategoryTheory.Functor C ℰ<VAR>CategoryTheory.yoneda.HasPointwiseLeftKanExtension A<VAR>L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) ℰ<VAR>α : A ⟶ CategoryTheory.yoneda.comp L<GOAL>L.IsLeftKanExtension α ↔ CategoryTheory.IsIso α ∧ Nonempty (CategoryTheory.Limits.PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} ℰ<VAR>A : CategoryTheory.Functor C ℰ<VAR>CategoryTheory.yoneda.HasPointwiseLeftKanExtension A<VAR>L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) ℰ<VAR>e : A ≅ CategoryTheory.yoneda.comp L<VAR>CategoryTheory.Limits.PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L<GOAL>L.IsLeftKanExtension e.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} ℰ<VAR>L : CategoryTheory.Functor (CategoryTheory.Functor C (Type v₁)) ℰ<VAR>CategoryTheory.Limits.PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L<VAR>CategoryTheory.yoneda.HasPointwiseLeftKanExtension (CategoryTheory.yoneda.comp ((CategoryTheory.opOpEquivalence C).congrLeft.functor.comp L))<GOAL>L.IsLeftAdjoint
<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>∀ (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P<VAR>X : C<GOAL>((CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan F).inv.app X).app (Opposite.op (F.obj X)) ((F.op.lanUnit.app (CategoryTheory.yoneda.obj X)).app (Opposite.op X) (CategoryTheory.CategoryStruct.id X)) = CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op (F.obj X)))
<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 (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))<VAR>φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>x y : P.Elements<VAR>f : x ⟶ y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (↑f).unop) (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.coconeApp φ x) = CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.coconeApp φ 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>G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))<VAR>φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>X : C<VAR>f : CategoryTheory.yoneda.obj X ⟶ P<GOAL>CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.presheafHom φ P)) = (G.map f).app (Opposite.op (F.obj X)) ((φ.app X).app (Opposite.op (F.obj X)) (CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op (F.obj X)))))
<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 (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))<VAR>φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G<VAR>X : C<GOAL>CategoryTheory.yonedaEquiv (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.presheafHom φ (CategoryTheory.yoneda.obj X)) = (φ.app X).app (F.op.obj (Opposite.op X)) (CategoryTheory.CategoryStruct.id (Opposite.unop (F.op.obj (Opposite.op X))))
<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 (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))<VAR>φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G<VAR>P Q : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>f : P ⟶ Q<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.presheafHom φ P) (CategoryTheory.whiskerLeft F.op (G.map f)) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.presheafHom φ Q)
<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>∀ (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P<VAR>G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))<VAR>φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G<VAR>X : C<GOAL>(CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.natTrans φ).app (CategoryTheory.yoneda.obj X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan F).inv.app X) (φ.app X)
<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>∀ (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P<VAR>Φ : CategoryTheory.yoneda.LeftExtension (F.comp CategoryTheory.yoneda)<VAR>f g : CategoryTheory.Functor.LeftExtension.mk F.op.lan (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan F).hom ⟶ Φ<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type v₁)<GOAL>(CategoryTheory.Presheaf.tautologicalCocone P).pt = P
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda P<GOAL>(CategoryTheory.Presheaf.tautologicalCocone P).ι.app X = X.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>I : Type v₁<VAR>CategoryTheory.SmallCategory I<VAR>F : CategoryTheory.Functor I C<VAR>c : CategoryTheory.Limits.Cocone (F.comp CategoryTheory.yoneda)<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(c.toCostructuredArrow.comp (CategoryTheory.CostructuredArrow.pre F CategoryTheory.yoneda c.pt)).Final
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<VAR>Y Z : C<VAR>f : Y ⟶ Z<GOAL>0 ≫ f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<GOAL>f ≫ 0 = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<GOAL>f ≫ 0 = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : Y ⟶ Z<GOAL>0 ≫ f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I J : CategoryTheory.Limits.HasZeroMorphisms C<VAR>w : ∀ (X Y : C), Zero.zero = Zero.zero<GOAL>I = J
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I J : CategoryTheory.Limits.HasZeroMorphisms C<GOAL>I = J
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<GOAL>Quiver.Hom.op 0 = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : Cᵒᵖ<GOAL>Quiver.Hom.unop 0 = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Mono g<VAR>h : f ≫ g = 0<GOAL>f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Epi f<VAR>h : f ≫ g = 0<GOAL>g = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>w : CategoryTheory.Limits.image.ι f = 0<GOAL>f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>w : f ≠ 0<GOAL>CategoryTheory.Limits.image.ι f ≠ 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F G : C ⥤ D<VAR>j : C<GOAL>CategoryTheory.NatTrans.app 0 j = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>o : CategoryTheory.Limits.IsZero X<VAR>f : X ⟶ Y<GOAL>f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>o : CategoryTheory.Limits.IsZero Y<VAR>f : X ⟶ Y<GOAL>f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<GOAL>CategoryTheory.Limits.IsZero X ↔ 𝟙 X = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Mono 0<GOAL>CategoryTheory.Limits.IsZero X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Epi 0<GOAL>CategoryTheory.Limits.IsZero Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<VAR>h : f = 0<GOAL>CategoryTheory.Limits.IsZero X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<VAR>h : f = 0<GOAL>CategoryTheory.Limits.IsZero Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsSplitMono f<GOAL>CategoryTheory.Limits.IsZero X ↔ f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsSplitEpi f<GOAL>CategoryTheory.Limits.IsZero Y ↔ f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<VAR>i : CategoryTheory.Limits.IsZero Y<GOAL>CategoryTheory.Limits.IsZero X