∀ {ι : Type u_2} {π : ι → Type u_3} {s t : Finset ι} [inst : DecidablePred fun x => x ∈ s] (hst : s ⊆ t)
  (u : (i : ↥s) → Set (π ↑i)),
  Finset.restrict₂ hst ⁻¹' Set.univ.pi u = Set.univ.pi fun j => if h : ↑j ∈ s then u ⟨↑j, h⟩ else Set.univ