∀ {A : Type u_1} {B : Type u_2} {F : Type u_3} [inst : FunLike F A B] {f : F} [inst_1 : MonoidWithZero A]
  [inst_2 : GroupWithZero B] [inst_3 : MonoidWithZeroHomClass F A B] {a : A},
  ((MonoidWithZeroHom.ValueGroup₀.restrict₀ f) a = 0) = (f a = 0)