internlm/Lean-Github huggingface dataset:
Theorem: MulAction.stabilizer_of_block
Proof 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]
Proof 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
Theorem: MulAction.stabilizer_of_block
Proof 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
Proof 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
Theorem: MulAction.stabilizer_of_block
Proof 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]
Proof 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
Theorem: MulAction.stabilizer_of_block
Proof 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]
Proof 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
Theorem: MulAction.stabilizer_of_block
Proof 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
Proof 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
Theorem: MulAction.stabilizer_of_block
Proof 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
Proof state after:
no goals
Theorem: MulAction.block_of_stabilizer_of_block
Proof 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
Proof 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
Theorem: MulAction.block_of_stabilizer_of_block
Proof 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
Proof 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
Theorem: MulAction.block_of_stabilizer_of_block
Proof 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
Proof 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
Theorem: MulAction.block_of_stabilizer_of_block
Proof 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
Proof 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
Theorem: MulAction.block_of_stabilizer_of_block
Proof 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⟩
Proof 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
Theorem: MulAction.block_of_stabilizer_of_block
Proof 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]
Proof 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
Theorem: MulAction.block_of_stabilizer_of_block
Proof 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
Proof state after:
no goals
Theorem: MulAction.block_of_stabilizer_of_block
Proof 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⟩
Proof 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
Theorem: MulAction.block_of_stabilizer_of_block
Proof 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)
Proof 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
Theorem: MulAction.block_of_stabilizer_of_block
Proof 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
Proof 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
Theorem: MulAction.block_of_stabilizer_of_block
Proof 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
Proof 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
Theorem: MulAction.block_of_stabilizer_of_block
Proof 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
Proof 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
Theorem: MulAction.block_of_stabilizer_of_block
Proof 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
Proof state after:
no goals
Theorem: MulAction.block_of_stabilizer_of_block
Proof 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⟩
Proof state after:
no goals
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
⊢ stabilizer G (orbit (↥H) a) = H
Tactic:
ext g
Proof state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
⊢ g ∈ stabilizer G (orbit (↥H) a) ↔ g ∈ H
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
⊢ g ∈ stabilizer G (orbit (↥H) a) ↔ g ∈ H
Tactic:
constructor
Proof state after:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
⊢ g ∈ stabilizer G (orbit (↥H) a) → g ∈ H

case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
⊢ g ∈ H → g ∈ stabilizer G (orbit (↥H) a)
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
⊢ g ∈ H → g ∈ stabilizer G (orbit (↥H) a)
Tactic:
intro hg
Proof state after:
case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g ∈ H
⊢ g ∈ stabilizer G (orbit (↥H) a)
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g ∈ H
⊢ g ∈ stabilizer G (orbit (↥H) a)
Tactic:
rw [mem_stabilizer_iff]
Proof state after:
case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g ∈ H
⊢ g • orbit (↥H) a = orbit (↥H) a
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g ∈ H
⊢ g • orbit (↥H) a = orbit (↥H) a
Tactic:
rw [← Subgroup.coe_mk H g hg, ← Subgroup.smul_def]
Proof state after:
case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g ∈ H
⊢ { val := g, property := hg } • orbit (↥H) a = orbit (↥H) a
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g ∈ H
⊢ { val := g, property := hg } • orbit (↥H) a = orbit (↥H) a
Tactic:
apply smul_orbit
Proof state after:
no goals
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
⊢ g ∈ stabilizer G (orbit (↥H) a) → g ∈ H
Tactic:
intro hg
Proof state after:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g ∈ stabilizer G (orbit (↥H) a)
⊢ g ∈ H
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g ∈ stabilizer G (orbit (↥H) a)
⊢ g ∈ H
Tactic:
rw [mem_stabilizer_iff] at hg
Proof state after:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
⊢ g ∈ H
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
⊢ g ∈ H
Tactic:
suffices g • a ∈ orbit H a by
  rw [mem_orbit_iff] at this
  obtain ⟨k, hk⟩ := this
  rw [← Subgroup.mul_mem_cancel_left H (SetLike.coe_mem k⁻¹)]
  rw [smul_eq_iff_eq_inv_smul] at hk
  apply hH
  rw [mem_stabilizer_iff]; rw [MulAction.mul_smul]
  rw [← Subgroup.smul_def]; exact hk.symm
