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

State before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
⊢ g ∈ stabilizer G s ↔ s ⊆ g • s
Tactic:
rw [← @inv_mem_iff, mem_stabilizer_of_finite_iff_smul_le G s hs]
State after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
⊢ g⁻¹ • s ⊆ s ↔ s ⊆ g • s

State before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
⊢ g⁻¹ • s ⊆ s ↔ s ⊆ g • s
Tactic:
exact Set.subset_set_smul_iff.symm
State after:
no goals