no goals
α : Type u
β : Type v
γ : Type w
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : Group β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
rw [inv_eq_iff_mul_eq_one, smul_mul_smul, mul_right_inv, mul_right_inv, one_smul]