feat(CategoryTheory/Bicategory/Grothendieck): functors between Grothendieck constructions induced by strong natural transforms

[robin-carlier]

Generalize the content of CategoryTheory/Grothendieck to pseudofunctor and show that a strong oplax natural transformation of pseudofunctors induces a functor between the Grothendieck contsructions, and that the construction preserves composition and identities.

---

The proof of map_comp_eq is rather slow and needs a slight increase in heartbeats to go through. It’s probably golfable.

[github-actions[bot]]

PR summary 7c4a7c92fb

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Bicategory.Grothendieck	326	328	+2 (+0.61%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Bicategory.Grothendieck	2

---

Declarations diff

+ map + mapCompForgetIso + mapCompIso + mapIdIso + map_comp_eq + map_comp_forget + map_id_eq + map_map + map_obj

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.