feat(Limits/Shapes/Pullback): add pasting lemmas and API

[callesonne]

This PR proves some additional pasting lemmas and adds some general API to pullbacks.

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

---

These additional pullback results will make some proofs in #14208 more convenient.

[github-actions[bot]]

PR summary 154d565bae

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ PullbackCone.pasteVertFlip + PushoutCocone.pasteVertFlip + botSquareIsPushout + hasPullbackHorizPaste + hasPullbackVertPaste + hasPushoutVertPaste + inl_pushoutRightPushoutInlIso_hom + inl_pushoutRightPushoutInlIso_inv + inr_inl_pushoutRightPushoutInlIso_hom + inr_inr_pushoutRightPushoutInlIso_hom + inr_pushoutRightPushoutInlIso_inv + instance : HasPushout f (g ≫ g') + pasteHorizIsPullback + pasteHorizIsPullbackEquiv + pasteHorizIsPushout + pasteHorizIsPushoutEquiv + pasteVertIsPullback + pasteVertIsPullbackEquiv + pasteVertIsPushout + pasteVertIsPushoutEquiv + pullbackDiagonalMapIso.hom_fst + pullbackDiagonalMapIso.hom_snd + pullbackDiagonalMapIso.inv_fst + pullbackDiagonalMapIso.inv_snd_fst + pullbackDiagonalMapIso.inv_snd_snd + pullbackLeftPullbackSndIso + pullbackLeftPullbackSndIso_hom_fst + pullbackLeftPullbackSndIso_hom_snd + pullbackLeftPullbackSndIso_inv_fst + pullbackLeftPullbackSndIso_inv_fst_snd + pullbackLeftPullbackSndIso_inv_snd_snd + pushoutRightPushoutInlIso + topSquareIsPullback - bigSquareIsPullback - bigSquareIsPushout - pullbackDiagonalMapIso_hom_fst - pullbackDiagonalMapIso_hom_snd - pullbackDiagonalMapIso_inv_fst - pullbackDiagonalMapIso_inv_snd_fst - pullbackDiagonalMapIso_inv_snd_snd

You can run this locally as follows

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

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

The doc-module for script/declarations_diff.sh contains some details about this script.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#14526~~
• ~~leanprover-community/mathlib4#14524~~ By Dependent Issues (🤖). Happy coding!

[kim-em]

Thanks for this! I agree the abbrevs are worth it.

If you can implement Johan's suggestion, that great. If it turns out annoying, just say so. I'm happy to merge soon.

[callesonne]

Thanks for this! I agree the abbrevs are worth it.

If you can implement Johan's suggestion, that great. If it turns out annoying, just say so. I'm happy to merge soon.

I can't seem to find this ext lemma, is it something to do with equivs between subsingletons?

[joelriou]

I can't seem to find this ext lemma, is it something to do with equivs between subsingletons?

Yes, you may prove the left/right_inv fields of the equivalence using Subsingleton.elim.

[joelriou]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style