no goals
α : Type ?u.8217
M₀ : Type u_1
G₀ : Type ?u.8223
M₀' : Type ?u.8226
G₀' : Type ?u.8229
F : Type ?u.8232
F' : Type ?u.8235
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit x
h1 : inverse x * y = z
⊢ y = x * z
rw [← h1, mul_inverse_cancel_left _ _ h]
no goals
α : Type ?u.8217
M₀ : Type u_1
G₀ : Type ?u.8223
M₀' : Type ?u.8226
G₀' : Type ?u.8229
F : Type ?u.8232
F' : Type ?u.8235
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit x
h1 : y = x * z
⊢ inverse x * y = z
rw [h1, inverse_mul_cancel_left _ _ h]