no goals
M : Type ?u.17057
M' : Type ?u.17060
M₁ : Type ?u.17063
R : Type ?u.17066
R' : Type u_1
F : Type ?u.17072
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
x y r : R'
hr : r ∈ R'⁰
⊢ r * x = r * y ↔ x = y
simp_rw [mul_comm r, mul_cancel_right_mem_nonZeroDivisors hr]