∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C}
  (f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ≅ G.obj { as := CategoryTheory.Limits.WalkingPair.left })
  (g :
    F.obj { as := CategoryTheory.Limits.WalkingPair.right } ≅ G.obj { as := CategoryTheory.Limits.WalkingPair.right })
  (X : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair),
  (CategoryTheory.Limits.mapPairIso f g).hom.app X =
    (match X with
      | { as := CategoryTheory.Limits.WalkingPair.left } => f
      | { as := CategoryTheory.Limits.WalkingPair.right } => g).hom