no goals
G : Type u_2
H : Type ?u.475255
α : Type u_1
β : Type ?u.475261
E : Type ?u.475264
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x : α
⊢ x ∈ fundamentalInterior G s ↔ x ∈ s ∧ ∀ (g : G), g ≠ 1 → ¬x ∈ g • s
simp [fundamentalInterior]