∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] {β : Type u_2} {F : Type u_3} [inst_2 : Group β]
  [inst_3 : LinearOrder β] [inst_4 : FunLike F α β] [OrderHomClass F α β] [MonoidHomClass F α β] (f : F) (a : α),
  |f a|ₘ = f |a|ₘ