∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (S : Subsemigroup M) (f : M →ₙ* N)
  (hf : Function.Injective ⇑f), S.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑S) hf, map_mul' := ⋯ }