ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>self : F.ReflectsEffectiveEpiFamilies<VAR>α : Type u<VAR>B : C<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<GOAL>(CategoryTheory.EffectiveEpiFamily (fun a => F.obj (X a)) fun a => F.map (π a)) → CategoryTheory.EffectiveEpiFamily X π
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>F.ReflectsEffectiveEpiFamilies<VAR>α : Type u<VAR>B : C<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>h : CategoryTheory.EffectiveEpiFamily (fun a => F.obj (X a)) fun a => F.map (π a)<GOAL>CategoryTheory.EffectiveEpiFamily X π
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>self : F.ReflectsFiniteEffectiveEpiFamilies<VAR>α : Type<VAR>Finite α<VAR>B : C<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<GOAL>(CategoryTheory.EffectiveEpiFamily (fun a => F.obj (X a)) fun a => F.map (π a)) → CategoryTheory.EffectiveEpiFamily X π
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>F.ReflectsFiniteEffectiveEpiFamilies<VAR>α : Type<VAR>Finite α<VAR>B : C<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>h : CategoryTheory.EffectiveEpiFamily (fun a => F.obj (X a)) fun a => F.map (π a)<GOAL>CategoryTheory.EffectiveEpiFamily X π
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasPullback f f<GOAL>CategoryTheory.Limits.pullback.diagonal f ≫ CategoryTheory.Limits.pullback.fst f f = 𝟙 X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasPullback f f<GOAL>CategoryTheory.Limits.pullback.diagonal f ≫ CategoryTheory.Limits.pullback.snd f f = 𝟙 X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasPullback f f<GOAL>CategoryTheory.IsKernelPair f (CategoryTheory.Limits.pullback.fst f f) (CategoryTheory.Limits.pullback.snd f f)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>U V₁ V₂ : C<VAR>f : X ⟶ Y<VAR>i : U ⟶ Y<VAR>i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i<VAR>i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i<GOAL>CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (i₁ ≫ CategoryTheory.Limits.pullback.snd f i) (i₂ ≫ CategoryTheory.Limits.pullback.snd f i) f f (i₁ ≫ CategoryTheory.Limits.pullback.fst f i) (i₂ ≫ CategoryTheory.Limits.pullback.fst f i) i ⋯ ⋯) ≫ CategoryTheory.Limits.pullback.fst (i₁ ≫ CategoryTheory.Limits.pullback.snd f i) (i₂ ≫ CategoryTheory.Limits.pullback.snd f i) ≫ i₁ ≫ CategoryTheory.Limits.pullback.fst f i = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (i₁ ≫ CategoryTheory.Limits.pullback.snd f i) (i₂ ≫ CategoryTheory.Limits.pullback.snd f i) f f (i₁ ≫ CategoryTheory.Limits.pullback.fst f i) (i₂ ≫ CategoryTheory.Limits.pullback.fst f i) i ⋯ ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>U V₁ V₂ : C<VAR>f : X ⟶ Y<VAR>i : U ⟶ Y<VAR>i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i<VAR>i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i<GOAL>CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (i₁ ≫ CategoryTheory.Limits.pullback.snd f i) (i₂ ≫ CategoryTheory.Limits.pullback.snd f i) f f (i₁ ≫ CategoryTheory.Limits.pullback.fst f i) (i₂ ≫ CategoryTheory.Limits.pullback.fst f i) i ⋯ ⋯) ≫ CategoryTheory.Limits.pullback.snd (i₁ ≫ CategoryTheory.Limits.pullback.snd f i) (i₂ ≫ CategoryTheory.Limits.pullback.snd f i) ≫ i₂ ≫ CategoryTheory.Limits.pullback.fst f i = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (i₁ ≫ CategoryTheory.Limits.pullback.snd f i) (i₂ ≫ CategoryTheory.Limits.pullback.snd f i) f f (i₁ ≫ CategoryTheory.Limits.pullback.fst f i) (i₂ ≫ CategoryTheory.Limits.pullback.fst f i) i ⋯ ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>U V₁ V₂ : C<VAR>f : X ⟶ Y<VAR>i : U ⟶ Y<VAR>i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i<VAR>i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i<VAR>CategoryTheory.Limits.HasPullback i₁ i₂<GOAL>(CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).hom ≫ CategoryTheory.Limits.pullback.fst i₁ i₂ = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (i₁ ≫ CategoryTheory.Limits.pullback.snd f i) (i₂ ≫ CategoryTheory.Limits.pullback.snd f i) f f (i₁ ≫ CategoryTheory.Limits.pullback.fst f i) (i₂ ≫ CategoryTheory.Limits.pullback.fst f i) i ⋯ ⋯) ≫ CategoryTheory.Limits.pullback.fst (i₁ ≫ CategoryTheory.Limits.pullback.snd f i) (i₂ ≫ CategoryTheory.Limits.pullback.snd f i)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>U V₁ V₂ : C<VAR>f : X ⟶ Y<VAR>i : U ⟶ Y<VAR>i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i<VAR>i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i<VAR>CategoryTheory.Limits.HasPullback i₁ i₂<GOAL>(CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).hom ≫ CategoryTheory.Limits.pullback.snd i₁ i₂ = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (i₁ ≫ CategoryTheory.Limits.pullback.snd f i) (i₂ ≫ CategoryTheory.Limits.pullback.snd f i) f f (i₁ ≫ CategoryTheory.Limits.pullback.fst f i) (i₂ ≫ CategoryTheory.Limits.pullback.fst f i) i ⋯ ⋯) ≫ CategoryTheory.Limits.pullback.snd (i₁ ≫ CategoryTheory.Limits.pullback.snd f i) (i₂ ≫ CategoryTheory.Limits.pullback.snd f i)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>U V₁ V₂ : C<VAR>f : X ⟶ Y<VAR>i : U ⟶ Y<VAR>i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i<VAR>i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i<VAR>CategoryTheory.Limits.HasPullback i₁ i₂<GOAL>(CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (i₁ ≫ CategoryTheory.Limits.pullback.snd f i) (i₂ ≫ CategoryTheory.Limits.pullback.snd f i) f f (i₁ ≫ CategoryTheory.Limits.pullback.fst f i) (i₂ ≫ CategoryTheory.Limits.pullback.fst f i) i ⋯ ⋯) = CategoryTheory.Limits.pullback.fst i₁ i₂ ≫ i₁ ≫ CategoryTheory.Limits.pullback.fst f i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>U V₁ V₂ : C<VAR>f : X ⟶ Y<VAR>i : U ⟶ Y<VAR>i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i<VAR>i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i<VAR>CategoryTheory.Limits.HasPullback i₁ i₂<GOAL>(CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (i₁ ≫ CategoryTheory.Limits.pullback.snd f i) (i₂ ≫ CategoryTheory.Limits.pullback.snd f i) f f (i₁ ≫ CategoryTheory.Limits.pullback.fst f i) (i₂ ≫ CategoryTheory.Limits.pullback.fst f i) i ⋯ ⋯) ≫ CategoryTheory.Limits.pullback.fst (i₁ ≫ CategoryTheory.Limits.pullback.snd f i) (i₂ ≫ CategoryTheory.Limits.pullback.snd f i) = CategoryTheory.Limits.pullback.fst i₁ i₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>U V₁ V₂ : C<VAR>f : X ⟶ Y<VAR>i : U ⟶ Y<VAR>i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i<VAR>i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i<VAR>CategoryTheory.Limits.HasPullback i₁ i₂<GOAL>(CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (i₁ ≫ CategoryTheory.Limits.pullback.snd f i) (i₂ ≫ CategoryTheory.Limits.pullback.snd f i) f f (i₁ ≫ CategoryTheory.Limits.pullback.fst f i) (i₂ ≫ CategoryTheory.Limits.pullback.fst f i) i ⋯ ⋯) ≫ CategoryTheory.Limits.pullback.snd (i₁ ≫ CategoryTheory.Limits.pullback.snd f i) (i₂ ≫ CategoryTheory.Limits.pullback.snd f i) = CategoryTheory.Limits.pullback.snd i₁ i₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>U V₁ V₂ : C<VAR>f : X ⟶ Y<VAR>i : U ⟶ Y<VAR>i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i<VAR>i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i<VAR>CategoryTheory.Limits.HasPullback i₁ i₂<GOAL>CategoryTheory.IsPullback (CategoryTheory.Limits.pullback.fst i₁ i₂ ≫ i₁ ≫ CategoryTheory.Limits.pullback.fst f i) (CategoryTheory.Limits.pullback.map i₁ i₂ (i₁ ≫ CategoryTheory.Limits.pullback.snd f i) (i₂ ≫ CategoryTheory.Limits.pullback.snd f i) (𝟙 V₁) (𝟙 V₂) (CategoryTheory.Limits.pullback.snd f i) ⋯ ⋯) (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (i₁ ≫ CategoryTheory.Limits.pullback.snd f i) (i₂ ≫ CategoryTheory.Limits.pullback.snd f i) f f (i₁ ≫ CategoryTheory.Limits.pullback.fst f i) (i₂ ≫ CategoryTheory.Limits.pullback.fst f i) i ⋯ ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>S T : C<VAR>f : X ⟶ T<VAR>g : Y ⟶ T<VAR>i : T ⟶ S<VAR>CategoryTheory.Limits.HasPullback i i<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback (f ≫ i) (g ≫ i)<VAR>CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)<GOAL>(CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).hom ≫ CategoryTheory.Limits.pullback.fst f g = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ CategoryTheory.Limits.pullback.fst (f ≫ i) (g ≫ i)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>S T : C<VAR>f : X ⟶ T<VAR>g : Y ⟶ T<VAR>i : T ⟶ S<VAR>CategoryTheory.Limits.HasPullback i i<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback (f ≫ i) (g ≫ i)<VAR>CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)<GOAL>(CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).hom ≫ CategoryTheory.Limits.pullback.snd f g = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ CategoryTheory.Limits.pullback.snd (f ≫ i) (g ≫ i)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>S T : C<VAR>f : X ⟶ T<VAR>g : Y ⟶ T<VAR>i : T ⟶ S<VAR>CategoryTheory.Limits.HasPullback i i<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback (f ≫ i) (g ≫ i)<VAR>CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)<GOAL>(CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) = CategoryTheory.Limits.pullback.fst f g ≫ f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>S T : C<VAR>f : X ⟶ T<VAR>g : Y ⟶ T<VAR>i : T ⟶ S<VAR>CategoryTheory.Limits.HasPullback i i<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback (f ≫ i) (g ≫ i)<VAR>CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)<GOAL>(CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ CategoryTheory.Limits.pullback.fst (f ≫ i) (g ≫ i) = CategoryTheory.Limits.pullback.fst f g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>S T : C<VAR>f : X ⟶ T<VAR>g : Y ⟶ T<VAR>i : T ⟶ S<VAR>CategoryTheory.Limits.HasPullback i i<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback (f ≫ i) (g ≫ i)<VAR>CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)<GOAL>(CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ CategoryTheory.Limits.pullback.snd (f ≫ i) (g ≫ i) = CategoryTheory.Limits.pullback.snd f g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y Z : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasPullback f f<VAR>CategoryTheory.Limits.HasPullback g g<VAR>CategoryTheory.Limits.HasPullback (f ≫ g) (f ≫ g)<GOAL>CategoryTheory.Limits.pullback.diagonal (f ≫ g) = CategoryTheory.Limits.pullback.diagonal f ≫ (CategoryTheory.Limits.pullbackDiagonalMapIdIso f f g).inv ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal g) (CategoryTheory.Limits.pullback.map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) ⋯ ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>S T : C<VAR>f : X ⟶ T<VAR>g : Y ⟶ T<VAR>i : T ⟶ S<VAR>CategoryTheory.Limits.HasPullback i i<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback (f ≫ i) (g ≫ i)<VAR>CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)<GOAL>CategoryTheory.IsPullback (CategoryTheory.Limits.pullback.fst f g ≫ f) (CategoryTheory.Limits.pullback.map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯) (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd g g ≫ g) f ≫ CategoryTheory.Limits.pullback.fst g g = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g) ≫ CategoryTheory.Limits.pullback.snd f g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd g g ≫ g) f ≫ CategoryTheory.Limits.pullback.snd g g = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g) ≫ CategoryTheory.Limits.pullback.snd f g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd g g ≫ g) f = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g) ≫ CategoryTheory.Limits.pullback.fst f g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g) ≫ CategoryTheory.Limits.pullback.fst f g = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd g g ≫ g) f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g) ≫ CategoryTheory.Limits.pullback.snd f g = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd g g ≫ g) f ≫ CategoryTheory.Limits.pullback.fst g g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g) ≫ CategoryTheory.Limits.pullback.fst f g = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd g g ≫ g) f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g) ≫ CategoryTheory.Limits.pullback.snd f g = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd g g ≫ g) f ≫ CategoryTheory.Limits.pullback.snd g g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.pullback.fst f g) = (CategoryTheory.Limits.pullbackSymmetry f (CategoryTheory.Over.mk g).hom).hom ≫ ((CategoryTheory.Over.pullback f).map (CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.diagonal g) ⋯)).left ≫ (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y S X' Y' S' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S'<VAR>g' : Y' ⟶ S'<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>i₃ : S ⟶ S'<VAR>e₁ : f ≫ i₃ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₂ ≫ g'<VAR>CategoryTheory.Mono i₃<GOAL>(CategoryTheory.Limits.pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).inv = CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (CategoryTheory.Limits.pullback.fst f g) ⋯) (CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (CategoryTheory.Limits.pullback.snd f g) ⋯) ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y S X' Y' S' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S'<VAR>g' : Y' ⟶ S'<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>i₃ : S ⟶ S'<VAR>e₁ : f ≫ i₃ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₂ ≫ g'<VAR>CategoryTheory.Mono i₃<GOAL>(CategoryTheory.Limits.pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).hom = CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f' g') i₁) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂) ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst f' g') i₁) (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f' g') i₁) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂) ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd f' g') i₂) ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y S X' Y' S' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S'<VAR>g' : Y' ⟶ S'<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>i₃ : S ⟶ S'<VAR>e₁ : f ≫ i₃ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₂ ≫ g'<VAR>CategoryTheory.Mono i₃<GOAL>CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂ = (CategoryTheory.Limits.pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).inv ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f' g') i₁) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂) ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y S X' Y' S' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S'<VAR>g' : Y' ⟶ S'<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>i₃ : S ⟶ S'<VAR>e₁ : f ≫ i₃ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₂ ≫ g'<VAR>CategoryTheory.Mono i₃<GOAL>CategoryTheory.IsPullback (CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (CategoryTheory.Limits.pullback.fst f g) ⋯) (CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (CategoryTheory.Limits.pullback.snd f g) ⋯) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f' g') i₁) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>α : Type u_2<VAR>B : C<VAR>X Y : α → C<VAR>f : (a : α) → X a ⟶ B<VAR>g : (a : α) → Y a ⟶ X a<VAR>∀ (a : α), CategoryTheory.Epi (g a)<VAR>CategoryTheory.EffectiveEpiFamily Y fun a => CategoryTheory.CategoryStruct.comp (g a) (f a)<GOAL>CategoryTheory.EffectiveEpiFamily X f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>B X Y : C<VAR>f : X ⟶ B<VAR>g : Y ⟶ X<VAR>CategoryTheory.Epi g<VAR>CategoryTheory.EffectiveEpi (CategoryTheory.CategoryStruct.comp g f)<GOAL>CategoryTheory.EffectiveEpi f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>B B' : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>i : B ⟶ B'<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.CategoryStruct.comp (π a₁) i) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.CategoryStruct.comp (π a₂) i) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)<VAR>Z : C<VAR>a₁ a₂ : α<VAR>g₁ : Z ⟶ X a₁<VAR>g₂ : Z ⟶ X a₂<VAR>hg : CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂)<GOAL>CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>K : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone K<GOAL>((adj.functorialityUnit K).app c).hom = adj.unit.app 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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>K : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone (K.comp F)<GOAL>((adj.functorialityCounit K).app c).hom = adj.counit.app c.pt
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>K : CategoryTheory.Functor J C<VAR>E : CategoryTheory.Functor C D<VAR>E.IsEquivalence<VAR>CategoryTheory.Limits.HasColimit K<GOAL>CategoryTheory.Limits.HasColimit (K.comp E)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>K : CategoryTheory.Functor J C<VAR>E : CategoryTheory.Functor C D<VAR>E.IsEquivalence<VAR>CategoryTheory.Limits.HasColimit (K.comp E)<GOAL>CategoryTheory.Limits.HasColimit K