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

State before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
⊢ fixingSubgroup G s ≤ stabilizer G s
Tactic:
intro k hk
State after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : k ∈ fixingSubgroup G s
⊢ k ∈ stabilizer G s

State before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : k ∈ fixingSubgroup G s
⊢ k ∈ stabilizer G s
Tactic:
rw [mem_fixingSubgroup_iff] at hk
State after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ k ∈ stabilizer G s

State before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ k ∈ stabilizer G s
Tactic:
rw [mem_stabilizer_iff]
State after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ k • s = s

State before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ k • s = s
Tactic:
change (fun x => k • x) '' s = s
State after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ (fun x => k • x) '' s = s

State before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ (fun x => k • x) '' s = s
Tactic:
conv_rhs => rw [← Set.image_id s]
State after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ (fun x => k • x) '' s = id '' s

State before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ (fun x => k • x) '' s = id '' s
Tactic:
apply Set.image_congr
State after:
case h
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ ∀ a ∈ s, k • a = id a

State before:
case h
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ ∀ a ∈ s, k • a = id a
Tactic:
simp only [id.def]
State after:
case h
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ ∀ a ∈ s, k • a = a

State before:
case h
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ ∀ a ∈ s, k • a = a
Tactic:
exact hk
State after:
no goals