Commit 2025-10-15 15:17 ab46cf68
View on Github →refactor: weaken HasPullbacks to HasPullback in MorphismProperty.OverAdjuction (#29810)
This PR replaces the global assumption of HasPullback T with the weaker assumption that pullbacks exist along the morphism only.
For the sake of readability I also moved the variable (f : X -> Y) into the statement of each theorem. As instructed in https://github.com/leanprover-community/mathlib4/pull/29795#discussion_r2363310388