no goals
α : Type ?u.29573
M₀ : Type ?u.29576
G₀ : Type u_1
M₀' : Type ?u.29582
G₀' : Type ?u.29585
F : Type ?u.29588
F' : Type ?u.29591
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : a ≠ 0
g : G₀
⊢ (fun g => a * g) (a⁻¹ * g) = g
simp [← mul_assoc, mul_inv_cancel h]