Small sets in the category of structured arrows

Here we prove a technical result about small sets in the category of structured arrows that will be used in the proof of the Special Adjoint Functor Theorem.

instance CategoryTheory.StructuredArrow.small_proj_preimage_of_locallySmall {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {S : D} {T : Functor C D} {𝒢 : Set C} [Small.{v₁, u₁} ↑𝒢] [LocallySmall.{v₁, v₂, u₂} D] : Small.{v₁, max u₁ v₂} ↑((proj S T).obj ⁻¹' 𝒢)

instance CategoryTheory.CostructuredArrow.small_proj_preimage_of_locallySmall {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {S : Functor C D} {T : D} {𝒢 : Set C} [Small.{v₁, u₁} ↑𝒢] [LocallySmall.{v₁, v₂, u₂} D] : Small.{v₁, max u₁ v₂} ↑((proj S T).obj ⁻¹' 𝒢)