Epimorphism_Preserves_Commutativity

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

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