∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddCommGroup Y]
  [inst_2 : LinearOrder Y] [IsOrderedAddMonoid Y], IsOrderedAddMonoid (Function.locallyFinsuppWithin U Y)