Theorem: Tutorial.inv_smul_smul (Solution/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:
rw [smul_smul]
State after:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x : X
⊢ (a⁻¹ * a) • x = x

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