G : Type u_1
H : Type ?u.251442
α : Type u_2
β : Type ?u.251448
E : Type ?u.251451
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✝ : Finite G
h : IsFundamentalDomain G s
t : Set α
ht : ∀ (g : G), g • t =ᶠ[ae μ] t
this : Fintype G
⊢ ↑↑μ t = Nat.card G • ↑↑μ (t ∩ s)
G : Type u_1
H : Type ?u.251442
α : Type u_2
β : Type ?u.251448
E : Type ?u.251451
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✝ : Finite G
h : IsFundamentalDomain G s
t : Set α
ht : ∀ (g : G), g • t =ᶠ[ae μ] t
⊢ ↑↑μ t = Nat.card G • ↑↑μ (t ∩ s)
haveI : Fintype G := Fintype.ofFinite G
G : Type u_1
H : Type ?u.251442
α : Type u_2
β : Type ?u.251448
E : Type ?u.251451
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✝ : Finite G
h : IsFundamentalDomain G s
t : Set α
ht : ∀ (g : G), g • t =ᶠ[ae μ] t
this : Fintype G
⊢ (∑' (g : G), ↑↑μ (g • t ∩ s)) = Nat.card G • ↑↑μ (t ∩ s)
G : Type u_1
H : Type ?u.251442
α : Type u_2
β : Type ?u.251448
E : Type ?u.251451
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✝ : Finite G
h : IsFundamentalDomain G s
t : Set α
ht : ∀ (g : G), g • t =ᶠ[ae μ] t
this : Fintype G
⊢ ↑↑μ t = Nat.card G • ↑↑μ (t ∩ s)
rw [h.measure_eq_tsum]
G : Type u_1
H : Type ?u.251442
α : Type u_2
β : Type ?u.251448
E : Type ?u.251451
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✝ : Finite G
h : IsFundamentalDomain G s
t : Set α
this : Fintype G
ht : ∀ (g : G), g • t ∩ s =ᶠ[ae μ] t ∩ s
⊢ (∑' (g : G), ↑↑μ (g • t ∩ s)) = Nat.card G • ↑↑μ (t ∩ s)
G : Type u_1
H : Type ?u.251442
α : Type u_2
β : Type ?u.251448
E : Type ?u.251451
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✝ : Finite G
h : IsFundamentalDomain G s
t : Set α
ht : ∀ (g : G), g • t =ᶠ[ae μ] t
this : Fintype G
⊢ (∑' (g : G), ↑↑μ (g • t ∩ s)) = Nat.card G • ↑↑μ (t ∩ s)
replace ht : ∀ g : G, (g • t ∩ s : Set α) =ᵐ[μ] (t ∩ s : Set α) := fun g =>
  ae_eq_set_inter (ht g) (ae_eq_refl s)
no goals
G : Type u_1
H : Type ?u.251442
α : Type u_2
β : Type ?u.251448
E : Type ?u.251451
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✝ : Finite G
h : IsFundamentalDomain G s
t : Set α
this : Fintype G
ht : ∀ (g : G), g • t ∩ s =ᶠ[ae μ] t ∩ s
⊢ (∑' (g : G), ↑↑μ (g • t ∩ s)) = Nat.card G • ↑↑μ (t ∩ s)
simp_rw [measure_congr (ht _), tsum_fintype, Finset.sum_const, Nat.card_eq_fintype_card,
  Finset.card_univ]