Epimorphism_Preserves_Semigroups

import Mathlib.Algebra.Group.Defs
import Mathlib.Logic.Function.Basic

theorem Epimorphism_Preserves_Semigroups {G H : Type _} [Semigroup G] [Mul H] (f : G → H) (hf : ∀ a b : G, f (a * b) = f a * f b) (hsurj : Function.Surjective f) : ∀ a b c : H, a * b * c = a * (b * c) := by sorry