feat(Pullback/CommSq): add more pasting lemmas for IsPullback (#14985)

This PR adds two (variants) of pasting lemmas in the `IsPullback` framework. These are variants where the second square has a morphism that is induced from the universal property of the first.

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

Author: callesonne