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

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
⊢ stabilizer G a ≤ stabilizer G B
Tactic:
intro g hg
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g ∈ stabilizer G a
⊢ g ∈ stabilizer G B

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g ∈ stabilizer G a
⊢ g ∈ stabilizer G B
Tactic:
rw [mem_stabilizer_iff] at hg ⊢
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
⊢ g • B = B

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
⊢ g • B = B
Tactic:
cases' IsBlock.def_one.mp hB g with h h'
State after:
case inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h : g • B = B
⊢ g • B = B

case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : Disjoint (g • B) B
⊢ g • B = B

State before:
case inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h : g • B = B
⊢ g • B = B

case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : Disjoint (g • B) B
⊢ g • B = B
Tactic:
exact h
State after:
case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : Disjoint (g • B) B
⊢ g • B = B

State before:
case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : Disjoint (g • B) B
⊢ g • B = B
Tactic:
exfalso
State after:
case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : Disjoint (g • B) B
⊢ False

State before:
case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : Disjoint (g • B) B
⊢ False
Tactic:
rw [← Set.mem_empty_iff_false a]
State after:
case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : Disjoint (g • B) B
⊢ a ∈ ∅

State before:
case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : Disjoint (g • B) B
⊢ a ∈ ∅
Tactic:
simp only [disjoint_iff, Set.inf_eq_inter, Set.bot_eq_empty] at h'
State after:
case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : g • B ∩ B = ∅
⊢ a ∈ ∅

State before:
case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : g • B ∩ B = ∅
⊢ a ∈ ∅
Tactic:
rw [← h', Set.mem_inter_iff]
State after:
case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : g • B ∩ B = ∅
⊢ a ∈ g • B ∧ a ∈ B

State before:
case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : g • B ∩ B = ∅
⊢ a ∈ g • B ∧ a ∈ B
Tactic:
constructor
State after:
case inr.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : g • B ∩ B = ∅
⊢ a ∈ g • B

case inr.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : g • B ∩ B = ∅
⊢ a ∈ B

State before:
case inr.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : g • B ∩ B = ∅
⊢ a ∈ g • B

case inr.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : g • B ∩ B = ∅
⊢ a ∈ B
Tactic:
rw [← hg]
State after:
case inr.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : g • B ∩ B = ∅
⊢ g • a ∈ g • B

case inr.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : g • B ∩ B = ∅
⊢ a ∈ B

State before:
case inr.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : g • B ∩ B = ∅
⊢ g • a ∈ g • B

case inr.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : g • B ∩ B = ∅
⊢ a ∈ B
Tactic:
rw [Set.smul_mem_smul_set_iff]
State after:
case inr.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : g • B ∩ B = ∅
⊢ a ∈ B

case inr.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : g • B ∩ B = ∅
⊢ a ∈ B

State before:
case inr.left
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : g • B ∩ B = ∅
⊢ a ∈ B

case inr.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : g • B ∩ B = ∅
⊢ a ∈ B
Tactic:
exact ha
State after:
case inr.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : g • B ∩ B = ∅
⊢ a ∈ B

State before:
case inr.right
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g • a = a
h' : g • B ∩ B = ∅
⊢ a ∈ B
Tactic:
exact ha
State after:
no goals