no goals
α : Type ?u.65645
β : Type ?u.65648
G : Type u_1
inst✝ : CommGroup G
a✝ b✝ c✝ d a b c : G
⊢ c * a / (c * b) = a / b
rw [div_eq_mul_inv, mul_inv_rev, mul_comm b⁻¹ c⁻¹, mul_comm c a, mul_assoc, ←mul_assoc c,
  mul_right_inv, one_mul, div_eq_mul_inv]