∀ {M : Type u_1} [inst : AddZeroClass M] {N : Type u_5} {S : Type u_6} [inst_1 : AddZeroClass N] [inst_2 : SetLike S M]
  [inst_3 : AddSubmonoidClass S M] (f : M →+ N) (s : S) (x : ↥s), (f.restrict s) x = f ↑x