Theorem: Tutorial.smul_inv_smul (Tutorial/Advanced/Algebra/Lecture3.lean)

State before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x : X
⊢ a • a⁻¹ • x = x
Tactic:
sorry
State after:
no goals