internlm/Lean-Github huggingface dataset:
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g : G
this : g • orbit (↥N) a = orbit (↥N) (g • a)
⊢ g • orbit (↥N) a = orbit (↥N) a ∨ Disjoint (g • orbit (↥N) a) (orbit (↥N) a)
Tactic:
rw [this]
Proof state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g : G
this : g • orbit (↥N) a = orbit (↥N) (g • a)
⊢ orbit (↥N) (g • a) = orbit (↥N) a ∨ Disjoint (orbit (↥N) (g • a)) (orbit (↥N) a)
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g : G
this : g • orbit (↥N) a = orbit (↥N) (g • a)
⊢ orbit (↥N) (g • a) = orbit (↥N) a ∨ Disjoint (orbit (↥N) (g • a)) (orbit (↥N) a)
Tactic:
apply orbit.equal_or_disjoint
Proof state after:
no goals
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g : G
x✝ : X
⊢ (∃ y, g • y • a = x✝) → ∃ y, y • g • a = x✝
Tactic:
rintro ⟨⟨k, hk⟩, rfl⟩
Proof state after:
case h.mp.intro.mk
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
⊢ ∃ y, y • g • a = g • { val := k, property := hk } • a
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
case h.mp.intro.mk
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
⊢ ∃ y, y • g • a = g • { val := k, property := hk } • a
Tactic:
suffices g * k * g⁻¹ ∈ N by
  use ⟨g * k * g⁻¹, this⟩
  change (g * k * g⁻¹) • g • a = g • k • a
  rw [smul_smul, inv_mul_cancel_right, ← smul_smul]
Proof state after:
case h.mp.intro.mk
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
⊢ g * k * g⁻¹ ∈ N
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
case h.mp.intro.mk
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
⊢ g * k * g⁻¹ ∈ N
Tactic:
apply nN.conj_mem
Proof state after:
case h.mp.intro.mk.a
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
⊢ k ∈ N
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
case h.mp.intro.mk.a
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
⊢ k ∈ N
Tactic:
exact hk
Proof state after:
no goals
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
this : g * k * g⁻¹ ∈ N
⊢ ∃ y, y • g • a = g • { val := k, property := hk } • a
Tactic:
use ⟨g * k * g⁻¹, this⟩
Proof state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
this : g * k * g⁻¹ ∈ N
⊢ { val := g * k * g⁻¹, property := this } • g • a = g • { val := k, property := hk } • a
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
this : g * k * g⁻¹ ∈ N
⊢ { val := g * k * g⁻¹, property := this } • g • a = g • { val := k, property := hk } • a
Tactic:
change (g * k * g⁻¹) • g • a = g • k • a
Proof state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
this : g * k * g⁻¹ ∈ N
⊢ (g * k * g⁻¹) • g • a = g • k • a
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
this : g * k * g⁻¹ ∈ N
⊢ (g * k * g⁻¹) • g • a = g • k • a
Tactic:
rw [smul_smul, inv_mul_cancel_right, ← smul_smul]
Proof state after:
no goals
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g : G
x✝ : X
⊢ (∃ y, y • g • a = x✝) → ∃ y, g • y • a = x✝
Tactic:
rintro ⟨⟨k, hk⟩, rfl⟩
Proof state after:
case h.mpr.intro.mk
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
⊢ ∃ y, g • y • a = { val := k, property := hk } • g • a
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
case h.mpr.intro.mk
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
⊢ ∃ y, g • y • a = { val := k, property := hk } • g • a
Tactic:
suffices g⁻¹ * k * g ∈ N by
  use ⟨g⁻¹ * k * g, this⟩
  change g • (g⁻¹ * k * g) • a = k • g • a
  simp only [← mul_assoc, ← smul_smul, smul_inv_smul, inv_inv]
