Theorem: MulAction.le_stabilizer_iff_smul_le (Jordan/Mathlib/Stabilizer.lean)

State before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ H ≤ stabilizer G s ↔ ∀ g ∈ H, g • s ⊆ s
Tactic:
constructor
State after:
case mp
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ H ≤ stabilizer G s → ∀ g ∈ H, g • s ⊆ s

case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ (∀ g ∈ H, g • s ⊆ s) → H ≤ stabilizer G s

State before:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ (∀ g ∈ H, g • s ⊆ s) → H ≤ stabilizer G s
Tactic:
intro hyp
State after:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
⊢ H ≤ stabilizer G s

State before:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
⊢ H ≤ stabilizer G s
Tactic:
intro g hg
State after:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ g ∈ stabilizer G s

State before:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ g ∈ stabilizer G s
Tactic:
rw [mem_stabilizer_iff]
State after:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ g • s = s

State before:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ g • s = s
Tactic:
apply subset_antisymm
State after:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ g • s ⊆ s

case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ s ⊆ g • s

State before:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ g • s ⊆ s

case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ s ⊆ g • s
Tactic:
exact hyp g hg
State after:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ s ⊆ g • s

State before:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ s ⊆ g • s
Tactic:
intro x hx
State after:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ x ∈ g • s

State before:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ x ∈ g • s
Tactic:
use g⁻¹ • x
State after:
case h
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ s ∧ (fun x => g • x) (g⁻¹ • x) = x

State before:
case h
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ s ∧ (fun x => g • x) (g⁻¹ • x) = x
Tactic:
constructor
State after:
case h.left
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ s

case h.right
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ (fun x => g • x) (g⁻¹ • x) = x

State before:
case h.left
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ s

case h.right
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ (fun x => g • x) (g⁻¹ • x) = x
Tactic:
apply hyp g⁻¹ (inv_mem hg)
State after:
case h.left.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ g⁻¹ • s

case h.right
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ (fun x => g • x) (g⁻¹ • x) = x

State before:
case h.left.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ g⁻¹ • s

case h.right
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ (fun x => g • x) (g⁻¹ • x) = x
Tactic:
simp only [Set.smul_mem_smul_set_iff, hx]
State after:
case h.right
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ (fun x => g • x) (g⁻¹ • x) = x

State before:
case h.right
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ (fun x => g • x) (g⁻¹ • x) = x
Tactic:
simp only [smul_inv_smul]
State after:
no goals

State before:
case mp
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ H ≤ stabilizer G s → ∀ g ∈ H, g • s ⊆ s
Tactic:
intro hyp g hg
State after:
case mp
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ g • s ⊆ s

State before:
case mp
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ g • s ⊆ s
Tactic:
apply Eq.subset
State after:
case mp.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ g • s = s

State before:
case mp.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ g • s = s
Tactic:
rw [← mem_stabilizer_iff]
State after:
case mp.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ g ∈ stabilizer G s

State before:
case mp.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ g ∈ stabilizer G s
Tactic:
exact hyp hg
State after:
no goals