ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WidePullbackShape J ⥤ C<VAR>X : C<VAR>f : X ⟶ F.obj none<VAR>π : (j : J) → X ⟶ F.obj (some j)<VAR>w : ∀ (j : J), π j ≫ F.map (CategoryTheory.Limits.WidePullbackShape.Hom.term j) = f<GOAL>(CategoryTheory.Limits.WidePullbackShape.mkCone f π w).pt = X
<VAR>J : Type w<VAR>X : CategoryTheory.Limits.WidePushoutShape J<GOAL>CategoryTheory.Limits.WidePushoutShape.Hom.id X = 𝟙 X
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → B ⟶ objs j<GOAL>∀ {X Y : CategoryTheory.Limits.WidePushoutShape J} (f : X ⟶ Y), (CategoryTheory.Limits.WidePushoutShape.wideSpan B objs arrows).map f = CategoryTheory.Limits.WidePushoutShape.Hom.casesOn (motive := fun a a_1 t => X = a → Y = a_1 → HEq f t → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y)) f (fun X_1 h => Eq.ndrec (motive := fun X_2 => Y = X_2 → HEq f (CategoryTheory.Limits.WidePushoutShape.Hom.id X_2) → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y)) (fun h => Eq.ndrec (motive := fun {Y} => (f : X ⟶ Y) → HEq f (CategoryTheory.Limits.WidePushoutShape.Hom.id X) → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y)) (fun f h => 𝟙 ((fun j => Option.casesOn j B objs) X)) ⋯ f) h) (fun j h => Eq.ndrec (motive := fun {X} => (f : X ⟶ Y) → Y = some j → HEq f (CategoryTheory.Limits.WidePushoutShape.Hom.init j) → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y)) (fun f h => Eq.ndrec (motive := fun {Y} => (f : none ⟶ Y) → HEq f (CategoryTheory.Limits.WidePushoutShape.Hom.init j) → ((fun j => Option.casesOn j B objs) none ⟶ (fun j => Option.casesOn j B objs) Y)) (fun f h => arrows j) ⋯ f) ⋯ f) ⋯ ⋯ ⋯
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → B ⟶ objs j<VAR>j : CategoryTheory.Limits.WidePushoutShape J<GOAL>(CategoryTheory.Limits.WidePushoutShape.wideSpan B objs arrows).obj j = Option.casesOn j B objs
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WidePushoutShape J ⥤ C<VAR>X : C<VAR>f : F.obj none ⟶ X<VAR>ι : (j : J) → F.obj (some j) ⟶ X<VAR>w : ∀ (j : J), F.map (CategoryTheory.Limits.WidePushoutShape.Hom.init j) ≫ ι j = f<VAR>j : CategoryTheory.Limits.WidePushoutShape J<GOAL>(CategoryTheory.Limits.WidePushoutShape.mkCocone f ι w).ι.app j = match j with | none => f | some j => ι j
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WidePushoutShape J ⥤ C<VAR>X : C<VAR>f : F.obj none ⟶ X<VAR>ι : (j : J) → F.obj (some j) ⟶ X<VAR>w : ∀ (j : J), F.map (CategoryTheory.Limits.WidePushoutShape.Hom.init j) ≫ ι j = f<GOAL>(CategoryTheory.Limits.WidePushoutShape.mkCocone f ι w).pt = X
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → objs j ⟶ B<VAR>CategoryTheory.Limits.HasWidePullback B objs arrows<VAR>j : J<GOAL>CategoryTheory.Limits.WidePullback.π arrows j ≫ arrows j = CategoryTheory.Limits.WidePullback.base arrows
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → objs j ⟶ B<VAR>CategoryTheory.Limits.HasWidePullback B objs arrows<VAR>X : C<VAR>f : X ⟶ B<VAR>fs : (j : J) → X ⟶ objs j<VAR>w : ∀ (j : J), fs j ≫ arrows j = f<VAR>j : J<GOAL>CategoryTheory.Limits.WidePullback.lift f fs w ≫ CategoryTheory.Limits.WidePullback.π arrows j = fs j
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → objs j ⟶ B<VAR>CategoryTheory.Limits.HasWidePullback B objs arrows<VAR>X : C<VAR>f : X ⟶ B<VAR>fs : (j : J) → X ⟶ objs j<VAR>w : ∀ (j : J), fs j ≫ arrows j = f<GOAL>CategoryTheory.Limits.WidePullback.lift f fs w ≫ CategoryTheory.Limits.WidePullback.base arrows = f
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → objs j ⟶ B<VAR>CategoryTheory.Limits.HasWidePullback B objs arrows<VAR>X : C<VAR>f : X ⟶ B<VAR>fs : (j : J) → X ⟶ objs j<VAR>w : ∀ (j : J), fs j ≫ arrows j = f<VAR>g : X ⟶ CategoryTheory.Limits.widePullback B objs arrows<GOAL>(∀ (j : J), g ≫ CategoryTheory.Limits.WidePullback.π arrows j = fs j) → g ≫ CategoryTheory.Limits.WidePullback.base arrows = f → g = CategoryTheory.Limits.WidePullback.lift f fs w
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → objs j ⟶ B<VAR>CategoryTheory.Limits.HasWidePullback B objs arrows<VAR>X : C<VAR>g : X ⟶ CategoryTheory.Limits.widePullback B objs arrows<GOAL>g = CategoryTheory.Limits.WidePullback.lift (g ≫ CategoryTheory.Limits.WidePullback.base arrows) (fun j => g ≫ CategoryTheory.Limits.WidePullback.π arrows j) ⋯
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → objs j ⟶ B<VAR>CategoryTheory.Limits.HasWidePullback B objs arrows<VAR>X : C<VAR>g1 g2 : X ⟶ CategoryTheory.Limits.widePullback B objs arrows<GOAL>(∀ (j : J), g1 ≫ CategoryTheory.Limits.WidePullback.π arrows j = g2 ≫ CategoryTheory.Limits.WidePullback.π arrows j) → g1 ≫ CategoryTheory.Limits.WidePullback.base arrows = g2 ≫ CategoryTheory.Limits.WidePullback.base arrows → g1 = g2
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → B ⟶ objs j<VAR>CategoryTheory.Limits.HasWidePushout B objs arrows<VAR>j : J<GOAL>arrows j ≫ CategoryTheory.Limits.WidePushout.ι arrows j = CategoryTheory.Limits.WidePushout.head arrows
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → B ⟶ objs j<VAR>CategoryTheory.Limits.HasWidePushout B objs arrows<VAR>X : C<VAR>f : B ⟶ X<VAR>fs : (j : J) → objs j ⟶ X<VAR>w : ∀ (j : J), arrows j ≫ fs j = f<VAR>j : J<GOAL>CategoryTheory.Limits.WidePushout.ι arrows j ≫ CategoryTheory.Limits.WidePushout.desc f fs w = fs j
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → B ⟶ objs j<VAR>CategoryTheory.Limits.HasWidePushout B objs arrows<VAR>X : C<VAR>f : B ⟶ X<VAR>fs : (j : J) → objs j ⟶ X<VAR>w : ∀ (j : J), arrows j ≫ fs j = f<GOAL>CategoryTheory.Limits.WidePushout.head arrows ≫ CategoryTheory.Limits.WidePushout.desc f fs w = f
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → B ⟶ objs j<VAR>CategoryTheory.Limits.HasWidePushout B objs arrows<VAR>X : C<VAR>f : B ⟶ X<VAR>fs : (j : J) → objs j ⟶ X<VAR>w : ∀ (j : J), arrows j ≫ fs j = f<VAR>g : CategoryTheory.Limits.widePushout B objs arrows ⟶ X<GOAL>(∀ (j : J), CategoryTheory.Limits.WidePushout.ι arrows j ≫ g = fs j) → CategoryTheory.Limits.WidePushout.head arrows ≫ g = f → g = CategoryTheory.Limits.WidePushout.desc f fs w
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → B ⟶ objs j<VAR>CategoryTheory.Limits.HasWidePushout B objs arrows<VAR>X : C<VAR>g : CategoryTheory.Limits.widePushout B objs arrows ⟶ X<GOAL>g = CategoryTheory.Limits.WidePushout.desc (CategoryTheory.Limits.WidePushout.head arrows ≫ g) (fun j => CategoryTheory.Limits.WidePushout.ι arrows j ≫ g) ⋯
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → B ⟶ objs j<VAR>CategoryTheory.Limits.HasWidePushout B objs arrows<VAR>X : C<VAR>g1 g2 : CategoryTheory.Limits.widePushout B objs arrows ⟶ X<GOAL>(∀ (j : J), CategoryTheory.Limits.WidePushout.ι arrows j ≫ g1 = CategoryTheory.Limits.WidePushout.ι arrows j ≫ g2) → CategoryTheory.Limits.WidePushout.head arrows ≫ g1 = CategoryTheory.Limits.WidePushout.head arrows ≫ g2 → g1 = g2
<VAR>J : Type w<VAR>X₁ X₂ : CategoryTheory.Limits.WidePullbackShape J<GOAL>∀ (a : X₁ ⟶ X₂), (CategoryTheory.Limits.widePullbackShapeOp J).map a = CategoryTheory.Limits.widePullbackShapeOpMap J X₁ X₂ a
<VAR>J : Type w<VAR>X : CategoryTheory.Limits.WidePullbackShape J<GOAL>(CategoryTheory.Limits.widePullbackShapeOp J).obj X = Opposite.op X
<VAR>J : Type w<VAR>X Y : CategoryTheory.Limits.WidePushoutShape J<GOAL>∀ (a : X ⟶ Y), (CategoryTheory.Limits.widePushoutShapeOp J).map a = CategoryTheory.Limits.widePushoutShapeOpMap J X Y a
<VAR>J : Type w<VAR>X : CategoryTheory.Limits.WidePushoutShape J<GOAL>(CategoryTheory.Limits.widePushoutShapeOp J).obj X = Opposite.op X
<VAR>J : Type w<VAR>X : (CategoryTheory.Limits.WidePullbackShape J)ᵒᵖ<GOAL>(CategoryTheory.Limits.widePullbackShapeUnop J).obj X = Opposite.unop X
<VAR>J : Type w<GOAL>∀ {X Y : (CategoryTheory.Limits.WidePullbackShape J)ᵒᵖ} (f : X ⟶ Y), (CategoryTheory.Limits.widePullbackShapeUnop J).map f = (CategoryTheory.Limits.widePullbackShapeOpMap J (Opposite.unop Y) (Opposite.unop X) f.unop).unop
<VAR>J : Type w<GOAL>∀ {X Y : (CategoryTheory.Limits.WidePushoutShape J)ᵒᵖ} (f : X ⟶ Y), (CategoryTheory.Limits.widePushoutShapeUnop J).map f = (CategoryTheory.Limits.widePushoutShapeOpMap J (Opposite.unop Y) (Opposite.unop X) f.unop).unop
<VAR>J : Type w<VAR>X : (CategoryTheory.Limits.WidePushoutShape J)ᵒᵖ<GOAL>(CategoryTheory.Limits.widePushoutShapeUnop J).obj X = Opposite.unop X
<VAR>J : Type w<GOAL>(CategoryTheory.Limits.widePushoutShapeOpEquiv J).functor = CategoryTheory.Limits.widePushoutShapeUnop J
<VAR>J : Type w<GOAL>(CategoryTheory.Limits.widePushoutShapeOpEquiv J).unitIso = (CategoryTheory.Limits.widePushoutShapeOpUnop J).symm
<VAR>J : Type w<GOAL>(CategoryTheory.Limits.widePushoutShapeOpEquiv J).inverse = CategoryTheory.Limits.widePullbackShapeOp J
<VAR>J : Type w<GOAL>(CategoryTheory.Limits.widePushoutShapeOpEquiv J).counitIso = CategoryTheory.Limits.widePullbackShapeUnopOp J
<VAR>J : Type w<GOAL>(CategoryTheory.Limits.widePullbackShapeOpEquiv J).unitIso = (CategoryTheory.Limits.widePullbackShapeOpUnop J).symm
<VAR>J : Type w<GOAL>(CategoryTheory.Limits.widePullbackShapeOpEquiv J).functor = CategoryTheory.Limits.widePullbackShapeUnop J
<VAR>J : Type w<GOAL>(CategoryTheory.Limits.widePullbackShapeOpEquiv J).inverse = CategoryTheory.Limits.widePushoutShapeOp J
<VAR>J : Type w<GOAL>(CategoryTheory.Limits.widePullbackShapeOpEquiv J).counitIso = CategoryTheory.Limits.widePushoutShapeUnopOp J
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasWidePushouts C<GOAL>CategoryTheory.Limits.HasWidePushouts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasWidePullbacks C<GOAL>CategoryTheory.Limits.HasWidePullbacks C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>J : C<VAR>hP : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveYonedaObj J)<GOAL>CategoryTheory.Injective J
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G<VAR>CategoryTheory.Limits.HasPullback f g<GOAL>CategoryTheory.Limits.HasPullback (G.map f) (G.map g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback (G.map f) (G.map g)<GOAL>(CategoryTheory.Limits.PreservesPullback.iso G f g).hom = CategoryTheory.Limits.pullbackComparison G f g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback (G.map f) (G.map g)<GOAL>(CategoryTheory.Limits.PreservesPullback.iso G f g).hom ≫ 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>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback (G.map f) (G.map g)<GOAL>(CategoryTheory.Limits.PreservesPullback.iso G f g).hom ≫ 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>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback (G.map f) (G.map g)<GOAL>(CategoryTheory.Limits.PreservesPullback.iso G f g).inv ≫ G.map (CategoryTheory.Limits.pullback.fst f g) = CategoryTheory.Limits.pullback.fst (G.map f) (G.map g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G<VAR>CategoryTheory.Limits.HasPullback f g<VAR>CategoryTheory.Limits.HasPullback (G.map f) (G.map g)<GOAL>(CategoryTheory.Limits.PreservesPullback.iso G f g).inv ≫ G.map (CategoryTheory.Limits.pullback.snd f g) = CategoryTheory.Limits.pullback.snd (G.map f) (G.map g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>W X Y : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G<VAR>CategoryTheory.Limits.HasPushout f g<GOAL>CategoryTheory.Limits.HasPushout (G.map f) (G.map g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>W X Y : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G<VAR>CategoryTheory.Limits.HasPushout f g<VAR>CategoryTheory.Limits.HasPushout (G.map f) (G.map g)<GOAL>(CategoryTheory.Limits.PreservesPushout.iso G f g).hom = CategoryTheory.Limits.pushoutComparison G f g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>W X Y : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G<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.PreservesPushout.iso G f g).hom = G.map (CategoryTheory.Limits.pushout.inl f g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>W X Y : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G<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.PreservesPushout.iso G f g).hom = G.map (CategoryTheory.Limits.pushout.inr f g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>W X Y : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G<VAR>CategoryTheory.Limits.HasPushout f g<VAR>CategoryTheory.Limits.HasPushout (G.map f) (G.map g)<GOAL>G.map (CategoryTheory.Limits.pushout.inl f g) ≫ (CategoryTheory.Limits.PreservesPushout.iso G f g).inv = CategoryTheory.Limits.pushout.inl (G.map f) (G.map g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>W X Y : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G<VAR>CategoryTheory.Limits.HasPushout f g<VAR>CategoryTheory.Limits.HasPushout (G.map f) (G.map g)<GOAL>G.map (CategoryTheory.Limits.pushout.inr f g) ≫ (CategoryTheory.Limits.PreservesPushout.iso G f g).inv = CategoryTheory.Limits.pushout.inr (G.map f) (G.map g)
<VAR>L R : Type w<VAR>fst snd : R → L<VAR>X : CategoryTheory.Limits.WalkingMulticospan fst snd<GOAL>CategoryTheory.Limits.WalkingMulticospan.Hom.id X = CategoryTheory.CategoryStruct.id X
<VAR>L R : Type w<VAR>fst snd : R → L<VAR>X Y Z : CategoryTheory.Limits.WalkingMulticospan fst snd<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.Limits.WalkingMulticospan.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g
<VAR>L R : Type v<VAR>fst snd : L → R<VAR>X : CategoryTheory.Limits.WalkingMultispan fst snd<GOAL>CategoryTheory.Limits.WalkingMultispan.Hom.id X = CategoryTheory.CategoryStruct.id X
<VAR>L R : Type v<VAR>fst snd : L → R<VAR>X Y Z : CategoryTheory.Limits.WalkingMultispan fst snd<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.Limits.WalkingMultispan.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>x y : CategoryTheory.Limits.WalkingMulticospan I.fstTo I.sndTo<VAR>f : x ⟶ y<GOAL>I.multicospan.map f = match x, y, f with | x, .(x), CategoryTheory.Limits.WalkingMulticospan.Hom.id .(x) => CategoryTheory.CategoryStruct.id ((fun x => match x with | CategoryTheory.Limits.WalkingMulticospan.left a => I.left a | CategoryTheory.Limits.WalkingMulticospan.right b => I.right b) x) | .(CategoryTheory.Limits.WalkingMulticospan.left (I.fstTo b)), .(CategoryTheory.Limits.WalkingMulticospan.right b), CategoryTheory.Limits.WalkingMulticospan.Hom.fst b => I.fst b | .(CategoryTheory.Limits.WalkingMulticospan.left (I.sndTo b)), .(CategoryTheory.Limits.WalkingMulticospan.right b), CategoryTheory.Limits.WalkingMulticospan.Hom.snd b => I.snd b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>x : CategoryTheory.Limits.WalkingMulticospan I.fstTo I.sndTo<GOAL>I.multicospan.obj x = match x with | CategoryTheory.Limits.WalkingMulticospan.left a => I.left a | CategoryTheory.Limits.WalkingMulticospan.right b => I.right b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<VAR>b : I.R<GOAL>CategoryTheory.CategoryStruct.comp I.fstPiMap (CategoryTheory.Limits.Pi.π I.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (I.fstTo b)) (I.fst b)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<VAR>b : I.R<GOAL>CategoryTheory.CategoryStruct.comp I.sndPiMap (CategoryTheory.Limits.Pi.π I.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (I.sndTo b)) (I.snd b)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<VAR>x : CategoryTheory.Limits.WalkingParallelPair<GOAL>I.parallelPairDiagram.obj x = match x with | CategoryTheory.Limits.WalkingParallelPair.zero => ∏ᶜ I.left | CategoryTheory.Limits.WalkingParallelPair.one => ∏ᶜ I.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>CategoryTheory.Limits.HasProduct I.left<VAR>CategoryTheory.Limits.HasProduct I.right<GOAL>∀ {X Y : CategoryTheory.Limits.WalkingParallelPair} (h : X ⟶ Y), I.parallelPairDiagram.map h = match X, Y, h with | x, .(x), CategoryTheory.Limits.WalkingParallelPairHom.id .(x) => CategoryTheory.CategoryStruct.id (match x with | CategoryTheory.Limits.WalkingParallelPair.zero => ∏ᶜ I.left | CategoryTheory.Limits.WalkingParallelPair.one => ∏ᶜ I.right) | .(CategoryTheory.Limits.WalkingParallelPair.zero), .(CategoryTheory.Limits.WalkingParallelPair.one), CategoryTheory.Limits.WalkingParallelPairHom.left => I.fstPiMap | .(CategoryTheory.Limits.WalkingParallelPair.zero), .(CategoryTheory.Limits.WalkingParallelPair.one), CategoryTheory.Limits.WalkingParallelPairHom.right => I.sndPiMap
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>a : I.L<GOAL>I.multispan.obj (CategoryTheory.Limits.WalkingMultispan.left a) = I.left a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>b : I.R<GOAL>I.multispan.obj (CategoryTheory.Limits.WalkingMultispan.right b) = I.right b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>a : I.L<GOAL>I.multispan.map (CategoryTheory.Limits.WalkingMultispan.Hom.fst a) = I.fst a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>a : I.L<GOAL>I.multispan.map (CategoryTheory.Limits.WalkingMultispan.Hom.snd a) = I.snd a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasCoproduct I.left<VAR>CategoryTheory.Limits.HasCoproduct I.right<VAR>b : I.L<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.left b) I.fstSigmaMap = CategoryTheory.CategoryStruct.comp (I.fst b) (CategoryTheory.Limits.Sigma.ι I.right (I.fstFrom b))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MultispanIndex C<VAR>CategoryTheory.Limits.HasCoproduct I.left<VAR>CategoryTheory.Limits.HasCoproduct I.right<VAR>b : I.L<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.left b) I.sndSigmaMap = CategoryTheory.CategoryStruct.comp (I.snd b) (CategoryTheory.Limits.Sigma.ι I.right (I.sndFrom b))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>K : CategoryTheory.Limits.Multifork I<VAR>a : I.L<GOAL>K.π.app (CategoryTheory.Limits.WalkingMulticospan.left a) = K.ι a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>K : CategoryTheory.Limits.Multifork I<VAR>b : I.R<GOAL>K.π.app (CategoryTheory.Limits.WalkingMulticospan.right b) = CategoryTheory.CategoryStruct.comp (K.ι (I.fstTo b)) (I.fst b)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>K : CategoryTheory.Limits.Multifork I<VAR>b : I.R<GOAL>K.π.app (CategoryTheory.Limits.WalkingMulticospan.right b) = CategoryTheory.CategoryStruct.comp (K.ι (I.sndTo b)) (I.snd b)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>K₁ K₂ : CategoryTheory.Limits.Multifork I<VAR>f : K₁ ⟶ K₂<VAR>j : I.L<GOAL>CategoryTheory.CategoryStruct.comp f.hom (K₂.ι j) = K₁.ι j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>P : C<VAR>ι : (a : I.L) → P ⟶ I.left a<VAR>w : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (ι (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (ι (I.sndTo b)) (I.snd b)<GOAL>(CategoryTheory.Limits.Multifork.ofι I P ι w).pt = P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : CategoryTheory.Limits.MulticospanIndex C<VAR>P : C<VAR>ι : (a : I.L) → P ⟶ I.left a<VAR>w : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (ι (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (ι (I.sndTo b)) (I.snd b)<VAR>x : CategoryTheory.Limits.WalkingMulticospan I.fstTo I.sndTo<GOAL>(CategoryTheory.Limits.Multifork.ofι I P ι w).π.app x = match x with | CategoryTheory.Limits.WalkingMulticospan.left a => ι a | CategoryTheory.Limits.WalkingMulticospan.right b => CategoryTheory.CategoryStruct.comp (ι (I.fstTo b)) (I.fst b)