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

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

State before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
y : X
⊢ ∃ a_1, (fun x => a • x) a_1 = y
Tactic:
use a⁻¹ • y
State after:
case h
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
y : X
⊢ (fun x => a • x) (a⁻¹ • y) = y

State before:
case h
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
y : X
⊢ (fun x => a • x) (a⁻¹ • y) = y
Tactic:
exact smul_inv_smul
State after:
no goals