no goals
α : Type ?u.7173
M₀ : Type u_1
G₀ : Type ?u.7179
M₀' : Type ?u.7182
G₀' : Type ?u.7185
F : Type ?u.7188
F' : Type ?u.7191
inst✝ : CancelMonoidWithZero M₀
a b c : M₀
⊢ a * c = b * c ↔ a = b ∨ c = 0
by_cases hc : c = 0 <;> [simp [hc]; simp [mul_left_inj', hc]]