-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem aEStronglyMeasurable_on_iff {β : Type*} [TopologicalSpace β]
    [PseudoMetrizableSpace β] (hs : IsFundamentalDomain G s μ) (ht : IsFundamentalDomain G t μ)
    {f : α → β} (hf : ∀ (g : G) (x), f (g • x) = f x) :
    AEStronglyMeasurable f (μ.restrict s) ↔ AEStronglyMeasurable f (μ.restrict t) :=
  calc
    AEStronglyMeasurable f (μ.restrict s) ↔
        AEStronglyMeasurable f (Measure.sum fun g : G => μ.restrict (g • t ∩ s))

Proof state:
G : Type u_1
α : Type u_3
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ (∀ (g : G), AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g • s ∩ t)))) ↔
    ∀ (g : G), AEStronglyMeasurable f (μ.restrict (g • s ∩ t))

Tactic:
refine forall_congr' fun g => ?_

Result:
G : Type u_1
α : Type u_3
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
g : G
⊢ AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g • s ∩ t))) ↔ AEStronglyMeasurable f (μ.restrict (g • s ∩ t))

Proof state:
G : Type u_1
α : Type u_3
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
g : G
he : MeasurableEmbedding fun x => g⁻¹ • x
⊢ AEStronglyMeasurable (f ∘ fun x => g⁻¹ • x) (μ.restrict (g • s ∩ t)) ↔ AEStronglyMeasurable f (μ.restrict (g • s ∩ t))

Tactic:
simp only [Function.comp_def, hf]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ AEStronglyMeasurable f (μ.restrict s) ↔ AEStronglyMeasurable f (sum fun g => μ.restrict (g • t ∩ s))

Tactic:
simp only [← ht.restrict_restrict,
  ht.sum_restrict_of_ac restrict_le_self.absolutelyContinuous]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ AEStronglyMeasurable f (sum fun g => μ.restrict (g • t ∩ s)) ↔
    ∀ (g : G), AEStronglyMeasurable f (μ.restrict (g • (g⁻¹ • s ∩ t)))

Tactic:
simp only [smul_set_inter, inter_comm, smul_inv_smul, aestronglyMeasurable_sum_measure_iff]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ (∀ (g : G), AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g⁻¹⁻¹ • s ∩ t)))) ↔
    ∀ (g : G), AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g • s ∩ t)))

Tactic:
simp only [inv_inv]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ (∀ (g : G), AEStronglyMeasurable f (μ.restrict (g • s ∩ t))) ↔ AEStronglyMeasurable f (μ.restrict t)

Tactic:
simp only [← aestronglyMeasurable_sum_measure_iff, ← hs.restrict_restrict,
  hs.sum_restrict_of_ac restrict_le_self.absolutelyContinuous]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
g : G
he : MeasurableEmbedding fun x => g⁻¹ • x
⊢ AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g • s ∩ t))) ↔ AEStronglyMeasurable f (μ.restrict (g • s ∩ t))

Tactic:
rw [← image_smul, ← ((measurePreserving_smul g⁻¹ μ).restrict_image_emb he
  _).aestronglyMeasurable_comp_iff he]

Result:
G : Type u_1
α : Type u_3
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
g : G
he : MeasurableEmbedding fun x => g⁻¹ • x
⊢ AEStronglyMeasurable (f ∘ fun x => g⁻¹ • x) (μ.restrict (g • s ∩ t)) ↔ AEStronglyMeasurable f (μ.restrict (g • s ∩ t))