∀ {X : Type u_1} {Y : Type u_2} [inst : Group X] [inst_1 : CommGroup Y] (U : Set X) (W : Set Y) (f : X → Y)
  (motive : f ∈ (U.pi fun x => W) ∩ Set.range DFunLike.coe → Prop) (x : f ∈ (U.pi fun x => W) ∩ Set.range DFunLike.coe),
  (∀ (hg : f ∈ U.pi fun x => W) (g : X →* Y) (hf : ⇑g = f), motive ⋯) → motive x