Update units.lean (#1938)

Author: jcommelin

src/algebra/group/units.lean

@@ -107,6 +107,8 @@ units.ext $ nat.eq_one_of_dvd_one ⟨u.inv, u.val_inv.symm⟩
 def units.mk_of_mul_eq_one [comm_monoid α] (a b : α) (hab : a * b = 1) : units α :=
 ⟨a, b, hab, (mul_comm b a).trans hab⟩
 
+@[simp] lemma units.coe_mk_of_mul_eq_one [comm_monoid α] {a b : α} (h : a * b = 1) :
+  (units.mk_of_mul_eq_one a b h : α) = a := rfl
 
 section monoid
   variables [monoid α] {a b c : α}