α : Type u
M : Type u_1
N : Type ?u.58079
inst✝ : CommMonoid M
a : M
⊢ (∃ b, a * b = 1) ↔ ∃ b, b * a = 1
α : Type u
M : Type u_1
N : Type ?u.58079
inst✝ : CommMonoid M
a : M
⊢ IsUnit a ↔ ∃ b, b * a = 1
rw [isUnit_iff_exists_inv]
no goals
α : Type u
M : Type u_1
N : Type ?u.58079
inst✝ : CommMonoid M
a : M
⊢ (∃ b, a * b = 1) ↔ ∃ b, b * a = 1
simp [mul_comm]