ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f' : W ⟶ X<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback f' (CategoryTheory.Limits.pullback.fst f g)<VAR>CategoryTheory.Limits.HasPullback (f' ≫ f) g<GOAL>(CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').hom ≫ CategoryTheory.Limits.pullback.fst (f' ≫ f) g = CategoryTheory.Limits.pullback.fst f' (CategoryTheory.Limits.pullback.fst f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f' : W ⟶ X<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback f' (CategoryTheory.Limits.pullback.fst f g)<VAR>CategoryTheory.Limits.HasPullback (f' ≫ f) g<GOAL>(CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').hom ≫ CategoryTheory.Limits.pullback.snd (f' ≫ f) g = CategoryTheory.Limits.pullback.snd f' (CategoryTheory.Limits.pullback.fst f g) ≫ CategoryTheory.Limits.pullback.snd f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f' : W ⟶ X<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback f' (CategoryTheory.Limits.pullback.fst f g)<VAR>CategoryTheory.Limits.HasPullback (f' ≫ f) g<GOAL>(CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv ≫ CategoryTheory.Limits.pullback.fst f' (CategoryTheory.Limits.pullback.fst f g) = CategoryTheory.Limits.pullback.fst (f' ≫ f) g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f' : W ⟶ X<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback f' (CategoryTheory.Limits.pullback.fst f g)<VAR>CategoryTheory.Limits.HasPullback (f' ≫ f) g<GOAL>(CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv ≫ CategoryTheory.Limits.pullback.snd f' (CategoryTheory.Limits.pullback.fst f g) ≫ CategoryTheory.Limits.pullback.snd f g = CategoryTheory.Limits.pullback.snd (f' ≫ f) g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f' : W ⟶ X<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback f' (CategoryTheory.Limits.pullback.fst f g)<VAR>CategoryTheory.Limits.HasPullback (f' ≫ f) g<GOAL>(CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv ≫ CategoryTheory.Limits.pullback.snd f' (CategoryTheory.Limits.pullback.fst f g) ≫ CategoryTheory.Limits.pullback.fst f g = CategoryTheory.Limits.pullback.fst (f' ≫ f) g ≫ f'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>g' : Z ⟶ W<VAR>CategoryTheory.Limits.HasPushout f g<VAR>CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr f g) g'<VAR>CategoryTheory.Limits.HasPushout f (g ≫ g')<GOAL>CategoryTheory.Limits.pushout.inl f (g ≫ g') ≫ (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').inv = CategoryTheory.Limits.pushout.inl f g ≫ CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushout.inr f g) g'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>g' : Z ⟶ W<VAR>CategoryTheory.Limits.HasPushout f g<VAR>CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr f g) g'<VAR>CategoryTheory.Limits.HasPushout f (g ≫ g')<GOAL>CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushout.inr f g) g' ≫ (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom = CategoryTheory.Limits.pushout.inr f (g ≫ g')
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>g' : Z ⟶ W<VAR>CategoryTheory.Limits.HasPushout f g<VAR>CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr f g) g'<VAR>CategoryTheory.Limits.HasPushout f (g ≫ g')<GOAL>CategoryTheory.Limits.pushout.inr f (g ≫ g') ≫ (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').inv = CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushout.inr f g) g'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>g' : Z ⟶ W<VAR>CategoryTheory.Limits.HasPushout f g<VAR>CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr f g) g'<VAR>CategoryTheory.Limits.HasPushout f (g ≫ g')<GOAL>CategoryTheory.Limits.pushout.inl f g ≫ CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushout.inr f g) g' ≫ (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom = CategoryTheory.Limits.pushout.inl f (g ≫ g')
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>g' : Z ⟶ W<VAR>CategoryTheory.Limits.HasPushout f g<VAR>CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr f g) g'<VAR>CategoryTheory.Limits.HasPushout f (g ≫ g')<GOAL>CategoryTheory.Limits.pushout.inr f g ≫ CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushout.inr f g) g' ≫ (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom = g' ≫ CategoryTheory.Limits.pushout.inr f (g ≫ g')
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor C D<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>F : CategoryTheory.Functor J C<VAR>CategoryTheory.Limits.PreservesLimit F G<VAR>c₁ c₂ : CategoryTheory.Limits.Cone F<VAR>t : CategoryTheory.Limits.IsLimit c₁<GOAL>(CategoryTheory.Limits.PreservesLimit.preserves t).lift (G.mapCone c₂) = G.map (t.lift c₂)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor C D<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>F : CategoryTheory.Functor J C<VAR>CategoryTheory.Limits.PreservesLimit F G<VAR>CategoryTheory.Limits.HasLimit F<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesLimitIso G F).hom (CategoryTheory.Limits.limit.π (F.comp G) j) = G.map (CategoryTheory.Limits.limit.π F j)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor C D<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>F : CategoryTheory.Functor J C<VAR>CategoryTheory.Limits.PreservesLimit F G<VAR>CategoryTheory.Limits.HasLimit F<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesLimitIso G F).inv (G.map (CategoryTheory.Limits.limit.π F j)) = CategoryTheory.Limits.limit.π (F.comp G) j
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor C D<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>F : CategoryTheory.Functor J C<VAR>CategoryTheory.Limits.PreservesLimit F G<VAR>CategoryTheory.Limits.HasLimit F<VAR>t : CategoryTheory.Limits.Cone F<GOAL>CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.limit.lift F t)) (CategoryTheory.preservesLimitIso G F).hom = CategoryTheory.Limits.limit.lift (F.comp G) (G.mapCone t)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor C D<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>CategoryTheory.Limits.PreservesLimitsOfShape J G<VAR>CategoryTheory.Limits.HasLimitsOfShape J D<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>X : CategoryTheory.Functor J C<GOAL>(CategoryTheory.preservesLimitNatIso G).inv.app X = (CategoryTheory.preservesLimitIso G X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor C D<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>CategoryTheory.Limits.PreservesLimitsOfShape J G<VAR>CategoryTheory.Limits.HasLimitsOfShape J D<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>X : CategoryTheory.Functor J C<GOAL>(CategoryTheory.preservesLimitNatIso G).hom.app X = (CategoryTheory.preservesLimitIso G X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor C D<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>F : CategoryTheory.Functor J C<VAR>CategoryTheory.Limits.PreservesColimit F G<VAR>c₁ c₂ : CategoryTheory.Limits.Cocone F<VAR>t : CategoryTheory.Limits.IsColimit c₁<GOAL>(CategoryTheory.Limits.PreservesColimit.preserves t).desc (G.mapCocone c₂) = G.map (t.desc c₂)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor C D<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>F : CategoryTheory.Functor J C<VAR>CategoryTheory.Limits.PreservesColimit F G<VAR>CategoryTheory.Limits.HasColimit F<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp G) j) (CategoryTheory.preservesColimitIso G F).inv = G.map (CategoryTheory.Limits.colimit.ι F j)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor C D<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>F : CategoryTheory.Functor J C<VAR>CategoryTheory.Limits.PreservesColimit F G<VAR>CategoryTheory.Limits.HasColimit F<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.colimit.ι F j)) (CategoryTheory.preservesColimitIso G F).hom = CategoryTheory.Limits.colimit.ι (F.comp G) j
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor C D<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>F : CategoryTheory.Functor J C<VAR>CategoryTheory.Limits.PreservesColimit F G<VAR>CategoryTheory.Limits.HasColimit F<VAR>t : CategoryTheory.Limits.Cocone F<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesColimitIso G F).inv (G.map (CategoryTheory.Limits.colimit.desc F t)) = CategoryTheory.Limits.colimit.desc (F.comp G) (G.mapCocone t)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor C D<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>CategoryTheory.Limits.PreservesColimitsOfShape J G<VAR>CategoryTheory.Limits.HasColimitsOfShape J D<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>X : CategoryTheory.Functor J C<GOAL>(CategoryTheory.preservesColimitNatIso G).inv.app X = (CategoryTheory.preservesColimitIso G X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor C D<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>CategoryTheory.Limits.PreservesColimitsOfShape J G<VAR>CategoryTheory.Limits.HasColimitsOfShape J D<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>X : CategoryTheory.Functor J C<GOAL>(CategoryTheory.preservesColimitNatIso G).hom.app X = (CategoryTheory.preservesColimitIso G X).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>CategoryTheory.Limits.HasPullback f₁ f₂<VAR>CategoryTheory.Limits.HasPullback f₃ f₄<VAR>CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f₁ f₂ ≫ f₃) f₄<GOAL>CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.Limits.pullback.fst f₃ f₄ ≫ f₂)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>CategoryTheory.Limits.HasPullback f₁ f₂<VAR>CategoryTheory.Limits.HasPullback f₃ f₄<VAR>CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.Limits.pullback.fst f₃ f₄ ≫ f₂)<GOAL>CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f₁ f₂ ≫ f₃) f₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>CategoryTheory.Limits.HasPullback f₁ f₂<VAR>CategoryTheory.Limits.HasPullback f₃ f₄<VAR>CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f₁ f₂ ≫ f₃) f₄<VAR>CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.Limits.pullback.fst f₃ f₄ ≫ f₂)<GOAL>(CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ CategoryTheory.Limits.pullback.fst f₁ f₂ = CategoryTheory.Limits.pullback.fst f₁ (CategoryTheory.Limits.pullback.fst f₃ f₄ ≫ f₂)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>CategoryTheory.Limits.HasPullback f₁ f₂<VAR>CategoryTheory.Limits.HasPullback f₃ f₄<VAR>CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f₁ f₂ ≫ f₃) f₄<VAR>CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.Limits.pullback.fst f₃ f₄ ≫ f₂)<GOAL>(CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ CategoryTheory.Limits.pullback.fst f₁ (CategoryTheory.Limits.pullback.fst f₃ f₄ ≫ f₂) = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ CategoryTheory.Limits.pullback.fst f₁ f₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>CategoryTheory.Limits.HasPullback f₁ f₂<VAR>CategoryTheory.Limits.HasPullback f₃ f₄<VAR>CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f₁ f₂ ≫ f₃) f₄<VAR>CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.Limits.pullback.fst f₃ f₄ ≫ f₂)<GOAL>(CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ CategoryTheory.Limits.pullback.snd f₁ (CategoryTheory.Limits.pullback.fst f₃ f₄ ≫ f₂) ≫ CategoryTheory.Limits.pullback.fst f₃ f₄ = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ CategoryTheory.Limits.pullback.snd f₁ f₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>CategoryTheory.Limits.HasPullback f₁ f₂<VAR>CategoryTheory.Limits.HasPullback f₃ f₄<VAR>CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f₁ f₂ ≫ f₃) f₄<VAR>CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.Limits.pullback.fst f₃ f₄ ≫ f₂)<GOAL>(CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ CategoryTheory.Limits.pullback.snd f₁ (CategoryTheory.Limits.pullback.fst f₃ f₄ ≫ f₂) ≫ CategoryTheory.Limits.pullback.snd f₃ f₄ = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd f₁ f₂ ≫ f₃) f₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>CategoryTheory.Limits.HasPullback f₁ f₂<VAR>CategoryTheory.Limits.HasPullback f₃ f₄<VAR>CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f₁ f₂ ≫ f₃) f₄<VAR>CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.Limits.pullback.fst f₃ f₄ ≫ f₂)<GOAL>(CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ CategoryTheory.Limits.pullback.snd f₁ f₂ = CategoryTheory.Limits.pullback.snd f₁ (CategoryTheory.Limits.pullback.fst f₃ f₄ ≫ f₂) ≫ CategoryTheory.Limits.pullback.fst f₃ f₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>CategoryTheory.Limits.HasPullback f₁ f₂<VAR>CategoryTheory.Limits.HasPullback f₃ f₄<VAR>CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f₁ f₂ ≫ f₃) f₄<VAR>CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.Limits.pullback.fst f₃ f₄ ≫ f₂)<GOAL>(CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd f₁ f₂ ≫ f₃) f₄ = CategoryTheory.Limits.pullback.snd f₁ (CategoryTheory.Limits.pullback.fst f₃ f₄ ≫ f₂) ≫ CategoryTheory.Limits.pullback.snd f₃ f₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>CategoryTheory.Limits.HasPushout g₁ g₂<VAR>CategoryTheory.Limits.HasPushout g₃ g₄<VAR>CategoryTheory.Limits.HasPushout (g₃ ≫ CategoryTheory.Limits.pushout.inr g₁ g₂) g₄<GOAL>CategoryTheory.Limits.HasPushout g₁ (g₂ ≫ CategoryTheory.Limits.pushout.inl g₃ g₄)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>CategoryTheory.Limits.HasPushout g₁ g₂<VAR>CategoryTheory.Limits.HasPushout g₃ g₄<VAR>CategoryTheory.Limits.HasPushout g₁ (g₂ ≫ CategoryTheory.Limits.pushout.inl g₃ g₄)<GOAL>CategoryTheory.Limits.HasPushout (g₃ ≫ CategoryTheory.Limits.pushout.inr g₁ g₂) g₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>CategoryTheory.Limits.HasPushout g₁ g₂<VAR>CategoryTheory.Limits.HasPushout g₃ g₄<VAR>CategoryTheory.Limits.HasPushout (g₃ ≫ CategoryTheory.Limits.pushout.inr g₁ g₂) g₄<VAR>CategoryTheory.Limits.HasPushout g₁ (g₂ ≫ CategoryTheory.Limits.pushout.inl g₃ g₄)<GOAL>CategoryTheory.Limits.pushout.inl g₁ g₂ ≫ CategoryTheory.Limits.pushout.inl (g₃ ≫ CategoryTheory.Limits.pushout.inr g₁ g₂) g₄ ≫ (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom = CategoryTheory.Limits.pushout.inl g₁ (g₂ ≫ CategoryTheory.Limits.pushout.inl g₃ g₄)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>CategoryTheory.Limits.HasPushout g₁ g₂<VAR>CategoryTheory.Limits.HasPushout g₃ g₄<VAR>CategoryTheory.Limits.HasPushout (g₃ ≫ CategoryTheory.Limits.pushout.inr g₁ g₂) g₄<VAR>CategoryTheory.Limits.HasPushout g₁ (g₂ ≫ CategoryTheory.Limits.pushout.inl g₃ g₄)<GOAL>CategoryTheory.Limits.pushout.inr g₁ g₂ ≫ CategoryTheory.Limits.pushout.inl (g₃ ≫ CategoryTheory.Limits.pushout.inr g₁ g₂) g₄ ≫ (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom = CategoryTheory.Limits.pushout.inl g₃ g₄ ≫ CategoryTheory.Limits.pushout.inr g₁ (g₂ ≫ CategoryTheory.Limits.pushout.inl g₃ g₄)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>CategoryTheory.Limits.HasPushout g₁ g₂<VAR>CategoryTheory.Limits.HasPushout g₃ g₄<VAR>CategoryTheory.Limits.HasPushout (g₃ ≫ CategoryTheory.Limits.pushout.inr g₁ g₂) g₄<VAR>CategoryTheory.Limits.HasPushout g₁ (g₂ ≫ CategoryTheory.Limits.pushout.inl g₃ g₄)<GOAL>CategoryTheory.Limits.pushout.inr g₃ g₄ ≫ CategoryTheory.Limits.pushout.inr g₁ (g₂ ≫ CategoryTheory.Limits.pushout.inl g₃ g₄) ≫ (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv = CategoryTheory.Limits.pushout.inr (g₃ ≫ CategoryTheory.Limits.pushout.inr g₁ g₂) g₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>CategoryTheory.Limits.HasPushout g₁ g₂<VAR>CategoryTheory.Limits.HasPushout g₃ g₄<VAR>CategoryTheory.Limits.HasPushout (g₃ ≫ CategoryTheory.Limits.pushout.inr g₁ g₂) g₄<VAR>CategoryTheory.Limits.HasPushout g₁ (g₂ ≫ CategoryTheory.Limits.pushout.inl g₃ g₄)<GOAL>CategoryTheory.Limits.pushout.inl g₁ (g₂ ≫ CategoryTheory.Limits.pushout.inl g₃ g₄) ≫ (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv = CategoryTheory.Limits.pushout.inl g₁ g₂ ≫ CategoryTheory.Limits.pushout.inl (g₃ ≫ CategoryTheory.Limits.pushout.inr g₁ g₂) g₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>CategoryTheory.Limits.HasPushout g₁ g₂<VAR>CategoryTheory.Limits.HasPushout g₃ g₄<VAR>CategoryTheory.Limits.HasPushout (g₃ ≫ CategoryTheory.Limits.pushout.inr g₁ g₂) g₄<VAR>CategoryTheory.Limits.HasPushout g₁ (g₂ ≫ CategoryTheory.Limits.pushout.inl g₃ g₄)<GOAL>CategoryTheory.Limits.pushout.inl g₃ g₄ ≫ CategoryTheory.Limits.pushout.inr g₁ (g₂ ≫ CategoryTheory.Limits.pushout.inl g₃ g₄) ≫ (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv = CategoryTheory.Limits.pushout.inr g₁ g₂ ≫ CategoryTheory.Limits.pushout.inl (g₃ ≫ CategoryTheory.Limits.pushout.inr g₁ g₂) g₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>CategoryTheory.Limits.HasPushout g₁ g₂<VAR>CategoryTheory.Limits.HasPushout g₃ g₄<VAR>CategoryTheory.Limits.HasPushout (g₃ ≫ CategoryTheory.Limits.pushout.inr g₁ g₂) g₄<VAR>CategoryTheory.Limits.HasPushout g₁ (g₂ ≫ CategoryTheory.Limits.pushout.inl g₃ g₄)<GOAL>CategoryTheory.Limits.pushout.inr (g₃ ≫ CategoryTheory.Limits.pushout.inr g₁ g₂) g₄ ≫ (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom = CategoryTheory.Limits.pushout.inr g₃ g₄ ≫ CategoryTheory.Limits.pushout.inr g₁ (g₂ ≫ CategoryTheory.Limits.pushout.inl g₃ g₄)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>sq : CategoryTheory.Square C<VAR>h : sq.IsPullback<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan sq.f₂₄ sq.f₃₄) F<GOAL>(sq.map F).IsPullback
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>sq : CategoryTheory.Square C<VAR>h : sq.IsPushout<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span sq.f₁₂ sq.f₁₃) F<GOAL>(sq.map F).IsPushout
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.IsPullback ↔ ∀ (X : Cᵒᵖ), (sq.map (CategoryTheory.coyoneda.obj X)).IsPullback
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.IsPushout ↔ ∀ (X : C), (sq.op.map (CategoryTheory.yoneda.obj X)).IsPullback
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : CategoryTheory.Limits.Cone F<VAR>self : CategoryTheory.Limits.IsLimit t<VAR>s : CategoryTheory.Limits.Cone F<VAR>m : s.pt ⟶ t.pt<GOAL>(∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = self.lift s
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : CategoryTheory.Limits.Cone F<VAR>self : CategoryTheory.Limits.IsLimit t<VAR>s : CategoryTheory.Limits.Cone F<VAR>j : J<GOAL>self.lift s ≫ t.π.app j = s.π.app j
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F G : J ⥤ C<VAR>c : CategoryTheory.Limits.Cone F<VAR>d : CategoryTheory.Limits.Cone G<VAR>hd : CategoryTheory.Limits.IsLimit d<VAR>α : F ⟶ G<VAR>j : J<GOAL>CategoryTheory.Limits.IsLimit.map c hd α ≫ d.π.app j = c.π.app j ≫ α.app j
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>c : CategoryTheory.Limits.Cone F<VAR>t : CategoryTheory.Limits.IsLimit c<GOAL>t.lift c = 𝟙 c.pt
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : CategoryTheory.Limits.Cone F<VAR>h : CategoryTheory.Limits.IsLimit t<VAR>s : CategoryTheory.Limits.Cone F<GOAL>(h.liftConeMorphism s).hom = h.lift s
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>s t : CategoryTheory.Limits.Cone F<VAR>h : CategoryTheory.Limits.IsLimit t<VAR>f f' : s ⟶ t<GOAL>f = f'
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : CategoryTheory.Limits.Cone F<VAR>h : CategoryTheory.Limits.IsLimit t<VAR>s : CategoryTheory.Limits.Cone F<GOAL>∃! l, ∀ (j : J), l ≫ t.π.app j = s.π.app j
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : CategoryTheory.Limits.Cone F<VAR>lift : (s : CategoryTheory.Limits.Cone F) → s ⟶ t<VAR>uniq : ∀ (s : CategoryTheory.Limits.Cone F) (m : s ⟶ t), m = lift s<VAR>s : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.IsLimit.mkConeMorphism lift uniq).lift s = (lift s).hom