no goals
α : Type ?u.20829
M₀ : Type ?u.20832
G₀ : Type u_1
M₀' : Type ?u.20838
G₀' : Type ?u.20841
F : Type ?u.20844
F' : Type ?u.20847
inst✝ : GroupWithZero G₀
a b c g h✝ x : G₀
h : a * b = 1
⊢ a⁻¹ = b
rw [← inv_mul_cancel_left₀ (left_ne_zero_of_mul_eq_one h) b, h, mul_one]