Proof state after:
case h.mpr.intro.mk
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
⊢ g⁻¹ * k * g ∈ N
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
case h.mpr.intro.mk
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
⊢ g⁻¹ * k * g ∈ N
Tactic:
convert nN.conj_mem k hk g⁻¹
Proof state after:
case h.e'_4.h.e'_6
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
⊢ g = g⁻¹⁻¹
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
case h.e'_4.h.e'_6
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
⊢ g = g⁻¹⁻¹
Tactic:
rw [inv_inv]
Proof state after:
no goals
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
this : g⁻¹ * k * g ∈ N
⊢ ∃ y, g • y • a = { val := k, property := hk } • g • a
Tactic:
use ⟨g⁻¹ * k * g, this⟩
Proof state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
this : g⁻¹ * k * g ∈ N
⊢ g • { val := g⁻¹ * k * g, property := this } • a = { val := k, property := hk } • g • a
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
this : g⁻¹ * k * g ∈ N
⊢ g • { val := g⁻¹ * k * g, property := this } • a = { val := k, property := hk } • g • a
Tactic:
change g • (g⁻¹ * k * g) • a = k • g • a
Proof state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
this : g⁻¹ * k * g ∈ N
⊢ g • (g⁻¹ * k * g) • a = k • g • a
Theorem: MulAction.orbit.IsBlock_of_normal
Proof state before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : Subgroup.Normal N
a : X
g k : G
hk : k ∈ N
this : g⁻¹ * k * g ∈ N
⊢ g • (g⁻¹ * k * g) • a = k • g • a
Tactic:
simp only [← mul_assoc, ← smul_smul, smul_inv_smul, inv_inv]
Proof state after:
no goals
Theorem: MulAction.IsBlockSystem.of_normal
Proof 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
Proof 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
Theorem: MulAction.IsBlockSystem.of_normal
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsBlockSystem.of_normal
Proof 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
Proof 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
Theorem: MulAction.IsBlockSystem.of_normal
Proof 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⟩
Proof 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)
Theorem: MulAction.IsBlockSystem.of_normal
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsBlock_of_suborbit
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
⊢ IsBlock G (orbit (↥H) a)
Tactic:
rw [IsBlock.mk_subset]
Proof state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
⊢ ∀ {g : G} {b : X}, b ∈ orbit (↥H) a → b ∈ g • orbit (↥H) a → g • orbit (↥H) a ≤ orbit (↥H) a
Theorem: MulAction.IsBlock_of_suborbit
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
⊢ ∀ {g : G} {b : X}, b ∈ orbit (↥H) a → b ∈ g • orbit (↥H) a → g • orbit (↥H) a ≤ orbit (↥H) a
Tactic:
intro g b
Proof state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
b : X
⊢ b ∈ orbit (↥H) a → b ∈ g • orbit (↥H) a → g • orbit (↥H) a ≤ orbit (↥H) a
Theorem: MulAction.IsBlock_of_suborbit
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
b : X
⊢ b ∈ orbit (↥H) a → b ∈ g • orbit (↥H) a → g • orbit (↥H) a ≤ orbit (↥H) a
Tactic:
rintro ⟨h, rfl⟩
Proof state after:
case intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h : ↥H
⊢ (fun m => m • a) h ∈ g • orbit (↥H) a → g • orbit (↥H) a ≤ orbit (↥H) a
Theorem: MulAction.IsBlock_of_suborbit
Proof state before:
case intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h : ↥H
⊢ (fun m => m • a) h ∈ g • orbit (↥H) a → g • orbit (↥H) a ≤ orbit (↥H) a
Tactic:
simp
Proof state after:
case intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h : ↥H
⊢ h • a ∈ g • orbit (↥H) a → g • orbit (↥H) a ⊆ orbit (↥H) a
Theorem: MulAction.IsBlock_of_suborbit
Proof state before:
case intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h : ↥H
⊢ h • a ∈ g • orbit (↥H) a → g • orbit (↥H) a ⊆ orbit (↥H) a
Tactic:
intro hb'
Proof state after:
case intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h : ↥H
hb' : h • a ∈ g • orbit (↥H) a
⊢ g • orbit (↥H) a ⊆ orbit (↥H) a
Theorem: MulAction.IsBlock_of_suborbit
Proof state before:
case intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h : ↥H
hb' : h • a ∈ g • orbit (↥H) a
⊢ g • orbit (↥H) a ⊆ orbit (↥H) a
Tactic:
suffices g ∈ H by
  rw [← Subgroup.coe_mk H g this, ← Subgroup.smul_def]
  apply smul_orbit_subset
