∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M → N) (hf : ∀ (x y : M), f (x * y) = f x * f y),
  { toFun := f, map_mul' := hf }.srange = { carrier := Set.range f, mul_mem' := ⋯ }