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

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
⊢ orbit (↥(stabilizer G B)) a = B
Tactic:
ext x
State after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
⊢ x ∈ orbit (↥(stabilizer G B)) a ↔ x ∈ B

State before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
⊢ x ∈ orbit (↥(stabilizer G B)) a ↔ x ∈ B
Tactic:
constructor
State after:
case h.mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
⊢ x ∈ orbit (↥(stabilizer G B)) a → x ∈ B

case h.mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
⊢ x ∈ B → x ∈ orbit (↥(stabilizer G B)) a

State before:
case h.mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
⊢ x ∈ B → x ∈ orbit (↥(stabilizer G B)) a
Tactic:
intro hx
State after:
case h.mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
hx : x ∈ B
⊢ x ∈ orbit (↥(stabilizer G B)) a

State before:
case h.mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
hx : x ∈ B
⊢ x ∈ orbit (↥(stabilizer G B)) a
Tactic:
obtain ⟨k, rfl⟩ := exists_smul_eq G a x
State after:
case h.mpr.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
hx : k • a ∈ B
⊢ k • a ∈ orbit (↥(stabilizer G B)) a

State before:
case h.mpr.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
hx : k • a ∈ B
⊢ k • a ∈ orbit (↥(stabilizer G B)) a
Tactic:
suffices k ∈ stabilizer G B by
  exact ⟨⟨k, this⟩, rfl⟩
State after:
case h.mpr.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
hx : k • a ∈ B
⊢ k ∈ stabilizer G B

State before:
case h.mpr.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
hx : k • a ∈ B
⊢ k ∈ stabilizer G B
Tactic:
rw [mem_stabilizer_iff]
State after:
case h.mpr.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
hx : k • a ∈ B
⊢ k • B = B

State before:
case h.mpr.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
hx : k • a ∈ B
⊢ k • B = B
Tactic:
exact IsBlock.def_mem hB ha hx
State after:
no goals

State before:
case h.mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
⊢ x ∈ orbit (↥(stabilizer G B)) a → x ∈ B
Tactic:
rintro ⟨k, rfl⟩
State after:
case h.mp.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
k : ↥(stabilizer G B)
⊢ (fun m => m • a) k ∈ B

State before:
case h.mp.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
k : ↥(stabilizer G B)
⊢ (fun m => m • a) k ∈ B
Tactic:
let z := mem_stabilizer_iff.mp (SetLike.coe_mem k)
State after:
case h.mp.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
k : ↥(stabilizer G B)
z : ↑k • B = B := mem_stabilizer_iff.mp (SetLike.coe_mem k)
⊢ (fun m => m • a) k ∈ B

State before:
case h.mp.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
k : ↥(stabilizer G B)
z : ↑k • B = B := mem_stabilizer_iff.mp (SetLike.coe_mem k)
⊢ (fun m => m • a) k ∈ B
Tactic:
rw [← Subgroup.smul_def] at z
State after:
case h.mp.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
k : ↥(stabilizer G B)
z : k • B = B
⊢ (fun m => m • a) k ∈ B

State before:
case h.mp.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
k : ↥(stabilizer G B)
z : k • B = B
⊢ (fun m => m • a) k ∈ B
Tactic:
let zk : k • a ∈ k • B := Set.smul_mem_smul_set_iff.mpr ha
State after:
case h.mp.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
k : ↥(stabilizer G B)
z : k • B = B
zk : k • a ∈ k • B := Set.smul_mem_smul_set_iff.mpr ha
⊢ (fun m => m • a) k ∈ B

State before:
case h.mp.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
k : ↥(stabilizer G B)
z : k • B = B
zk : k • a ∈ k • B := Set.smul_mem_smul_set_iff.mpr ha
⊢ (fun m => m • a) k ∈ B
Tactic:
rw [z] at zk
State after:
case h.mp.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
k : ↥(stabilizer G B)
z : k • B = B
zk : k • a ∈ B
⊢ (fun m => m • a) k ∈ B

State before:
case h.mp.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
k : ↥(stabilizer G B)
z : k • B = B
zk : k • a ∈ B
⊢ (fun m => m • a) k ∈ B
Tactic:
exact zk
State after:
no goals

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
hx : k • a ∈ B
this : k ∈ stabilizer G B
⊢ k • a ∈ orbit (↥(stabilizer G B)) a
Tactic:
exact ⟨⟨k, this⟩, rfl⟩
State after:
no goals