α : Type ?u.75037
β : Type ?u.75040
G : Type u_1
inst✝ : CommGroup G
a b c d : G
⊢ c * b = d * a ↔ a * d = c * b
α : Type ?u.75037
β : Type ?u.75040
G : Type u_1
inst✝ : CommGroup G
a b c d : G
⊢ a / b = c / d ↔ a * d = c * b
rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, eq_comm, div_eq_iff_eq_mul']
no goals
α : Type ?u.75037
β : Type ?u.75040
G : Type u_1
inst✝ : CommGroup G
a b c d : G
⊢ c * b = d * a ↔ a * d = c * b
simp only [mul_comm, eq_comm]