[Merged by Bors] - chore(CategoryTheory/Limits/Shapes/Pullbacks): split into multiple files and add documentation

[callesonne]

In this PR we split the file CategoryTheory/Limits/Shapes/Pullbacks.lean into 7 (!) smaller files and add documentation.

This contribution was inspired by the AIM workshop "Formalizing algebraic geometry" in June 2024.

---

This PR does not touch the code itself (except some lemma that I think had the wrong name by mistake, see the PR summary). In an upcoming PR I will golf & apply some fixes that I have noticed whilst going through this file, and in yet another PR I will add some API that I thought was missing whilst writing #14208

[erdOne]

This is great!

[joelriou]

It looks good to me. I know this can be a penance, but you should run git blame (probably more on mathlib3...) so as to identify slightly more precisely the main authors of the different chunks.

[callesonne]

It looks good to me. I know this can be a penance, but you should run git blame (probably more on mathlib3...) so as to identify slightly more precisely the main authors of the different chunks.

Yes, thanks! I was planning to ask about this (also I won't add myself as author for most files in the final version of this PR)

[github-actions]

PR summary fa6ea3ae90

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Limits.Shapes.Pullbacks	400	0	-400 (-100.00%)

---

Declarations diff

+ PullbackCone.fst_limit_cone
+ PullbackCone.snd_limit_cone
++-- flip_pt
- PullbackCone.fst_colimit_cocone
- PullbackCone.snd_colimit_cocone

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[erdOne]

Fantastic! Thanks a lot!
maintainer merge.

[github-actions]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style