no goals
α : Type ?u.9281
M₀ : Type u_1
G₀ : Type ?u.9287
M₀' : Type ?u.9290
G₀' : Type ?u.9293
F : Type ?u.9296
F' : Type ?u.9299
inst✝ : CancelMonoidWithZero M₀
a b c : M₀
⊢ a * b = a ↔ a * b = a * 1
rw [mul_one]