∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {α : Type u_2}
  (f : { a // a ≠ 0 } → α),
  (∀ (a b : { a // a ≠ 0 }), FiniteArchimedeanClass.mk ↑a ⋯ = FiniteArchimedeanClass.mk ↑b ⋯ → f a = f b) →
    ∀ (a b : M),
      ArchimedeanClass.mk a = ArchimedeanClass.mk b →
        (if h : a = 0 then ⊤ else ↑(f ⟨a, h⟩)) = if h : b = 0 then ⊤ else ↑(f ⟨b, h⟩)