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

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]
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

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
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

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⟩
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

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
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

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'
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

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
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

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'
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

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'
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

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
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

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
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

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
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

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
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

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'
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

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'
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

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
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

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
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

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
State after:
no goals

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]
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

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
State after:
no goals