no goals
G : Type u_2
H : Type ?u.534094
α : Type u_1
β : Type ?u.534100
E : Type ?u.534103
inst✝³ : Countable G
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s
⊢ ↑↑μ (fundamentalFrontier G s) = 0
simpa only [fundamentalFrontier, iUnion₂_inter, measure_iUnion_null_iff', one_smul,
  measure_iUnion_null_iff, inter_comm s, Function.onFun] using fun g (hg : g ≠ 1) =>
  hs.aedisjoint hg