∀ {M : Type u_3} {N : Type u_4} [inst : Semigroup M] [inst_1 : Semigroup N] {s : Set M} (f : M → N)
  (hs : Subsemigroup.closure s = ⊤) (hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y),
  MulHom.ofDense f hs hmul = { toFun := f, map_mul' := ⋯ }