α : Type ?u.58098
β : Type ?u.58101
G : Type u_1
inst✝ : Group G
a✝ b✝ c✝ d a b c : G
⊢ a * c / c / b = a / b
α : Type ?u.58098
β : Type ?u.58101
G : Type u_1
inst✝ : Group G
a✝ b✝ c✝ d a b c : G
⊢ a * c / (b * c) = a / b
rw [div_mul_eq_div_div_swap]
no goals
α : Type ?u.58098
β : Type ?u.58101
G : Type u_1
inst✝ : Group G
a✝ b✝ c✝ d a b c : G
⊢ a * c / c / b = a / b
simp only [mul_left_inj, eq_self_iff_true, mul_div_cancel'']