no goals
α : Type ?u.25853
M₀ : Type ?u.25856
G₀ : Type u_1
M₀' : Type ?u.25862
G₀' : Type ?u.25865
F : Type ?u.25868
F' : Type ?u.25871
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a / a * a = a
rw [div_eq_mul_inv, mul_inv_mul_self a]