If there is an inverse, it's unique?

Stream: Is there code for X?

[Anne Baanen]

What is the best way to get the result i * j = 1 → i * j' = 1 → j = j' in a comm_monoid? It seems like this would be in mathlib already but library_search doesn't find it, nor the equivalent in a general monoid.

[Mario Carneiro]

It exists, but the proof is buried inside units.ext.

import algebra.group.units

example {α} [comm_monoid α] (i j j' : α) :
  i * j = 1 → i * j' = 1 → j = j' :=
λ h h', congr_arg units.inv $
  @units.ext _ _ (units.mk_of_mul_eq_one _ _ h) (units.mk_of_mul_eq_one _ _ h') rfl