ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)<GOAL>CategoryTheory.Limits.PushoutCocone.inl (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.span f g)) = CategoryTheory.Limits.pushout.inl f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)<GOAL>CategoryTheory.Limits.PushoutCocone.inr (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.span f g)) = CategoryTheory.Limits.pushout.inr 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>CategoryTheory.Limits.HasPullback f g<VAR>h : W ⟶ X<VAR>k : W ⟶ Y<VAR>w : h ≫ f = k ≫ g<GOAL>CategoryTheory.Limits.pullback.lift h k w ≫ CategoryTheory.Limits.pullback.fst f g = h
<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>CategoryTheory.Limits.HasPullback f g<VAR>h : W ⟶ X<VAR>k : W ⟶ Y<VAR>w : h ≫ f = k ≫ g<GOAL>CategoryTheory.Limits.pullback.lift h k w ≫ CategoryTheory.Limits.pullback.snd f g = k
<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>CategoryTheory.Limits.HasPushout f g<VAR>h : Y ⟶ W<VAR>k : Z ⟶ W<VAR>w : f ≫ h = g ≫ k<GOAL>CategoryTheory.Limits.pushout.inl f g ≫ CategoryTheory.Limits.pushout.desc h k w = h
<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>CategoryTheory.Limits.HasPushout f g<VAR>h : Y ⟶ W<VAR>k : Z ⟶ W<VAR>w : f ≫ h = g ≫ k<GOAL>CategoryTheory.Limits.pushout.inr f g ≫ CategoryTheory.Limits.pushout.desc h k w = k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasPullback f g<GOAL>CategoryTheory.Limits.pullback.fst f g ≫ f = CategoryTheory.Limits.pullback.snd f g ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.Limits.HasPushout f g<GOAL>f ≫ CategoryTheory.Limits.pushout.inl f g = g ≫ CategoryTheory.Limits.pushout.inr f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasPullback f g<VAR>W : C<VAR>k l : W ⟶ CategoryTheory.Limits.pullback f g<VAR>h₀ : k ≫ CategoryTheory.Limits.pullback.fst f g = l ≫ CategoryTheory.Limits.pullback.fst f g<VAR>h₁ : k ≫ CategoryTheory.Limits.pullback.snd f g = l ≫ CategoryTheory.Limits.pullback.snd f g<GOAL>k = l
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.Limits.HasPushout f g<VAR>W : C<VAR>k l : CategoryTheory.Limits.pushout f g ⟶ W<VAR>h₀ : CategoryTheory.Limits.pushout.inl f g ≫ k = CategoryTheory.Limits.pushout.inl f g ≫ l<VAR>h₁ : CategoryTheory.Limits.pushout.inr f g ≫ k = CategoryTheory.Limits.pushout.inr f g ≫ l<GOAL>k = l
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' X'' Y'' Z'' : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f' : X' ⟶ Z'<VAR>g' : Y' ⟶ Z'<VAR>f'' : X'' ⟶ Z''<VAR>g'' : Y'' ⟶ Z''<VAR>i₁ : X ⟶ X'<VAR>j₁ : X' ⟶ X''<VAR>i₂ : Y ⟶ Y'<VAR>j₂ : Y' ⟶ Y''<VAR>i₃ : Z ⟶ Z'<VAR>j₃ : Z' ⟶ Z''<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback f' g'<VAR>CategoryTheory.Limits.HasPullback f'' g''<VAR>e₁ : f ≫ i₃ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₂ ≫ g'<VAR>e₃ : f' ≫ j₃ = j₁ ≫ f''<VAR>e₄ : g' ≫ j₃ = j₂ ≫ g''<GOAL>CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂ ≫ CategoryTheory.Limits.pullback.map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄ = CategoryTheory.Limits.pullback.map f g f'' g'' (i₁ ≫ j₁) (i₂ ≫ j₂) (i₃ ≫ j₃) ⋯ ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasPullback f g<GOAL>CategoryTheory.Limits.pullback.map f g f g (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯ = 𝟙 (CategoryTheory.Limits.pullback f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' X'' Y'' Z'' : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>f' : X' ⟶ Y'<VAR>g' : X' ⟶ Z'<VAR>f'' : X'' ⟶ Y''<VAR>g'' : X'' ⟶ Z''<VAR>i₁ : X ⟶ X'<VAR>j₁ : X' ⟶ X''<VAR>i₂ : Y ⟶ Y'<VAR>j₂ : Y' ⟶ Y''<VAR>i₃ : Z ⟶ Z'<VAR>j₃ : Z' ⟶ Z''<VAR>CategoryTheory.Limits.HasPushout f g<VAR>CategoryTheory.Limits.HasPushout f' g'<VAR>CategoryTheory.Limits.HasPushout f'' g''<VAR>e₁ : f ≫ i₂ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₁ ≫ g'<VAR>e₃ : f' ≫ j₂ = j₁ ≫ f''<VAR>e₄ : g' ≫ j₃ = j₁ ≫ g''<GOAL>CategoryTheory.Limits.pushout.map f g f' g' i₂ i₃ i₁ e₁ e₂ ≫ CategoryTheory.Limits.pushout.map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄ = CategoryTheory.Limits.pushout.map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁) ⋯ ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.Limits.HasPushout f g<GOAL>CategoryTheory.Limits.pushout.map f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯ = 𝟙 (CategoryTheory.Limits.pushout f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f₁ f₂ : X ⟶ Z<VAR>g₁ g₂ : Y ⟶ Z<VAR>h₁ : f₁ = f₂<VAR>h₂ : g₁ = g₂<VAR>CategoryTheory.Limits.HasPullback f₁ g₁<VAR>CategoryTheory.Limits.HasPullback f₂ g₂<GOAL>(CategoryTheory.Limits.pullback.congrHom h₁ h₂).hom = CategoryTheory.Limits.pullback.map f₁ g₁ f₂ g₂ (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f₁ f₂ : X ⟶ Z<VAR>g₁ g₂ : Y ⟶ Z<VAR>h₁ : f₁ = f₂<VAR>h₂ : g₁ = g₂<VAR>CategoryTheory.Limits.HasPullback f₁ g₁<VAR>CategoryTheory.Limits.HasPullback f₂ g₂<GOAL>(CategoryTheory.Limits.pullback.congrHom h₁ h₂).inv = CategoryTheory.Limits.pullback.map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y S T S' : C<VAR>f : X ⟶ T<VAR>g : Y ⟶ T<VAR>i : T ⟶ S<VAR>i' : S ⟶ S'<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback (f ≫ i) (g ≫ i)<VAR>CategoryTheory.Limits.HasPullback (f ≫ i ≫ i') (g ≫ i ≫ i')<VAR>CategoryTheory.Limits.HasPullback ((f ≫ i) ≫ i') ((g ≫ i) ≫ i')<GOAL>CategoryTheory.Limits.pullback.mapDesc f g (i ≫ i') = CategoryTheory.Limits.pullback.mapDesc f g i ≫ CategoryTheory.Limits.pullback.mapDesc (f ≫ i) (g ≫ i) i' ≫ (CategoryTheory.Limits.pullback.congrHom ⋯ ⋯).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f₁ f₂ : X ⟶ Y<VAR>g₁ g₂ : X ⟶ Z<VAR>h₁ : f₁ = f₂<VAR>h₂ : g₁ = g₂<VAR>CategoryTheory.Limits.HasPushout f₁ g₁<VAR>CategoryTheory.Limits.HasPushout f₂ g₂<GOAL>(CategoryTheory.Limits.pushout.congrHom h₁ h₂).hom = CategoryTheory.Limits.pushout.map f₁ g₁ f₂ g₂ (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f₁ f₂ : X ⟶ Y<VAR>g₁ g₂ : X ⟶ Z<VAR>h₁ : f₁ = f₂<VAR>h₂ : g₁ = g₂<VAR>CategoryTheory.Limits.HasPushout f₁ g₁<VAR>CategoryTheory.Limits.HasPushout f₂ g₂<GOAL>(CategoryTheory.Limits.pushout.congrHom h₁ h₂).inv = CategoryTheory.Limits.pushout.map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y S T S' : C<VAR>f : T ⟶ X<VAR>g : T ⟶ Y<VAR>i : S ⟶ T<VAR>i' : S' ⟶ S<VAR>CategoryTheory.Limits.HasPushout f g<VAR>CategoryTheory.Limits.HasPushout (i ≫ f) (i ≫ g)<VAR>CategoryTheory.Limits.HasPushout (i' ≫ i ≫ f) (i' ≫ i ≫ g)<VAR>CategoryTheory.Limits.HasPushout ((i' ≫ i) ≫ f) ((i' ≫ i) ≫ g)<GOAL>CategoryTheory.Limits.pushout.mapLift f g (i' ≫ i) = (CategoryTheory.Limits.pushout.congrHom ⋯ ⋯).hom ≫ CategoryTheory.Limits.pushout.mapLift (i ≫ f) (i ≫ g) i' ≫ CategoryTheory.Limits.pushout.mapLift f g i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback (G.map f) (G.map g)<GOAL>CategoryTheory.Limits.pullbackComparison G f g ≫ CategoryTheory.Limits.pullback.fst (G.map f) (G.map g) = G.map (CategoryTheory.Limits.pullback.fst f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback (G.map f) (G.map g)<GOAL>CategoryTheory.Limits.pullbackComparison G f g ≫ CategoryTheory.Limits.pullback.snd (G.map f) (G.map g) = G.map (CategoryTheory.Limits.pullback.snd f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback (G.map f) (G.map g)<VAR>W : C<VAR>h : W ⟶ X<VAR>k : W ⟶ Y<VAR>w : h ≫ f = k ≫ g<GOAL>G.map (CategoryTheory.Limits.pullback.lift h k w) ≫ CategoryTheory.Limits.pullbackComparison G f g = CategoryTheory.Limits.pullback.lift (G.map h) (G.map k) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.Limits.HasPushout f g<VAR>CategoryTheory.Limits.HasPushout (G.map f) (G.map g)<GOAL>CategoryTheory.Limits.pushout.inl (G.map f) (G.map g) ≫ CategoryTheory.Limits.pushoutComparison G f g = G.map (CategoryTheory.Limits.pushout.inl f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.Limits.HasPushout f g<VAR>CategoryTheory.Limits.HasPushout (G.map f) (G.map g)<GOAL>CategoryTheory.Limits.pushout.inr (G.map f) (G.map g) ≫ CategoryTheory.Limits.pushoutComparison G f g = G.map (CategoryTheory.Limits.pushout.inr f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.Limits.HasPushout f g<VAR>CategoryTheory.Limits.HasPushout (G.map f) (G.map g)<VAR>W : C<VAR>h : Y ⟶ W<VAR>k : Z ⟶ W<VAR>w : f ≫ h = g ≫ k<GOAL>CategoryTheory.Limits.pushoutComparison G f g ≫ G.map (CategoryTheory.Limits.pushout.desc h k w) = CategoryTheory.Limits.pushout.desc (G.map h) (G.map k) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasPullback f g<GOAL>CategoryTheory.Limits.HasPullback g f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasPullback f g<GOAL>(CategoryTheory.Limits.pullbackSymmetry f g).hom ≫ CategoryTheory.Limits.pullback.fst g f = CategoryTheory.Limits.pullback.snd f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasPullback f g<GOAL>(CategoryTheory.Limits.pullbackSymmetry f g).hom ≫ CategoryTheory.Limits.pullback.snd g f = CategoryTheory.Limits.pullback.fst f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasPullback f g<GOAL>(CategoryTheory.Limits.pullbackSymmetry f g).inv ≫ CategoryTheory.Limits.pullback.fst f g = CategoryTheory.Limits.pullback.snd g f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasPullback f g<GOAL>(CategoryTheory.Limits.pullbackSymmetry f g).inv ≫ CategoryTheory.Limits.pullback.snd f g = CategoryTheory.Limits.pullback.fst g f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.Limits.HasPushout f g<GOAL>CategoryTheory.Limits.HasPushout g f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.Limits.HasPushout f g<GOAL>CategoryTheory.Limits.pushout.inl f g ≫ (CategoryTheory.Limits.pushoutSymmetry f g).hom = CategoryTheory.Limits.pushout.inr g f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.Limits.HasPushout f g<GOAL>CategoryTheory.Limits.pushout.inr f g ≫ (CategoryTheory.Limits.pushoutSymmetry f g).hom = CategoryTheory.Limits.pushout.inl g f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.Limits.HasPushout f g<GOAL>CategoryTheory.Limits.pushout.inl g f ≫ (CategoryTheory.Limits.pushoutSymmetry f g).inv = CategoryTheory.Limits.pushout.inr f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.Limits.HasPushout f g<GOAL>CategoryTheory.Limits.pushout.inr g f ≫ (CategoryTheory.Limits.pushoutSymmetry f g).inv = CategoryTheory.Limits.pushout.inl f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}, CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)<GOAL>CategoryTheory.Limits.HasPullbacks C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}, CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)<GOAL>CategoryTheory.Limits.HasPushouts C
<GOAL>∀ {X Y : (CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair)ᵒᵖ} (f : X ⟶ Y), CategoryTheory.Limits.walkingSpanOpEquiv.functor.map f = (CategoryTheory.Limits.widePushoutShapeOpMap CategoryTheory.Limits.WalkingPair (Opposite.unop Y) (Opposite.unop X) f.unop).unop
<VAR>X : CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair<GOAL>CategoryTheory.Limits.walkingSpanOpEquiv.inverse.obj X = Opposite.op X
<VAR>X : (CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair)ᵒᵖ<GOAL>CategoryTheory.Limits.walkingSpanOpEquiv.unitIso.hom.app X = 𝟙 X
<VAR>X₁ X₂ : CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair<GOAL>∀ (a : X₁ ⟶ X₂), CategoryTheory.Limits.walkingSpanOpEquiv.inverse.map a = CategoryTheory.Limits.widePullbackShapeOpMap CategoryTheory.Limits.WalkingPair X₁ X₂ a
<VAR>X : CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair<GOAL>CategoryTheory.Limits.walkingSpanOpEquiv.counitIso.hom.app X = 𝟙 X
<VAR>X : (CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair)ᵒᵖ<GOAL>CategoryTheory.Limits.walkingSpanOpEquiv.functor.obj X = Opposite.unop X
<VAR>X : (CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair)ᵒᵖ<GOAL>CategoryTheory.Limits.walkingSpanOpEquiv.unitIso.inv.app X = 𝟙 X
<VAR>X : CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair<GOAL>CategoryTheory.Limits.walkingSpanOpEquiv.counitIso.inv.app X = 𝟙 X
<GOAL>∀ {X Y : (CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair)ᵒᵖ} (f : X ⟶ Y), CategoryTheory.Limits.walkingCospanOpEquiv.functor.map f = (CategoryTheory.Limits.widePullbackShapeOpMap CategoryTheory.Limits.WalkingPair (Opposite.unop Y) (Opposite.unop X) f.unop).unop
<VAR>X : (CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair)ᵒᵖ<GOAL>CategoryTheory.Limits.walkingCospanOpEquiv.unitIso.inv.app X = 𝟙 X
<VAR>X : CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair<GOAL>CategoryTheory.Limits.walkingCospanOpEquiv.inverse.obj X = Opposite.op X
<VAR>X : (CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair)ᵒᵖ<GOAL>CategoryTheory.Limits.walkingCospanOpEquiv.unitIso.hom.app X = 𝟙 X
<VAR>X : CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair<GOAL>CategoryTheory.Limits.walkingCospanOpEquiv.counitIso.hom.app X = 𝟙 X
<VAR>X Y : CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair<GOAL>∀ (a : X ⟶ Y), CategoryTheory.Limits.walkingCospanOpEquiv.inverse.map a = CategoryTheory.Limits.widePushoutShapeOpMap CategoryTheory.Limits.WalkingPair X Y a
<VAR>X : (CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair)ᵒᵖ<GOAL>CategoryTheory.Limits.walkingCospanOpEquiv.functor.obj X = Opposite.unop X
<VAR>X : CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair<GOAL>CategoryTheory.Limits.walkingCospanOpEquiv.counitIso.inv.app X = 𝟙 X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ Cᵒᵖ<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>s : CategoryTheory.Limits.Cone F.leftOp<GOAL>(CategoryTheory.Limits.isLimitConeLeftOpOfCocone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeLeftOp s)).unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ Cᵒᵖ<VAR>c : CategoryTheory.Limits.Cone F<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>s : CategoryTheory.Limits.Cocone F.leftOp<GOAL>(CategoryTheory.Limits.isColimitCoconeLeftOpOfCone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeLeftOp s)).unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>s : CategoryTheory.Limits.Cone F.rightOp<GOAL>(CategoryTheory.Limits.isLimitConeRightOpOfCocone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeRightOp s)).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ C<VAR>c : CategoryTheory.Limits.Cone F<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>s : CategoryTheory.Limits.Cocone F.rightOp<GOAL>(CategoryTheory.Limits.isColimitCoconeRightOpOfCone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeRightOp s)).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ Cᵒᵖ<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>s : CategoryTheory.Limits.Cone F.unop<GOAL>(CategoryTheory.Limits.isLimitConeUnopOfCocone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeUnop s)).unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ Cᵒᵖ<VAR>c : CategoryTheory.Limits.Cone F<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>s : CategoryTheory.Limits.Cocone F.unop<GOAL>(CategoryTheory.Limits.isColimitCoconeUnopOfCone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeUnop s)).unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ Cᵒᵖ<VAR>c : CategoryTheory.Limits.Cocone F.leftOp<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>s : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.isLimitConeOfCoconeLeftOp F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeLeftOpOfCone s)).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ Cᵒᵖ<VAR>c : CategoryTheory.Limits.Cone F.leftOp<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>s : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.isColimitCoconeOfConeLeftOp F hc).desc s = (hc.lift (CategoryTheory.Limits.coneLeftOpOfCocone s)).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ C<VAR>c : CategoryTheory.Limits.Cocone F.rightOp<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>s : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.isLimitConeOfCoconeRightOp F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeRightOpOfCone s)).unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ C<VAR>c : CategoryTheory.Limits.Cone F.rightOp<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>s : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.isColimitCoconeOfConeRightOp F hc).desc s = (hc.lift (CategoryTheory.Limits.coneRightOpOfCocone s)).unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ Cᵒᵖ<VAR>c : CategoryTheory.Limits.Cocone F.unop<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>s : CategoryTheory.Limits.Cone F<GOAL>(CategoryTheory.Limits.isLimitConeOfCoconeUnop F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeUnopOfCone s)).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ Cᵒᵖ<VAR>c : CategoryTheory.Limits.Cone F.unop<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>s : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.isColimitConeOfCoconeUnop F hc).desc s = (hc.lift (CategoryTheory.Limits.coneUnopOfCocone s)).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ Cᵒᵖ<VAR>CategoryTheory.Limits.HasColimit F.leftOp<GOAL>CategoryTheory.Limits.HasLimit F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F.op<GOAL>CategoryTheory.Limits.HasLimit F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<GOAL>CategoryTheory.Limits.HasLimit F.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>CategoryTheory.Limits.HasColimitsOfShape Jᵒᵖ C<GOAL>CategoryTheory.Limits.HasLimitsOfShape J Cᵒᵖ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>CategoryTheory.Limits.HasColimitsOfShape Jᵒᵖ Cᵒᵖ<GOAL>CategoryTheory.Limits.HasLimitsOfShape J C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasColimits Cᵒᵖ<GOAL>CategoryTheory.Limits.HasLimits C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ<GOAL>CategoryTheory.Limits.HasCofilteredLimitsOfSize.{v₂, u₂, v₁, u₁} C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ Cᵒᵖ<VAR>CategoryTheory.Limits.HasLimit F.leftOp<GOAL>CategoryTheory.Limits.HasColimit F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasLimit F.op<GOAL>CategoryTheory.Limits.HasColimit F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasLimit F<GOAL>CategoryTheory.Limits.HasColimit F.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ Cᵒᵖ<GOAL>CategoryTheory.Limits.HasColimitsOfShape J C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasLimits Cᵒᵖ<GOAL>CategoryTheory.Limits.HasColimits C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasCofilteredLimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ<GOAL>CategoryTheory.Limits.HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : Type v₂<VAR>CategoryTheory.Limits.HasProductsOfShape X Cᵒᵖ<GOAL>CategoryTheory.Limits.HasCoproductsOfShape X C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : Type v₂<VAR>CategoryTheory.Limits.HasCoproductsOfShape X Cᵒᵖ<GOAL>CategoryTheory.Limits.HasProductsOfShape X C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasCoproducts Cᵒᵖ<GOAL>CategoryTheory.Limits.HasProducts C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasProducts Cᵒᵖ<GOAL>CategoryTheory.Limits.HasCoproducts C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasFiniteProducts Cᵒᵖ<GOAL>CategoryTheory.Limits.HasFiniteCoproducts C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasFiniteCoproducts Cᵒᵖ<GOAL>CategoryTheory.Limits.HasFiniteProducts C