no goals
G : Type u_1
H : Type ?u.390629
α : Type u_2
β : Type ?u.390635
E : Type u_3
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 α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : IsFundamentalDomain G s
f : α → E
t : Set α
hf : IntegrableOn f t
⊢ (∑' (g : G), ∫ (x : α) in t ∩ g⁻¹ • s, f x ∂μ) = ∑' (g : G), ∫ (x : α) in g⁻¹ • (g • t ∩ s), f x ∂μ
simp only [smul_set_inter, inv_smul_smul]