∀ {ι : Type u_7} (p : ι → Prop) (Y : ι → Type u_8) [inst : (i : ι) → TopologicalSpace (Y i)] [inst_1 : DecidablePred p]
  (f : (i : ι) → Y i), (Homeomorph.piEquivPiSubtypeProd p Y) f = (fun x => f ↑x, fun x => f ↑x)