no goals
α : Type ?u.14933
M₀ : Type ?u.14936
G₀ : Type u_1
M₀' : Type ?u.14942
G₀' : Type ?u.14945
F : Type ?u.14948
F' : Type ?u.14951
inst✝ : GroupWithZero G₀
a b✝ c g h✝ x : G₀
h : a ≠ 0
b : G₀
⊢ a * a⁻¹ * b = b
simp [h]