Theorem: MulAction.IsPartition.of_orbits (Jordan/Blocks.lean)

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
⊢ Setoid.IsPartition (Set.range fun a => orbit G a)
Tactic:
constructor
State after:
case left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
⊢ ∅ ∉ Set.range fun a => orbit G a

case right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
⊢ ∀ (a : X), ∃! b x, a ∈ b

State before:
case right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
⊢ ∀ (a : X), ∃! b x, a ∈ b
Tactic:
intro a
State after:
case right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ ∃! b x, a ∈ b

State before:
case right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ ∃! b x, a ∈ b
Tactic:
use orbit G a
State after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ (fun b => ∃! x, a ∈ b) (orbit G a) ∧ ∀ (y : Set X), (fun b => ∃! x, a ∈ b) y → y = orbit G a

State before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ (fun b => ∃! x, a ∈ b) (orbit G a) ∧ ∀ (y : Set X), (fun b => ∃! x, a ∈ b) y → y = orbit G a
Tactic:
constructor
State after:
case h.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ (fun b => ∃! x, a ∈ b) (orbit G a)

case h.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ ∀ (y : Set X), (fun b => ∃! x, a ∈ b) y → y = orbit G a

State before:
case left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
⊢ ∅ ∉ Set.range fun a => orbit G a
Tactic:
rintro ⟨a, ha : orbit G a = ∅⟩
State after:
case left.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
ha : orbit G a = ∅
⊢ False

State before:
case left.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
ha : orbit G a = ∅
⊢ False
Tactic:
exact Set.Nonempty.ne_empty (MulAction.orbit_nonempty a) ha
State after:
no goals

State before:
case h.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ (fun b => ∃! x, a ∈ b) (orbit G a)
Tactic:
simp only [Set.mem_range_self, mem_orbit_self, exists_unique_iff_exists, exists_true_left]
State after:
no goals

State before:
case h.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ ∀ (y : Set X), (fun b => ∃! x, a ∈ b) y → y = orbit G a
Tactic:
simp only [Set.mem_range, exists_unique_iff_exists, exists_prop, and_imp, forall_exists_index,
  forall_apply_eq_imp_iff']
State after:
case h.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ ∀ (y : Set X) (x : X), orbit G x = y → a ∈ y → y = orbit G a

State before:
case h.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ ∀ (y : Set X) (x : X), orbit G x = y → a ∈ y → y = orbit G a
Tactic:
rintro B b ⟨rfl⟩ ha
State after:
case h.right.refl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
ha : a ∈ orbit G b
⊢ orbit G b = orbit G a

State before:
case h.right.refl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
ha : a ∈ orbit G b
⊢ orbit G b = orbit G a
Tactic:
apply symm
State after:
case h.right.refl.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
ha : a ∈ orbit G b
⊢ orbit G a = orbit G b

State before:
case h.right.refl.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
ha : a ∈ orbit G b
⊢ orbit G a = orbit G b
Tactic:
rw [orbit_eq_iff]
State after:
case h.right.refl.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
ha : a ∈ orbit G b
⊢ a ∈ orbit G b

State before:
case h.right.refl.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a b : X
ha : a ∈ orbit G b
⊢ a ∈ orbit G b
Tactic:
exact ha
State after:
no goals