Theorem: MulAction.IsBlock_of_invariant (Jordan/Blocks.lean)

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
⊢ IsBlock G B
Tactic:
rw [IsBlock.def_one]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
⊢ ∀ (g : G), g • B = B ∨ Disjoint (g • B) B

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
⊢ ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
Tactic:
intro g
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ g • B = B ∨ Disjoint (g • B) B

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ g • B = B ∨ Disjoint (g • B) B
Tactic:
apply Or.intro_left
State after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ g • B = B

State before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ g • B = B
Tactic:
apply le_antisymm
State after:
case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ g • B ≤ B

case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ B ≤ g • B

State before:
case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ g • B ≤ B

case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ B ≤ g • B
Tactic:
exact hfB g
State after:
case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ B ≤ g • B

State before:
case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
⊢ B ≤ g • B
Tactic:
intro x hx
State after:
case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
x : X
hx : x ∈ B
⊢ x ∈ g • B

State before:
case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
x : X
hx : x ∈ B
⊢ x ∈ g • B
Tactic:
rw [Set.mem_smul_set_iff_inv_smul_mem]
State after:
case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
x : X
hx : x ∈ B
⊢ g⁻¹ • x ∈ B

State before:
case h.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
x : X
hx : x ∈ B
⊢ g⁻¹ • x ∈ B
Tactic:
apply hfB g⁻¹
State after:
case h.a.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
x : X
hx : x ∈ B
⊢ g⁻¹ • x ∈ g⁻¹ • B

State before:
case h.a.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
x : X
hx : x ∈ B
⊢ g⁻¹ • x ∈ g⁻¹ • B
Tactic:
rw [Set.smul_mem_smul_set_iff]
State after:
case h.a.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
x : X
hx : x ∈ B
⊢ x ∈ B

State before:
case h.a.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
x : X
hx : x ∈ B
⊢ x ∈ B
Tactic:
exact hx
State after:
no goals