no goals
α : Type ?u.18039
M₀ : Type ?u.18042
G₀ : Type u_1
M₀' : Type ?u.18048
G₀' : Type ?u.18051
F : Type ?u.18054
F' : Type ?u.18057
inst✝ : GroupWithZero G₀
a b c g h✝ x : G₀
h : x ≠ 0
y y' : G₀
w : (fun y => x * y) y = (fun y => x * y) y'
⊢ y = y'
simpa only [← mul_assoc, inv_mul_cancel h, one_mul] using congr_arg (fun y => x⁻¹ * y) w