∀ {A : Type u_1} {B : Type u_2} {F : Type u_3} [inst : FunLike F A B] {f : F} [inst_1 : GroupWithZero A]
  [inst_2 : GroupWithZero B] [inst_3 : MonoidWithZeroHomClass F A B],
  Units.val '' ↑(MonoidWithZeroHom.valueGroup f) = Set.range ⇑f \ {0}