Restriction_of_Homomorphism_to_Image_is_Epimorphism

import Mathlib.Data.Set.Function
import Mathlib.Algebra.Group.Defs

theorem Restriction_of_Homomorphism_to_Image_is_Epimorphism {G H : Type _} [Group G] [Group H] (f : G → H) (hf : ∀ a b : G, f (a * b) = f a * f b) : Function.Surjective (fun g : G => (⟨f g, Set.mem_range.mpr ⟨g, rfl⟩⟩ : Set.range f)) := by sorry