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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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