feat(category_theory/limits): Results about pullbacks (#9984)
feat(category_theory/limits): Results about pullbacks (#9984)

- Provided the explicit isomorphism `X ×[Z] Y ≅ Y ×[Z] X`.
- Provided the pullback of f g when either one is iso or when both are mono.



Co-authored-by: erdOne <5a6b17dbbc661dec6b250b080ab0033de7d56af5@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib