no goals
α : Type ?u.31135
M₀ : Type ?u.31138
G₀ : Type u_1
M₀' : Type ?u.31144
G₀' : Type ?u.31147
F : Type ?u.31150
F' : Type ?u.31153
inst✝ : CommGroupWithZero G₀
a✝ b✝ c✝ d a b c : G₀
⊢ a / c * b = a * b / c
simp_rw [div_eq_mul_inv, mul_assoc, mul_comm c⁻¹]