Proof state after:
case intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h : ↥H
hb' : h • a ∈ g • orbit (↥H) a
⊢ g ∈ H
Theorem: MulAction.IsBlock_of_suborbit
Proof state before:
case intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h : ↥H
hb' : h • a ∈ g • orbit (↥H) a
⊢ g ∈ H
Tactic:
rw [Set.mem_smul_set_iff_inv_smul_mem, Subgroup.smul_def, ← MulAction.mul_smul] at hb'
Proof state after:
case intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h : ↥H
hb' : (g⁻¹ * ↑h) • a ∈ orbit (↥H) a
⊢ g ∈ H
Theorem: MulAction.IsBlock_of_suborbit
Proof state before:
case intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h : ↥H
hb' : (g⁻¹ * ↑h) • a ∈ orbit (↥H) a
⊢ g ∈ H
Tactic:
obtain ⟨k : ↥H, hk⟩ := hb'
Proof state after:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (fun m => m • a) k = (g⁻¹ * ↑h) • a
⊢ g ∈ H
Theorem: MulAction.IsBlock_of_suborbit
Proof state before:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (fun m => m • a) k = (g⁻¹ * ↑h) • a
⊢ g ∈ H
Tactic:
simp only at hk
Proof state after:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : k • a = (g⁻¹ * ↑h) • a
⊢ g ∈ H
Theorem: MulAction.IsBlock_of_suborbit
Proof state before:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : k • a = (g⁻¹ * ↑h) • a
⊢ g ∈ H
Tactic:
rw [MulAction.mul_smul, ← smul_eq_iff_eq_inv_smul, ← inv_inv (h : G), ← smul_eq_iff_eq_inv_smul, ←
  MulAction.mul_smul, Subgroup.smul_def, ← MulAction.mul_smul] at hk
Proof state after:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : ((↑h)⁻¹ * g * ↑k) • a = a
⊢ g ∈ H
Theorem: MulAction.IsBlock_of_suborbit
Proof state before:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : ((↑h)⁻¹ * g * ↑k) • a = a
⊢ g ∈ H
Tactic:
rw [← mem_stabilizer_iff] at hk
Proof state after:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
⊢ g ∈ H
Theorem: MulAction.IsBlock_of_suborbit
Proof state before:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
⊢ g ∈ H
Tactic:
let hk' := hH hk
Proof state after:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
hk' : (↑h)⁻¹ * g * ↑k ∈ H := hH hk
⊢ g ∈ H
Theorem: MulAction.IsBlock_of_suborbit
Proof state before:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
hk' : (↑h)⁻¹ * g * ↑k ∈ H := hH hk
⊢ g ∈ H
Tactic:
rw [Subgroup.mul_mem_cancel_right, Subgroup.mul_mem_cancel_left] at hk'
Proof state after:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
hk' : g ∈ H
⊢ g ∈ H

case intro.intro.h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
hk' : (↑h)⁻¹ * g ∈ H
⊢ (↑h)⁻¹ ∈ H

case intro.intro.h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
hk' : (↑h)⁻¹ * g * ↑k ∈ H := hH hk
⊢ ↑k ∈ H
Theorem: MulAction.IsBlock_of_suborbit
Proof state before:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
hk' : g ∈ H
⊢ g ∈ H

case intro.intro.h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
hk' : (↑h)⁻¹ * g ∈ H
⊢ (↑h)⁻¹ ∈ H

