G : Type u_1
H✝ : Type ?u.223644
α : Type u_2
β : Type ?u.223650
E : Type ?u.223653
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ν : ν ≪ μ
t : Set α
H : Measure.restrict ν t ≪ μ
⊢ ↑↑ν t = ∑' (g : G), ↑↑ν (t ∩ g • s)
G : Type u_1
H : Type ?u.223644
α : Type u_2
β : Type ?u.223650
E : Type ?u.223653
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ν : ν ≪ μ
t : Set α
⊢ ↑↑ν t = ∑' (g : G), ↑↑ν (t ∩ g • s)
have H : ν.restrict t ≪ μ := Measure.restrict_le_self.absolutelyContinuous.trans hν
no goals
G : Type u_1
H✝ : Type ?u.223644
α : Type u_2
β : Type ?u.223650
E : Type ?u.223653
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ν : ν ≪ μ
t : Set α
H : Measure.restrict ν t ≪ μ
⊢ ↑↑ν t = ∑' (g : G), ↑↑ν (t ∩ g • s)
simpa only [set_lintegral_one, Pi.one_def,
  Measure.restrict_apply₀ ((h.nullMeasurableSet_smul _).mono_ac H), inter_comm] using
  h.lintegral_eq_tsum_of_ac H 1