no goals
α : Type ?u.20012
M₀ : Type ?u.20015
G₀ : Type u_1
M₀' : Type ?u.20021
G₀' : Type ?u.20024
F : Type ?u.20027
F' : Type ?u.20030
inst✝ : GroupWithZero G₀
a b✝ c g h✝ x : G₀
h : a ≠ 0
b : G₀
⊢ a⁻¹ * a * b = b
simp [h]