no goals
α : Type ?u.8485
M₀ : Type u_1
G₀ : Type ?u.8491
M₀' : Type ?u.8494
G₀' : Type ?u.8497
F : Type ?u.8500
F' : Type ?u.8503
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit z
h1 : x = y * inverse z
⊢ x * z = y
rw [h1, inverse_mul_cancel_right _ _ h]
no goals
α : Type ?u.8485
M₀ : Type u_1
G₀ : Type ?u.8491
M₀' : Type ?u.8494
G₀' : Type ?u.8497
F : Type ?u.8500
F' : Type ?u.8503
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit z
h1 : x * z = y
⊢ x = y * inverse z
rw [← h1, mul_inverse_cancel_right _ _ h]