Theorem: MulAction.orbit.equal_or_disjoint (Jordan/Blocks.lean)

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
⊢ orbit G a = orbit G b ∨ Disjoint (orbit G a) (orbit G b)
Tactic:
cases' em (Disjoint (orbit G a) (orbit G b)) with h h
State after:
case inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : Disjoint (orbit G a) (orbit G b)
⊢ orbit G a = orbit G b ∨ Disjoint (orbit G a) (orbit G b)

case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : ¬Disjoint (orbit G a) (orbit G b)
⊢ orbit G a = orbit G b ∨ Disjoint (orbit G a) (orbit G b)

State before:
case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : ¬Disjoint (orbit G a) (orbit G b)
⊢ orbit G a = orbit G b ∨ Disjoint (orbit G a) (orbit G b)
Tactic:
apply Or.intro_left
State after:
case inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : ¬Disjoint (orbit G a) (orbit G b)
⊢ orbit G a = orbit G b

State before:
case inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : ¬Disjoint (orbit G a) (orbit G b)
⊢ orbit G a = orbit G b
Tactic:
rw [Set.not_disjoint_iff] at h
State after:
case inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : ∃ x ∈ orbit G a, x ∈ orbit G b
⊢ orbit G a = orbit G b

State before:
case inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : ∃ x ∈ orbit G a, x ∈ orbit G b
⊢ orbit G a = orbit G b
Tactic:
obtain ⟨x, hxa, hxb⟩ := h
State after:
case inr.h.intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b x : X
hxa : x ∈ orbit G a
hxb : x ∈ orbit G b
⊢ orbit G a = orbit G b

State before:
case inr.h.intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b x : X
hxa : x ∈ orbit G a
hxb : x ∈ orbit G b
⊢ orbit G a = orbit G b
Tactic:
rw [← orbit_eq_iff] at hxa hxb
State after:
case inr.h.intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b x : X
hxa : orbit G x = orbit G a
hxb : orbit G x = orbit G b
⊢ orbit G a = orbit G b

State before:
case inr.h.intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b x : X
hxa : orbit G x = orbit G a
hxb : orbit G x = orbit G b
⊢ orbit G a = orbit G b
Tactic:
rw [← hxa, ← hxb]
State after:
no goals

State before:
case inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : Disjoint (orbit G a) (orbit G b)
⊢ orbit G a = orbit G b ∨ Disjoint (orbit G a) (orbit G b)
Tactic:
apply Or.intro_right
State after:
case inl.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : Disjoint (orbit G a) (orbit G b)
⊢ Disjoint (orbit G a) (orbit G b)

State before:
case inl.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
h : Disjoint (orbit G a) (orbit G b)
⊢ Disjoint (orbit G a) (orbit G b)
Tactic:
exact h
State after:
no goals