α : Type ?u.67616
β : Type ?u.67619
G : Type u_1
inst✝ : CommGroup G
a b c d : G
h : b = c / a
⊢ a * (c * a⁻¹) = c
α : Type ?u.67616
β : Type ?u.67619
G : Type u_1
inst✝ : CommGroup G
a b c d : G
h : b = c / a
⊢ a * b = c
simp [h]
no goals
α : Type ?u.67616
β : Type ?u.67619
G : Type u_1
inst✝ : CommGroup G
a b c d : G
h : b = c / a
⊢ a * (c * a⁻¹) = c
rw [mul_comm c, mul_inv_cancel_left]