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

State before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
⊢ orbit G x = orbit G y ↔ y ∈ orbit G x
Tactic:
constructor
State after:
case mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
⊢ orbit G x = orbit G y → y ∈ orbit G x

case mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
⊢ y ∈ orbit G x → orbit G x = orbit G y

State before:
case mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
⊢ orbit G x = orbit G y → y ∈ orbit G x
Tactic:
intro h
State after:
case mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
h : orbit G x = orbit G y
⊢ y ∈ orbit G x

State before:
case mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
h : orbit G x = orbit G y
⊢ y ∈ orbit G x
Tactic:
rw [h]
State after:
case mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
h : orbit G x = orbit G y
⊢ y ∈ orbit G y

State before:
case mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
h : orbit G x = orbit G y
⊢ y ∈ orbit G y
Tactic:
exists 1
State after:
case mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
h : orbit G x = orbit G y
⊢ 1 • y = y

State before:
case mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
h : orbit G x = orbit G y
⊢ 1 • y = y
Tactic:
simp
State after:
no goals

State before:
case mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
⊢ y ∈ orbit G x → orbit G x = orbit G y
Tactic:
intro ⟨a, ha⟩
State after:
case mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
⊢ orbit G x = orbit G y

State before:
case mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
⊢ orbit G x = orbit G y
Tactic:
ext z
State after:
case mpr.h
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
⊢ z ∈ orbit G x ↔ z ∈ orbit G y

State before:
case mpr.h
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
⊢ z ∈ orbit G x ↔ z ∈ orbit G y
Tactic:
constructor
State after:
case mpr.h.mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
⊢ z ∈ orbit G x → z ∈ orbit G y

case mpr.h.mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
⊢ z ∈ orbit G y → z ∈ orbit G x

State before:
case mpr.h.mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
⊢ z ∈ orbit G x → z ∈ orbit G y
Tactic:
intro ⟨b, hb⟩
State after:
case mpr.h.mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • x = z
⊢ z ∈ orbit G y

State before:
case mpr.h.mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • x = z
⊢ z ∈ orbit G y
Tactic:
rw [← hb, ← ha]
State after:
case mpr.h.mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • x = z
⊢ b • x ∈ orbit G (a • x)

State before:
case mpr.h.mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • x = z
⊢ b • x ∈ orbit G (a • x)
Tactic:
exists b * a⁻¹
State after:
case mpr.h.mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • x = z
⊢ (b * a⁻¹) • a • x = b • x

State before:
case mpr.h.mp
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • x = z
⊢ (b * a⁻¹) • a • x = b • x
Tactic:
simp [mul_smul]
State after:
no goals

State before:
case mpr.h.mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
⊢ z ∈ orbit G y → z ∈ orbit G x
Tactic:
intro ⟨b, hb⟩
State after:
case mpr.h.mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • y = z
⊢ z ∈ orbit G x

State before:
case mpr.h.mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • y = z
⊢ z ∈ orbit G x
Tactic:
rw [← hb, ← ha]
State after:
case mpr.h.mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • y = z
⊢ b • a • x ∈ orbit G x

State before:
case mpr.h.mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • y = z
⊢ b • a • x ∈ orbit G x
Tactic:
exists b * a
State after:
case mpr.h.mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • y = z
⊢ (b * a) • x = b • a • x

State before:
case mpr.h.mpr
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
a : G
ha : a • x = y
z : X
b : G
hb : b • y = z
⊢ (b * a) • x = b • a • x
Tactic:
simp [mul_smul]
State after:
no goals