Theorem: Tutorial.GroupAction.injective (Solution/Advanced/Algebra/Lecture3.lean)

State before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
⊢ Function.Injective fun x => a • x
Tactic:
intro x y (h : a • x = a • y)
State after:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x y : X
h : a • x = a • y
⊢ x = y

State before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x y : X
h : a • x = a • y
⊢ x = y
Tactic:
calc x = a⁻¹ • a • x := by rw [inv_smul_smul]
  _ = a⁻¹ • a • y := by rw [h]
  _ = y := by rw [inv_smul_smul]
State after:
no goals

State before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x y : X
h : a • x = a • y
⊢ x = a⁻¹ • a • x
Tactic:
rw [inv_smul_smul]
State after:
no goals

State before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x y : X
h : a • x = a • y
⊢ a⁻¹ • a • x = a⁻¹ • a • y
Tactic:
rw [h]
State after:
no goals

State before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x y : X
h : a • x = a • y
⊢ a⁻¹ • a • y = y
Tactic:
rw [inv_smul_smul]
State after:
no goals