Epimorphism_Preserves_Associativity

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

theorem Epimorphism_Preserves_Associativity {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