no goals
α : Type ?u.7284
M₀ : Type u_1
G₀ : Type ?u.7290
M₀' : Type ?u.7293
G₀' : Type ?u.7296
F : Type ?u.7299
F' : Type ?u.7302
inst✝ : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ y * inverse x * x = y
rw [mul_assoc, inverse_mul_cancel x h, mul_one]