∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z}
  (c : CategoryTheory.Limits.PullbackCone f g) (X_1 : CategoryTheory.Limits.WalkingSpan),
  c.unop.ι.app X_1 =
    CategoryTheory.CategoryStruct.comp
      (match X_1 with
          | none => CategoryTheory.Iso.refl Z
          | some CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Iso.refl X
          | some CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Iso.refl Y).hom.unop
      (c.π.app X_1).unop