no goals
G : Type u_1
H : Type ?u.302877
α : Type u_2
β : Type ?u.302883
E : Type ?u.302886
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 α
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
⊢ ↑↑μ s = ↑↑μ t
simpa only [set_lintegral_one] using hs.set_lintegral_eq ht (fun _ => 1) fun _ _ => rfl