Theorem: MulAction.orbit.IsBlock_of_normal (Jordan/Blocks.lean)

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
⊢ IsBlock G (orbit (↥N) a)
Tactic:
rw [IsBlock.def_one]
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), g • orbit (↥N) a = orbit (↥N) a ∨ Disjoint (g • orbit (↥N) a) (orbit (↥N) a)

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), g • orbit (↥N) a = orbit (↥N) a ∨ Disjoint (g • orbit (↥N) a) (orbit (↥N) a)
Tactic:
intro g
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
⊢ g • orbit (↥N) a = orbit (↥N) a ∨ Disjoint (g • orbit (↥N) a) (orbit (↥N) a)

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
⊢ g • orbit (↥N) a = orbit (↥N) a ∨ Disjoint (g • orbit (↥N) a) (orbit (↥N) a)
Tactic:
suffices g • orbit N a = orbit N (g • a) by rw [this]; apply orbit.equal_or_disjoint
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
⊢ g • orbit (↥N) a = orbit (↥N) (g • a)

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
⊢ g • orbit (↥N) a = orbit (↥N) (g • a)
Tactic:
change ((fun x : X => g • x) '' Set.range fun k : N => k • a) = Set.range fun k : N => k • g • a
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
⊢ ((fun x => g • x) '' Set.range fun k => k • a) = Set.range fun k => k • g • a

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
⊢ ((fun x => g • x) '' Set.range fun k => k • a) = Set.range fun k => k • g • a
Tactic:
simp only [Set.image_smul, Set.smul_set_range]
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
⊢ (Set.range fun i => g • i • a) = Set.range fun k => k • g • a

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
⊢ (Set.range fun i => g • i • a) = Set.range fun k => k • g • a
Tactic:
ext
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 : G
x✝ : X
⊢ (x✝ ∈ Set.range fun i => g • i • a) ↔ x✝ ∈ Set.range fun k => k • g • a

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 : G
x✝ : X
⊢ (x✝ ∈ Set.range fun i => g • i • a) ↔ x✝ ∈ Set.range fun k => k • g • a
Tactic:
simp only [Set.mem_range]
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 : G
x✝ : X
⊢ (∃ y, g • y • a = x✝) ↔ ∃ y, y • g • a = x✝

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 : G
x✝ : X
⊢ (∃ y, g • y • a = x✝) ↔ ∃ y, y • g • a = x✝
Tactic:
constructor
State after:
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✝

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✝

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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