case intro.intro.h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
hk' : (↑h)⁻¹ * g * ↑k ∈ H := hH hk
⊢ ↑k ∈ H
Tactic:
exact hk'
Proof state after:
case intro.intro.h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
hk' : (↑h)⁻¹ * g ∈ H
⊢ (↑h)⁻¹ ∈ H

case intro.intro.h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
hk' : (↑h)⁻¹ * g * ↑k ∈ H := hH hk
⊢ ↑k ∈ H
Theorem: MulAction.IsBlock_of_suborbit
Proof state before:
case intro.intro.h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
hk' : (↑h)⁻¹ * g ∈ H
⊢ (↑h)⁻¹ ∈ H

case intro.intro.h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
hk' : (↑h)⁻¹ * g * ↑k ∈ H := hH hk
⊢ ↑k ∈ H
Tactic:
apply Subgroup.inv_mem
Proof state after:
case intro.intro.h.a
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
hk' : (↑h)⁻¹ * g ∈ H
⊢ ↑h ∈ H

case intro.intro.h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
hk' : (↑h)⁻¹ * g * ↑k ∈ H := hH hk
⊢ ↑k ∈ H
Theorem: MulAction.IsBlock_of_suborbit
Proof state before:
case intro.intro.h.a
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
hk' : (↑h)⁻¹ * g ∈ H
⊢ ↑h ∈ H

case intro.intro.h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
hk' : (↑h)⁻¹ * g * ↑k ∈ H := hH hk
⊢ ↑k ∈ H
Tactic:
exact SetLike.coe_mem h
Proof state after:
case intro.intro.h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
hk' : (↑h)⁻¹ * g * ↑k ∈ H := hH hk
⊢ ↑k ∈ H
Theorem: MulAction.IsBlock_of_suborbit
Proof state before:
case intro.intro.h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h k : ↥H
hk : (↑h)⁻¹ * g * ↑k ∈ stabilizer G a
hk' : (↑h)⁻¹ * g * ↑k ∈ H := hH hk
⊢ ↑k ∈ H
Tactic:
exact SetLike.coe_mem k
Proof state after:
no goals
Theorem: MulAction.IsBlock_of_suborbit
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h : ↥H
hb' : h • a ∈ g • orbit (↥H) a
this : g ∈ H
⊢ g • orbit (↥H) a ⊆ orbit (↥H) a
Tactic:
rw [← Subgroup.coe_mk H g this, ← Subgroup.smul_def]
Proof state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h : ↥H
hb' : h • a ∈ g • orbit (↥H) a
this : g ∈ H
⊢ { val := g, property := this } • orbit (↥H) a ⊆ orbit (↥H) a
Theorem: MulAction.IsBlock_of_suborbit
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h : ↥H
hb' : h • a ∈ g • orbit (↥H) a
this : g ∈ H
⊢ { val := g, property := this } • orbit (↥H) a ⊆ orbit (↥H) a
Tactic:
apply smul_orbit_subset
Proof state after:
no goals
Theorem: MulAction.stabilizer_of_block
Proof 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
Proof 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
Theorem: MulAction.stabilizer_of_block
Proof 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 ⊢
Proof 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
Theorem: MulAction.stabilizer_of_block
Proof 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'
Proof 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
Theorem: MulAction.stabilizer_of_block
Proof 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
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' : Disjoint (g • B) B
⊢ g • B = 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' : Disjoint (g • B) B
⊢ g • B = B
Tactic:
exfalso
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' : Disjoint (g • B) B
⊢ False
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' : Disjoint (g • B) B
⊢ False
Tactic:
rw [← Set.mem_empty_iff_false a]
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' : Disjoint (g • B) B
⊢ a ∈ ∅
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' : Disjoint (g • B) B
⊢ a ∈ ∅
Tactic:
simp only [disjoint_iff, Set.inf_eq_inter, Set.bot_eq_empty] at h'
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 ∈ ∅