no goals
α : Type ?u.11158
M₀ : Type u_1
G₀ : Type ?u.11164
M₀' : Type ?u.11167
G₀' : Type ?u.11170
F : Type ?u.11173
F' : Type ?u.11176
inst✝ : CancelMonoidWithZero M₀
a b c : M₀
ha : a ≠ 0
⊢ a * b = a ↔ b = 1
rw [Iff.comm, ← mul_right_inj' ha, mul_one]