Theorem: MulAction.IsBlockSystem.of_normal (Jordan/Blocks.lean)

State before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
⊢ IsBlockSystem G (Set.range fun a => orbit (↥N) a)
Tactic:
constructor
State after:
case left
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
⊢ Setoid.IsPartition (Set.range fun a => orbit (↥N) a)

case right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
⊢ ∀ b ∈ Set.range fun a => orbit (↥N) a, IsBlock G b

State before:
case left
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
⊢ Setoid.IsPartition (Set.range fun a => orbit (↥N) a)
Tactic:
apply IsPartition.of_orbits
State after:
no goals

State before:
case right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
⊢ ∀ b ∈ Set.range fun a => orbit (↥N) a, IsBlock G b
Tactic:
intro b
State after:
case right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
b : Set X
⊢ (b ∈ Set.range fun a => orbit (↥N) a) → IsBlock G b

State before:
case right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
b : Set X
⊢ (b ∈ Set.range fun a => orbit (↥N) a) → IsBlock G b
Tactic:
rintro ⟨a, rfl⟩
State after:
case right.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
⊢ IsBlock G ((fun a => orbit (↥N) a) a)

State before:
case right.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
⊢ IsBlock G ((fun a => orbit (↥N) a) a)
Tactic:
exact orbit.IsBlock_of_normal nN a
State after:
no goals