∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : X ⟶ Z)
  (X_1 : CategoryTheory.Limits.WalkingCospan),
  (CategoryTheory.Limits.cospanUnop f g).inv.app X_1 =
    (match X_1 with
      | none => CategoryTheory.Iso.refl (Opposite.unop X)
      | some CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Iso.refl (Opposite.unop Y)
      | some CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Iso.refl (Opposite.unop Z)).inv