awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
A : Set α
hA₀ : MeasurableSet A
hA : ∀ (g : G), (fun (x : α) ↦ g • x) ⁻¹' A = A
⊢ ∫⁻ (x : α) in s, A.indicator 1 x ∂μ = ∫⁻ (x : α) in t, A.indicator 1 x ∂μ

Tactic:
have : ∫⁻ x in s, A.indicator 1 x ∂μ = ∫⁻ x in t, A.indicator 1 x ∂μ := by
    refine hs.setLIntegral_eq ht (Set.indicator A fun _ => 1) fun g x ↦ ?_
    convert! (Set.indicator_comp_right (g • · : α → α) (g := fun _ ↦ (1 : ℝ≥0∞))).symm
    rw [hA g]
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
A : Set α
hA₀ : MeasurableSet A
hA : ∀ (g : G), (fun (x : α) ↦ g • x) ⁻¹' A = A
this : ∫⁻ (x : α) in s, A.indicator 1 x ∂μ = ∫⁻ (x : α) in t, A.indicator 1 x ∂μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (A ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (A ∩ t) : ℝ≥0∞)

Tactic:
simpa [Measure.restrict_apply hA₀, lintegral_indicator hA₀] using this

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.lintegral_indicator
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simpa only [setLIntegral_one] using hs.setLIntegral_eq ht (fun _ => 1) fun _ _ => rfl

Premises used: MeasureTheory.IsFundamentalDomain.setLIntegral_eq, MeasureTheory.setLIntegral_one, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
β : Type u_6
inst_6 : TopologicalSpace β
inst_7 : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ AEStronglyMeasurable f (μ.restrict s) ↔
    AEStronglyMeasurable (m₀ := inst_2) f (sum fun (g : G) ↦ μ.restrict (g • t ∩ s))

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

Premises used: MeasureTheory.IsFundamentalDomain.restrict_restrict, LE.le.absolutelyContinuous, MeasureTheory.Measure.restrict_le_self, MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
β : Type u_6
inst_6 : TopologicalSpace β
inst_7 : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ AEStronglyMeasurable (m₀ := inst_2) f (sum fun (g : 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]

Premises used: aestronglyMeasurable_sum_measure_iff, Set.smul_set_inter, smul_inv_smul, Set.inter_comm
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
β : Type u_6
inst_6 : TopologicalSpace β
inst_7 : 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]

Premises used: inv_inv
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
β : Type u_6
inst_6 : TopologicalSpace β
inst_7 : 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:
forall_congr' fun g => ?_

Premises used: forall_congr'
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
β : Type u_6
inst_6 : TopologicalSpace β
inst_7 : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
refine :
  ∀ (g : G), AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g • s ∩ t))) ↔ AEStronglyMeasurable f (μ.restrict (g • s ∩ t))
⊢ (∀ (g : G), AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g • s ∩ t)))) ↔
    ∀ (g : G), AEStronglyMeasurable f (μ.restrict (g • s ∩ t))

Tactic:
refine forall_congr' fun g => ?_

Premises used: forall_congr'
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
β : Type u_6
inst_6 : TopologicalSpace β
inst_7 : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
g : G
⊢ MeasurableEmbedding (β := α) fun (x : α) ↦ g⁻¹ • x

Tactic:
have he : MeasurableEmbedding (g⁻¹ • · : α → α) := measurableEmbedding_const_smul _
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
β : Type u_6
inst_6 : TopologicalSpace β
inst_7 : 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
rw :
  AEStronglyMeasurable (f ∘ fun (x : α) ↦ g⁻¹ • x) (μ.restrict (g • s ∩ t)) ↔
    AEStronglyMeasurable f (μ.restrict (g • s ∩ t))
⊢ 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]

Premises used: Set.image_smul, MeasureTheory.MeasurePreserving.restrict_image_emb, MeasureTheory.MeasurePreserving.aestronglyMeasurable_comp_iff, Inv.inv, MeasureTheory.measurePreserving_smul
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
β : Type u_6
inst_6 : TopologicalSpace β
inst_7 : 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]

