ext_iff lemmas in CategoryTheory

Stream: mathlib4

[Floris van Doorn]

Is there a reason that ext-lemmas in category theory have no ext_iff version? E.g. CategoryTheory.Limits.pullback.hom_ext_iff for docs#CategoryTheory.Limits.pullback.hom_ext.
For example src#AlgebraicGeometry.Scheme.Pullback.cocycle seems like it could become a 1/2-line proof with simp [pullback.hom_ext_iff, some more lemmas]

[Floris van Doorn]

I noticed this when cleaning up AlgebraicGeometry.Pullbacks (#12995)

[Kim Morrison]

No, just oversight. It would be great to add these.