no goals
α : Type ?u.13686
M₀ : Type ?u.13689
G₀ : Type u_1
M₀' : Type ?u.13695
G₀' : Type ?u.13698
F : Type ?u.13701
F' : Type ?u.13704
inst✝¹ : MonoidWithZero M₀
inst✝ : CommGroupWithZero G₀
a b✝ c d b : G₀
h : a ≠ 0
⊢ 1 / (a * b) * a = 1 / b
rw [div_mul_eq_mul_div, one_mul, div_mul_right _ h]