{ι : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {u : ι → Set X} →
        {s : Set X} → {p : Set X → Prop} → CoeFun (ShrinkingLemma.PartialRefinement u s p) fun x => ι → Set X