Proof state after:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
⊢ g • a ∈ orbit (↥H) a
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
⊢ g • a ∈ orbit (↥H) a
Tactic:
rw [← hg]
Proof state after:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
⊢ g • a ∈ g • orbit (↥H) a
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
⊢ g • a ∈ g • orbit (↥H) a
Tactic:
simp only [Set.smul_mem_smul_set_iff, mem_orbit_self]
Proof state after:
no goals
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
this : g • a ∈ orbit (↥H) a
⊢ g ∈ H
Tactic:
rw [mem_orbit_iff] at this
Proof state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
this : ∃ x, x • a = g • a
⊢ g ∈ H
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
this : ∃ x, x • a = g • a
⊢ g ∈ H
Tactic:
obtain ⟨k, hk⟩ := this
Proof state after:
case intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
k : ↥H
hk : k • a = g • a
⊢ g ∈ H
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
case intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
k : ↥H
hk : k • a = g • a
⊢ g ∈ H
Tactic:
rw [← Subgroup.mul_mem_cancel_left H (SetLike.coe_mem k⁻¹)]
Proof state after:
case intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
k : ↥H
hk : k • a = g • a
⊢ ↑k⁻¹ * g ∈ H
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
case intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
k : ↥H
hk : k • a = g • a
⊢ ↑k⁻¹ * g ∈ H
Tactic:
rw [smul_eq_iff_eq_inv_smul] at hk
Proof state after:
case intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
k : ↥H
hk : a = k⁻¹ • g • a
⊢ ↑k⁻¹ * g ∈ H
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
case intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
k : ↥H
hk : a = k⁻¹ • g • a
⊢ ↑k⁻¹ * g ∈ H
Tactic:
apply hH
Proof state after:
case intro.a
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
k : ↥H
hk : a = k⁻¹ • g • a
⊢ ↑k⁻¹ * g ∈ stabilizer G a
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
case intro.a
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
k : ↥H
hk : a = k⁻¹ • g • a
⊢ ↑k⁻¹ * g ∈ stabilizer G a
Tactic:
rw [mem_stabilizer_iff]
Proof state after:
case intro.a
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
k : ↥H
hk : a = k⁻¹ • g • a
⊢ (↑k⁻¹ * g) • a = a
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
case intro.a
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
k : ↥H
hk : a = k⁻¹ • g • a
⊢ (↑k⁻¹ * g) • a = a
Tactic:
rw [MulAction.mul_smul]
Proof state after:
case intro.a
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
k : ↥H
hk : a = k⁻¹ • g • a
⊢ ↑k⁻¹ • g • a = a
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
case intro.a
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
k : ↥H
hk : a = k⁻¹ • g • a
⊢ ↑k⁻¹ • g • a = a
Tactic:
rw [← Subgroup.smul_def]
Proof state after:
case intro.a
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
k : ↥H
hk : a = k⁻¹ • g • a
⊢ k⁻¹ • g • a = a
Theorem: MulAction.stabilizer_of_block_of_stabilizer
Proof state before:
case intro.a
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g • orbit (↥H) a = orbit (↥H) a
k : ↥H
hk : a = k⁻¹ • g • a
⊢ k⁻¹ • g • a = a
Tactic:
exact hk.symm
Proof state after:
no goals
Theorem: MulAction.Setoid.nat_sum
Proof state before:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
⊢ ∑ᶠ (x : ↑c), Nat.card ↑↑x = Nat.card α
Tactic:
classical
have := Fintype.ofFinite α
simp only [finsum_eq_sum_of_fintype, Nat.card_eq_fintype_card]
rw [← Fintype.card_sigma]
refine' Fintype.card_congr (Equiv.ofBijective (fun x => x.snd : (Σ a : ↥c, a) → α) _)
constructor
rintro ⟨⟨x, hx⟩, ⟨a, ha : a ∈ x⟩⟩ ⟨⟨y, hy⟩, ⟨b, hb : b ∈ y⟩⟩ hab
dsimp at hab
rw [hab] at ha
rw [Sigma.subtype_ext_iff]
simp only [Subtype.mk_eq_mk, Subtype.coe_mk]
apply And.intro _ hab
refine' ExistsUnique.unique (hc.2 b) _ _
simp only [exists_unique_iff_exists, exists_prop]
exact ⟨hx, ha⟩
simp only [exists_unique_iff_exists, exists_prop]
exact ⟨hy, hb⟩
intro a
obtain ⟨x, ⟨hx, ha : a ∈ x, _⟩, _⟩ := hc.2 a
use ⟨⟨x, hx⟩, ⟨a, ha⟩⟩
Proof state after:
no goals
Theorem: MulAction.Setoid.nat_sum
Proof state before:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
⊢ ∑ᶠ (x : ↑c), Nat.card ↑↑x = Nat.card α
Tactic:
have := Fintype.ofFinite α
Proof state after:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ ∑ᶠ (x : ↑c), Nat.card ↑↑x = Nat.card α
Theorem: MulAction.Setoid.nat_sum
Proof state before:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ ∑ᶠ (x : ↑c), Nat.card ↑↑x = Nat.card α
Tactic:
simp only [finsum_eq_sum_of_fintype, Nat.card_eq_fintype_card]
Proof state after:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ ∑ x : ↑c, Fintype.card ↑↑x = Fintype.card α
Theorem: MulAction.Setoid.nat_sum
Proof state before:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ ∑ x : ↑c, Fintype.card ↑↑x = Fintype.card α
Tactic:
rw [← Fintype.card_sigma]
Proof state after:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Fintype.card ((x : ↑c) × ↑↑x) = Fintype.card α
Theorem: MulAction.Setoid.nat_sum
Proof state before:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Fintype.card ((x : ↑c) × ↑↑x) = Fintype.card α
Tactic:
refine' Fintype.card_congr (Equiv.ofBijective (fun x => x.snd : (Σ a : ↥c, a) → α) _)
Proof state after:
G : Type ?u.182986
inst✝² : Group G
X : Type ?u.182992
inst✝¹ : MulAction G X
α : Type u_1
inst✝ : Finite α
c : Set (Set α)
hc : Setoid.IsPartition c
this : Fintype α
⊢ Function.Bijective fun x => ↑x.snd