no goals
G : Type u_3
H : Type u_1
α : Type u_2
β : Type ?u.505777
E : Type ?u.505780
inst✝⁴ : Group G
inst✝³ : MulAction G α
s : Set α
x : α
inst✝² : Group H
inst✝¹ : MulAction H α
inst✝ : SMulCommClass H G α
g : H
⊢ fundamentalInterior G (g • s) = g • fundamentalInterior G s
simp_rw [fundamentalInterior, smul_set_sdiff, smul_set_Union, smul_comm g (_ : G) (_ : Set α)]