no goals
M : Type ?u.15454
M' : Type ?u.15457
M₁ : Type ?u.15460
R : Type u_1
R' : Type ?u.15466
F : Type ?u.15469
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
x y r : R
hr : r ∈ R⁰
h : x * r = y * r
⊢ x = y
rw [← sub_eq_zero, ← mul_right_mem_nonZeroDivisors_eq_zero_iff hr, sub_mul, h, sub_self]