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

State before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
⊢ stabilizer G sᶜ = stabilizer G s
Tactic:
have : ∀ s : Set α, stabilizer G s ≤ stabilizer G (sᶜ) :=
  by
  intro s g h
  rw [mem_stabilizer_iff, smul_compl_set, mem_stabilizer_iff.1 h]
State after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
this : ∀ (s : Set α), stabilizer G s ≤ stabilizer G sᶜ
⊢ stabilizer G sᶜ = stabilizer G s

State before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
this : ∀ (s : Set α), stabilizer G s ≤ stabilizer G sᶜ
⊢ stabilizer G sᶜ = stabilizer G s
Tactic:
refine' le_antisymm _ (this _)
State after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
this : ∀ (s : Set α), stabilizer G s ≤ stabilizer G sᶜ
⊢ stabilizer G sᶜ ≤ stabilizer G s

State before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
this : ∀ (s : Set α), stabilizer G s ≤ stabilizer G sᶜ
⊢ stabilizer G sᶜ ≤ stabilizer G s
Tactic:
convert this _
State after:
case h.e'_4.h.e'_5
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
this : ∀ (s : Set α), stabilizer G s ≤ stabilizer G sᶜ
⊢ s = sᶜᶜ

State before:
case h.e'_4.h.e'_5
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
this : ∀ (s : Set α), stabilizer G s ≤ stabilizer G sᶜ
⊢ s = sᶜᶜ
Tactic:
exact (compl_compl _).symm
State after:
no goals

State before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
⊢ ∀ (s : Set α), stabilizer G s ≤ stabilizer G sᶜ
Tactic:
intro s g h
State after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s✝ s : Set α
g : G
h : g ∈ stabilizer G s
⊢ g ∈ stabilizer G sᶜ

State before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s✝ s : Set α
g : G
h : g ∈ stabilizer G s
⊢ g ∈ stabilizer G sᶜ
Tactic:
rw [mem_stabilizer_iff, smul_compl_set, mem_stabilizer_iff.1 h]
State after:
no goals