Lean: Prove that if homomorphisms are equal as functions, then they are equal as homomorphisms.

Question

Let's say I have a simple magma structure defined as follows:

structure Magma :=
  (carrier : Type u)
  (op : carrier → carrier → carrier)

together with a magma homomorphism structure:

class hom {X Y : Magma} (f : X → Y) :=
  (resp_op : ∀ x y : X,
    f (X.op x y) = Y.op (f x) (f y) )

structure Hom (X Y : Magma) :=
  (func : X → Y) (hom_func : hom func)

And I need to prove the following (trivial) lemma:

lemma equate_hom {X Y : Magma} :
∀ f g : Hom X Y, f.func = g.func  →  f = g

I have been stuck on this for some time now. But there must be some really simple way to do this, right? The full example is here.