∀ {A : Type u_2} {B : Type u_1} {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) (h : ¬f a = 0),
  Units.mk0 (f a) h ∈ MonoidWithZeroHom.valueGroup f