no goals
α : Type ?u.25591
M₀ : Type ?u.25594
G₀ : Type u_1
M₀' : Type ?u.25600
G₀' : Type ?u.25603
F : Type ?u.25606
F' : Type ?u.25609
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a * a / a = a
rw [div_eq_mul_inv, mul_self_mul_inv a]