ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>α : Type u_1<VAR>Z : α → C<VAR>c : CategoryTheory.Limits.Cofan Z<VAR>f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>hf : CategoryTheory.Limits.IsLimit f<VAR>b : α<GOAL>(CategoryTheory.Limits.opCoproductIsoProduct' hc hf).inv ≫ (c.inj b).op = f.proj b
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>α : Type u_1<VAR>Z : α → C<VAR>c c' : CategoryTheory.Limits.Cofan Z<VAR>f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>hc' : CategoryTheory.Limits.IsColimit c'<VAR>hf : CategoryTheory.Limits.IsLimit f<GOAL>(CategoryTheory.Limits.opCoproductIsoProduct' hc hf).hom ≫ (CategoryTheory.Limits.opCoproductIsoProduct' hc' hf).inv = (hc.coconePointUniqueUpToIso hc').op.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>α : Type u_1<VAR>Z : α → C<VAR>CategoryTheory.Limits.HasCoproduct Z<VAR>b : α<GOAL>(CategoryTheory.Limits.opCoproductIsoProduct Z).inv ≫ (CategoryTheory.Limits.Sigma.ι Z b).op = CategoryTheory.Limits.Pi.π (fun x => Opposite.op (Z x)) b
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>α : Type u_1<VAR>Z : α → C<VAR>c : CategoryTheory.Limits.Cofan Z<VAR>f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>hf : CategoryTheory.Limits.IsLimit f<VAR>c' : CategoryTheory.Limits.Cofan Z<GOAL>(hc.desc c').op ≫ (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).hom = hf.lift c'.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>α : Type u_1<VAR>Z : α → C<VAR>CategoryTheory.Limits.HasCoproduct Z<VAR>X : C<VAR>π : (a : α) → Z a ⟶ X<GOAL>(CategoryTheory.Limits.Sigma.desc π).op ≫ (CategoryTheory.Limits.opCoproductIsoProduct Z).hom = CategoryTheory.Limits.Pi.lift fun a => (π a).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>α : Type u_1<VAR>Z : α → C<VAR>f : CategoryTheory.Limits.Fan Z<VAR>c : CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)<VAR>hf : CategoryTheory.Limits.IsLimit f<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>b : α<GOAL>(f.proj b).op ≫ (CategoryTheory.Limits.opProductIsoCoproduct' hf hc).hom = c.inj b
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>α : Type u_1<VAR>Z : α → C<VAR>f f' : CategoryTheory.Limits.Fan Z<VAR>c : CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)<VAR>hf : CategoryTheory.Limits.IsLimit f<VAR>hf' : CategoryTheory.Limits.IsLimit f'<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.Limits.opProductIsoCoproduct' hf hc).hom ≫ (CategoryTheory.Limits.opProductIsoCoproduct' hf' hc).inv = (hf.conePointUniqueUpToIso hf').op.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>α : Type u_1<VAR>Z : α → C<VAR>CategoryTheory.Limits.HasProduct Z<VAR>b : α<GOAL>(CategoryTheory.Limits.Pi.π Z b).op ≫ (CategoryTheory.Limits.opProductIsoCoproduct Z).hom = CategoryTheory.Limits.Sigma.ι (fun x => Opposite.op (Z x)) b
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>α : Type u_1<VAR>Z : α → C<VAR>f : CategoryTheory.Limits.Fan Z<VAR>c : CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)<VAR>hf : CategoryTheory.Limits.IsLimit f<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>f' : CategoryTheory.Limits.Fan Z<GOAL>(CategoryTheory.Limits.opProductIsoCoproduct' hf hc).inv ≫ (hf.lift f').op = hc.desc f'.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>α : Type u_1<VAR>Z : α → C<VAR>CategoryTheory.Limits.HasProduct Z<VAR>X : C<VAR>π : (a : α) → X ⟶ Z a<GOAL>(CategoryTheory.Limits.opProductIsoCoproduct Z).inv ≫ (CategoryTheory.Limits.Pi.lift π).op = CategoryTheory.Limits.Sigma.desc fun a => (π a).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingSpan), (CategoryTheory.Limits.spanOp f g).inv.app X_1 = (Option.rec (CategoryTheory.Iso.refl (Opposite.op Z)) (fun val => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op X)) (CategoryTheory.Iso.refl (Opposite.op Y)) val) X_1).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingSpan), (CategoryTheory.Limits.spanOp f g).hom.app X_1 = (Option.rec (CategoryTheory.Iso.refl (Opposite.op Z)) (fun val => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op X)) (CategoryTheory.Iso.refl (Opposite.op Y)) val) X_1).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingCospanᵒᵖ), (CategoryTheory.Limits.opCospan f g).hom.app X_1 = (Option.rec (CategoryTheory.Iso.refl (Opposite.op Z)) (fun val => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op X)) (CategoryTheory.Iso.refl (Opposite.op Y)) val) (Opposite.unop X_1)).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingCospanᵒᵖ), (CategoryTheory.Limits.opCospan f g).inv.app X_1 = (Option.rec (CategoryTheory.Iso.refl (Opposite.op Z)) (fun val => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op X)) (CategoryTheory.Iso.refl (Opposite.op Y)) val) (Opposite.unop X_1)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingCospan), (CategoryTheory.Limits.cospanOp f g).hom.app X_1 = (Option.rec (CategoryTheory.Iso.refl (Opposite.op X)) (fun val => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op Y)) (CategoryTheory.Iso.refl (Opposite.op Z)) val) X_1).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingCospan), (CategoryTheory.Limits.cospanOp f g).inv.app X_1 = (Option.rec (CategoryTheory.Iso.refl (Opposite.op X)) (fun val => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op Y)) (CategoryTheory.Iso.refl (Opposite.op Z)) val) X_1).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingSpanᵒᵖ), (CategoryTheory.Limits.opSpan f g).hom.app X_1 = (Option.rec (CategoryTheory.Iso.refl (Opposite.op X)) (fun val => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op Y)) (CategoryTheory.Iso.refl (Opposite.op Z)) val) (Opposite.unop X_1)).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingSpanᵒᵖ), (CategoryTheory.Limits.opSpan f g).inv.app X_1 = (Option.rec (CategoryTheory.Iso.refl (Opposite.op X)) (fun val => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op Y)) (CategoryTheory.Iso.refl (Opposite.op Z)) val) (Opposite.unop X_1)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>c : CategoryTheory.Limits.PushoutCocone f g<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingCospan), c.unop.π.app X_1 = (c.ι.app X_1).unop ≫ (Option.rec (CategoryTheory.Iso.refl X) (fun val => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl Y) (CategoryTheory.Iso.refl Z) val) X_1).inv.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>c : CategoryTheory.Limits.PushoutCocone f g<GOAL>c.unop.pt = Opposite.unop c.pt
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>c : CategoryTheory.Limits.PushoutCocone f g<GOAL>c.unop.fst = c.inl.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>c : CategoryTheory.Limits.PushoutCocone f g<GOAL>c.unop.snd = c.inr.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>c : CategoryTheory.Limits.PushoutCocone f g<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingCospan), c.op.π.app X_1 = (c.ι.app X_1).op ≫ (Option.rec (CategoryTheory.Iso.refl (Opposite.op X)) (fun val => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op Y)) (CategoryTheory.Iso.refl (Opposite.op Z)) val) X_1).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>c : CategoryTheory.Limits.PushoutCocone f g<GOAL>c.op.pt = Opposite.op c.pt
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>c : CategoryTheory.Limits.PushoutCocone f g<GOAL>c.op.fst = c.inl.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>c : CategoryTheory.Limits.PushoutCocone f g<GOAL>c.op.snd = c.inr.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>c : CategoryTheory.Limits.PullbackCone f g<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingSpan), c.unop.ι.app X_1 = (Option.rec (CategoryTheory.Iso.refl Z) (fun val => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl X) (CategoryTheory.Iso.refl Y) val) X_1).hom.unop ≫ (c.π.app X_1).unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>c : CategoryTheory.Limits.PullbackCone f g<GOAL>c.unop.pt = Opposite.unop c.pt
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>c : CategoryTheory.Limits.PullbackCone f g<GOAL>c.unop.inl = c.fst.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>c : CategoryTheory.Limits.PullbackCone f g<GOAL>c.unop.inr = c.snd.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>c : CategoryTheory.Limits.PullbackCone f g<GOAL>c.op.pt = Opposite.op c.pt
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>c : CategoryTheory.Limits.PullbackCone f g<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingSpan), c.op.ι.app X_1 = (Option.rec (CategoryTheory.Iso.refl (Opposite.op Z)) (fun val => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op X)) (CategoryTheory.Iso.refl (Opposite.op Y)) val) X_1).hom ≫ (c.π.app X_1).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>c : CategoryTheory.Limits.PullbackCone f g<GOAL>c.op.inl = c.fst.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>c : CategoryTheory.Limits.PullbackCone f g<GOAL>c.op.inr = c.snd.op
<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>CategoryTheory.Limits.HasPushout f.op g.op<GOAL>(CategoryTheory.Limits.pullbackIsoUnopPushout f g).inv ≫ CategoryTheory.Limits.pullback.fst f g = (CategoryTheory.Limits.pushout.inl f.op g.op).unop
<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>CategoryTheory.Limits.HasPushout f.op g.op<GOAL>(CategoryTheory.Limits.pullbackIsoUnopPushout f g).inv ≫ CategoryTheory.Limits.pullback.snd f g = (CategoryTheory.Limits.pushout.inr f.op g.op).unop
<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>CategoryTheory.Limits.HasPushout f.op g.op<GOAL>CategoryTheory.Limits.pushout.inl f.op g.op ≫ (CategoryTheory.Limits.pullbackIsoUnopPushout f g).hom.op = (CategoryTheory.Limits.pullback.fst f g).op
<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>CategoryTheory.Limits.HasPushout f.op g.op<GOAL>CategoryTheory.Limits.pushout.inr f.op g.op ≫ (CategoryTheory.Limits.pullbackIsoUnopPushout f g).hom.op = (CategoryTheory.Limits.pullback.snd f g).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : X ⟶ Y<VAR>CategoryTheory.Limits.HasPushout f g<VAR>CategoryTheory.Limits.HasPullback f.op g.op<GOAL>CategoryTheory.Limits.pushout.inl f g ≫ (CategoryTheory.Limits.pushoutIsoUnopPullback f g).hom = (CategoryTheory.Limits.pullback.fst f.op g.op).unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : X ⟶ Y<VAR>CategoryTheory.Limits.HasPushout f g<VAR>CategoryTheory.Limits.HasPullback f.op g.op<GOAL>CategoryTheory.Limits.pushout.inr f g ≫ (CategoryTheory.Limits.pushoutIsoUnopPullback f g).hom = (CategoryTheory.Limits.pullback.snd f.op g.op).unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : X ⟶ Y<VAR>CategoryTheory.Limits.HasPushout f g<VAR>CategoryTheory.Limits.HasPullback f.op g.op<GOAL>(CategoryTheory.Limits.pushoutIsoUnopPullback f g).inv.op ≫ CategoryTheory.Limits.pullback.fst f.op g.op = (CategoryTheory.Limits.pushout.inl f g).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : X ⟶ Y<VAR>CategoryTheory.Limits.HasPushout f g<VAR>CategoryTheory.Limits.HasPullback f.op g.op<GOAL>(CategoryTheory.Limits.pushoutIsoUnopPullback f g).inv.op ≫ CategoryTheory.Limits.pullback.snd f.op g.op = (CategoryTheory.Limits.pushout.inr f g).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.cospan f g).obj CategoryTheory.Limits.WalkingCospan.left = X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<GOAL>(CategoryTheory.Limits.span f g).obj CategoryTheory.Limits.WalkingSpan.left = Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.cospan f g).obj CategoryTheory.Limits.WalkingCospan.right = Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<GOAL>(CategoryTheory.Limits.span f g).obj CategoryTheory.Limits.WalkingSpan.right = Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.cospan f g).obj CategoryTheory.Limits.WalkingCospan.one = Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<GOAL>(CategoryTheory.Limits.span f g).obj CategoryTheory.Limits.WalkingSpan.zero = X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.cospan f g).map CategoryTheory.Limits.WalkingCospan.Hom.inl = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<GOAL>(CategoryTheory.Limits.span f g).map CategoryTheory.Limits.WalkingSpan.Hom.fst = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.cospan f g).map CategoryTheory.Limits.WalkingCospan.Hom.inr = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<GOAL>(CategoryTheory.Limits.span f g).map CategoryTheory.Limits.WalkingSpan.Hom.snd = 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>w : CategoryTheory.Limits.WalkingCospan<GOAL>(CategoryTheory.Limits.cospan f g).map (CategoryTheory.Limits.WalkingCospan.Hom.id w) = 𝟙 ((CategoryTheory.Limits.cospan f g).obj w)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>w : CategoryTheory.Limits.WalkingSpan<GOAL>(CategoryTheory.Limits.span f g).map (CategoryTheory.Limits.WalkingSpan.Hom.id w) = 𝟙 ((CategoryTheory.Limits.span f g).obj w)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WalkingCospan ⥤ C<VAR>X : CategoryTheory.Limits.WalkingCospan<GOAL>(CategoryTheory.Limits.diagramIsoCospan F).inv.app X = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WalkingCospan ⥤ C<VAR>X : CategoryTheory.Limits.WalkingCospan<GOAL>(CategoryTheory.Limits.diagramIsoCospan F).hom.app X = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WalkingSpan ⥤ C<VAR>X : CategoryTheory.Limits.WalkingSpan<GOAL>(CategoryTheory.Limits.diagramIsoSpan F).inv.app X = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WalkingSpan ⥤ C<VAR>X : CategoryTheory.Limits.WalkingSpan<GOAL>(CategoryTheory.Limits.diagramIsoSpan F).hom.app X = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.cospanCompIso F f g).app CategoryTheory.Limits.WalkingCospan.left = CategoryTheory.Iso.refl ((CategoryTheory.Limits.cospan f g ⋙ F).obj CategoryTheory.Limits.WalkingCospan.left)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.cospanCompIso F f g).app CategoryTheory.Limits.WalkingCospan.right = CategoryTheory.Iso.refl ((CategoryTheory.Limits.cospan f g ⋙ F).obj CategoryTheory.Limits.WalkingCospan.right)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.cospanCompIso F f g).app CategoryTheory.Limits.WalkingCospan.one = CategoryTheory.Iso.refl ((CategoryTheory.Limits.cospan f g ⋙ F).obj CategoryTheory.Limits.WalkingCospan.one)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.cospanCompIso F f g).hom.app CategoryTheory.Limits.WalkingCospan.left = 𝟙 ((CategoryTheory.Limits.cospan f g ⋙ F).obj CategoryTheory.Limits.WalkingCospan.left)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.cospanCompIso F f g).hom.app CategoryTheory.Limits.WalkingCospan.right = 𝟙 ((CategoryTheory.Limits.cospan f g ⋙ F).obj CategoryTheory.Limits.WalkingCospan.right)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.cospanCompIso F f g).hom.app CategoryTheory.Limits.WalkingCospan.one = 𝟙 ((CategoryTheory.Limits.cospan f g ⋙ F).obj CategoryTheory.Limits.WalkingCospan.one)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.cospanCompIso F f g).inv.app CategoryTheory.Limits.WalkingCospan.left = 𝟙 ((CategoryTheory.Limits.cospan (F.map f) (F.map g)).obj CategoryTheory.Limits.WalkingCospan.left)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.cospanCompIso F f g).inv.app CategoryTheory.Limits.WalkingCospan.right = 𝟙 ((CategoryTheory.Limits.cospan (F.map f) (F.map g)).obj CategoryTheory.Limits.WalkingCospan.right)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Limits.cospanCompIso F f g).inv.app CategoryTheory.Limits.WalkingCospan.one = 𝟙 ((CategoryTheory.Limits.cospan (F.map f) (F.map g)).obj CategoryTheory.Limits.WalkingCospan.one)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<GOAL>(CategoryTheory.Limits.spanCompIso F f g).app CategoryTheory.Limits.WalkingSpan.left = CategoryTheory.Iso.refl ((CategoryTheory.Limits.span f g ⋙ F).obj CategoryTheory.Limits.WalkingSpan.left)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<GOAL>(CategoryTheory.Limits.spanCompIso F f g).app CategoryTheory.Limits.WalkingSpan.right = CategoryTheory.Iso.refl ((CategoryTheory.Limits.span f g ⋙ F).obj CategoryTheory.Limits.WalkingSpan.right)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<GOAL>(CategoryTheory.Limits.spanCompIso F f g).app CategoryTheory.Limits.WalkingSpan.zero = CategoryTheory.Iso.refl ((CategoryTheory.Limits.span f g ⋙ F).obj CategoryTheory.Limits.WalkingSpan.zero)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<GOAL>(CategoryTheory.Limits.spanCompIso F f g).hom.app CategoryTheory.Limits.WalkingSpan.left = 𝟙 ((CategoryTheory.Limits.span f g ⋙ F).obj CategoryTheory.Limits.WalkingSpan.left)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<GOAL>(CategoryTheory.Limits.spanCompIso F f g).hom.app CategoryTheory.Limits.WalkingSpan.right = 𝟙 ((CategoryTheory.Limits.span f g ⋙ F).obj CategoryTheory.Limits.WalkingSpan.right)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<GOAL>(CategoryTheory.Limits.spanCompIso F f g).hom.app CategoryTheory.Limits.WalkingSpan.zero = 𝟙 ((CategoryTheory.Limits.span f g ⋙ F).obj CategoryTheory.Limits.WalkingSpan.zero)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<GOAL>(CategoryTheory.Limits.spanCompIso F f g).inv.app CategoryTheory.Limits.WalkingSpan.left = 𝟙 ((CategoryTheory.Limits.span (F.map f) (F.map g)).obj CategoryTheory.Limits.WalkingSpan.left)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<GOAL>(CategoryTheory.Limits.spanCompIso F f g).inv.app CategoryTheory.Limits.WalkingSpan.right = 𝟙 ((CategoryTheory.Limits.span (F.map f) (F.map g)).obj CategoryTheory.Limits.WalkingSpan.right)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<GOAL>(CategoryTheory.Limits.spanCompIso F f g).inv.app CategoryTheory.Limits.WalkingSpan.zero = 𝟙 ((CategoryTheory.Limits.span (F.map f) (F.map g)).obj CategoryTheory.Limits.WalkingSpan.zero)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' : C<VAR>iX : X ≅ X'<VAR>iY : Y ≅ Y'<VAR>iZ : Z ≅ Z'<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f' : X' ⟶ Z'<VAR>g' : Y' ⟶ Z'<VAR>wf : iX.hom ≫ f' = f ≫ iZ.hom<VAR>wg : iY.hom ≫ g' = g ≫ iZ.hom<GOAL>(CategoryTheory.Limits.cospanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingCospan.left = iX
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' : C<VAR>iX : X ≅ X'<VAR>iY : Y ≅ Y'<VAR>iZ : Z ≅ Z'<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f' : X' ⟶ Z'<VAR>g' : Y' ⟶ Z'<VAR>wf : iX.hom ≫ f' = f ≫ iZ.hom<VAR>wg : iY.hom ≫ g' = g ≫ iZ.hom<GOAL>(CategoryTheory.Limits.cospanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingCospan.right = iY
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X' Y' Z' : C<VAR>iX : X ≅ X'<VAR>iY : Y ≅ Y'<VAR>iZ : Z ≅ Z'<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f' : X' ⟶ Z'<VAR>g' : Y' ⟶ Z'<VAR>wf : iX.hom ≫ f' = f ≫ iZ.hom<VAR>wg : iY.hom ≫ g' = g ≫ iZ.hom<GOAL>(CategoryTheory.Limits.cospanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingCospan.one = iZ