Premises used: Function.comp_def
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
β : Type u_6
inst_6 : TopologicalSpace β
inst_7 : 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]

Premises used: aestronglyMeasurable_sum_measure_iff, MeasureTheory.IsFundamentalDomain.restrict_restrict, LE.le.absolutelyContinuous, MeasureTheory.Measure.restrict_le_self, MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hf₁ : ∀ (g : G) (x : α), ‖f (g • x)‖ₑ = ‖f x‖ₑ
⊢ ∫⁻ (a : α) in s, ‖f a‖ₑ ∂μ < ∞ ↔ ∫⁻ (a : α) in t, ‖f a‖ₑ ∂μ < ∞

Tactic:
rw [hs.setLIntegral_eq ht]

Premises used: MeasureTheory.IsFundamentalDomain.setLIntegral_eq
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
g : G
x : α
hf₁ hf₂ : ‖f x‖ₑ = ‖f x‖ₑ
⊢ ‖f (g • x)‖ₑ = ‖f x‖ₑ

Tactic:
rw [hf]
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ IntegrableOn f s μ ↔ IntegrableOn f t μ

Tactic:
and_congr (hs.aestronglyMeasurable_on_iff ht hf) (hs.hasFiniteIntegral_on_iff ht hf)

Premises used: MeasureTheory.IsFundamentalDomain.aestronglyMeasurable_on_iff, MeasureTheory.Integrable, MeasureTheory.IntegrableOn, MeasureTheory.IsFundamentalDomain.hasFiniteIntegral_on_iff, and_congr
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
ν : Measure α
inst_7 : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
f : α → E
hf : Integrable f ν
rw : @Integrable _ _ _ _ inst_2 f (sum fun (g : G) ↦ ν.restrict (g • s))
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : α), f x ∂ν) (∑' (g : G), ∫ (x : α) in g • s, f x ∂ν)

Tactic:
rw [← MeasureTheory.integral_sum_measure, h.sum_restrict_of_ac hν]

Premises used: MeasureTheory.integral_sum_measure, MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
ν : Measure α
inst_7 : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
f : α → E
hf rw : Integrable f ν
⊢ @Integrable _ _ _ _ inst_2 f (sum fun (g : G) ↦ ν.restrict (g • s))

Tactic:
rw [h.sum_restrict_of_ac hν]

Premises used: MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
ν : Measure α
inst_7 : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
f : α → E
hf : Integrable f ν
⊢ Integrable f ν

Tactic:
hf
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
ν : Measure α
inst_7 : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
f : α → E
hf : Integrable f ν
⊢ Integrable f ν

Tactic:
exact hf
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
f : α → E
hf : Integrable f μ
⊢ μ ≪ μ

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
f : α → E
hf : Integrable f μ
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : α), f x ∂μ) (∑' (g : G), ∫ (x : α) in s, f (g⁻¹ • x) ∂μ)

Tactic:
calc
    ∫ x, f x ∂μ = ∑' g : G, ∫ x in g • s, f x ∂μ := h.integral_eq_tsum f hf
    _ = ∑' g : G, ∫ x in g⁻¹ • s, f x ∂μ := ((Equiv.inv G).tsum_eq _).symm
    _ = ∑' g : G, ∫ x in s, f (g⁻¹ • x) ∂μ := tsum_congr fun g =>
      (measurePreserving_smul g⁻¹ μ).setIntegral_image_emb (measurableEmbedding_const_smul _) _ _

Premises used: Trans.trans, Equiv.inv, tsum_congr, MeasureTheory.MeasurePreserving.setIntegral_image_emb, Equiv.tsum_eq, measurableEmbedding_const_smul, Inv.inv, MeasureTheory.measurePreserving_smul, Eq.symm, MeasureTheory.IsFundamentalDomain.integral_eq_tsum
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
f : α → E
hf : Integrable f μ
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : α), f x ∂μ) (∑' (g : G), ∫ (x : α) in s, f (g • x) ∂μ)

Tactic:
(integral_eq_tsum' h f hf).trans ((Equiv.inv G).tsum_eq (fun g ↦ ∫ (x : α) in s, f (g • x) ∂μ))

Premises used: Equiv.inv, Equiv.tsum_eq, MeasureTheory.Measure.restrict, MeasureTheory.integral, HSMul.hSMul, MeasureTheory.IsFundamentalDomain.integral_eq_tsum', Eq.trans
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
f : α → E
t : Set α
hf : IntegrableOn f t μ
⊢ Eq.{u_5 + 1} (α := E) (∑' (g : G), ∫ (x : α) in g • s, f x ∂μ.restrict t) (∑' (g : G), ∫ (x : α) in t ∩ g • s, f x ∂μ)

Tactic:
simp only [h.restrict_restrict, inter_comm]

Premises used: MeasureTheory.IsFundamentalDomain.restrict_restrict, Set.inter_comm
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
f : α → E
t : Set α
hf : IntegrableOn f t μ
⊢ Eq.{u_5 + 1} (α := E) (∑' (g : G), ∫ (x : α) in t ∩ g⁻¹ • s, f x ∂μ)
    (∑' (g : G), ∫ (x : α) in g⁻¹ • (g • t ∩ s), f x ∂μ)

Tactic:
simp only [smul_set_inter, inv_smul_smul]

Premises used: Set.smul_set_inter, inv_smul_smul
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
pos : ∀ (hfs : IntegrableOn f s μ), Eq.{u_5 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in t, f x ∂μ)
neg : ∀ (hfs : ¬IntegrableOn f s μ), Eq.{u_5 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in t, f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in t, f x ∂μ)

Tactic:
by_cases hfs : IntegrableOn f s μ

Premises used: MeasureTheory.IntegrableOn
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs rwa rwa₁ rwa₂ rwa₃ : IntegrableOn f s μ
⊢ IntegrableOn f t μ

Tactic:
rwa [ht.integrableOn_iff hs hf]

Premises used: MeasureTheory.IsFundamentalDomain.integrableOn_iff
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : IntegrableOn f s μ
⊢ IntegrableOn f t μ

Tactic:
have hft : IntegrableOn f t μ := by rwa [ht.integrableOn_iff hs hf]
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∑' (g : G), ∫ (x : α) in s ∩ g • t, f x ∂μ)

Tactic:
ht.setIntegral_eq_tsum hfs

Premises used: MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
⊢ Eq.{u_5 + 1} (α := E) (∑' (g : G), ∫ (x : α) in s ∩ g • t, f x ∂μ)
    (∑' (g : G), ∫ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ)

Tactic:
simp only [hf, inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
⊢ Eq.{u_5 + 1} (α := E) (∑' (g : G), ∫ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ) (∫ (x : α) in t, f x ∂μ)

Tactic:
(hs.setIntegral_eq_tsum' hft).symm

Premises used: MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum', Eq.symm
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
x :
  Eq.{u_5 + 1} (α := E) (∑' (g : G), ∫ (x : α) in s ∩ g • t, f x ∂μ)
    (∑' (g : G), ∫ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in t, f x ∂μ)

Tactic:
calc
      ∫ x in s, f x ∂μ = ∑' g : G, ∫ x in s ∩ g • t, f x ∂μ := ht.setIntegral_eq_tsum hfs
      _ = ∑' g : G, ∫ x in g • t ∩ s, f (g⁻¹ • x) ∂μ := by simp only [hf, inter_comm]
      _ = ∫ x in t, f x ∂μ := (hs.setIntegral_eq_tsum' hft).symm

Premises used: MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum', MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum, Eq.symm
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : ¬IntegrableOn f s μ
neg : ¬Integrable f (μ.restrict t)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in t, f x ∂μ)

Tactic:
rw [integral_undef hfs, integral_undef]

Premises used: MeasureTheory.integral_undef
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : ¬IntegrableOn f s μ
neg neg₁ neg₂ neg₃ : ∀ (hfs : ¬IntegrableOn f t μ), ¬Integrable f (μ.restrict t)
⊢ ¬Integrable f (μ.restrict t)

Tactic:
rwa [hs.integrableOn_iff ht hf] at hfs

Premises used: MeasureTheory.IsFundamentalDomain.integrableOn_iff