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