-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem measure_eq_card_smul_of_smul_ae_eq_self [Finite G] (h : IsFundamentalDomain G s μ)
    (t : Set α) (ht : ∀ g : G, (g • t : Set α) =ᵐ[μ] t) : μ t = Nat.card G • μ (t ∩ s)

Proof state:
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : Finite G
h : IsFundamentalDomain G s μ
t : Set α
ht : ∀ (g : G), g • t =ᶠ[ae μ] t
⊢ μ t = Nat.card G • μ (t ∩ s)

Tactic:
haveI : Fintype G := Fintype.ofFinite G

Result:
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
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)

Proof state:
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
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)

Tactic:
replace ht : ∀ g : G, (g • t ∩ s : Set α) =ᵐ[μ] (t ∩ s : Set α) := fun g =>
  ae_eq_set_inter (ht g) (ae_eq_refl s)

Result:
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
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)

Proof state:
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
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)

Tactic:
simp_rw [measure_congr (ht _), tsum_fintype, Finset.sum_const, Nat.card_eq_fintype_card,
  Finset.card_univ]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
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)

Tactic:
rw [h.measure_eq_tsum]

Result:
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
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)