chore: backports for leanprover/lean4#4814 (part 27) (#15543)

Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

@@ -542,7 +542,7 @@ instance (priority := 900) : IsLocalAtTarget P := by
     exact of_isPullback (.of_hasPullback _ _) this
 
 open AffineTargetMorphismProperty in
-protected theorem iff :
+protected theorem iff {P : MorphismProperty Scheme} {Q : AffineTargetMorphismProperty} :
     HasAffineProperty P Q ↔ IsLocalAtTarget P ∧ Q = of P :=
   ⟨fun _ ↦ ⟨inferInstance, ext fun _ _ _ ↦ iff_of_isAffine.symm⟩,
     fun ⟨_, e⟩ ↦ e ▸ of_isLocalAtTarget P⟩