no goals
G : Type u_1
H : Type ?u.157160
α : Type u_2
β : Type ?u.157166
E : Type ?u.157169
inst✝¹⁰ : Group G
inst✝⁹ : Group H
inst✝⁸ : MulAction G α
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MulAction H β
inst✝⁵ : MeasurableSpace β
inst✝⁴ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
ν : Measure α
h : IsFundamentalDomain G s
hν : ν ≪ μ
⊢ (sum fun g => Measure.restrict ν (g • s)) = ν
rw [← restrict_iUnion_ae (h.aedisjoint.mono fun i j h => hν h) fun g =>
    (h.nullMeasurableSet_smul g).mono_ac hν,
  restrict_congr_set (hν h.iUnion_smul_ae_eq), restrict_univ]