no goals
α : Type ?u.7593
M₀ : Type u_1
G₀ : Type ?u.7599
M₀' : Type ?u.7602
G₀' : Type ?u.7605
F : Type ?u.7608
F' : Type ?u.7611
inst✝ : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ x * (inverse x * y) = y
rw [← mul_assoc, mul_inverse_cancel x h, one_mul]