-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem setIntegral_eq (hs : IsFundamentalDomain G s μ) (ht : IsFundamentalDomain G t μ)
    {f : α → E} (hf : ∀ (g : G) (x), f (g • x) = f x) : ∫ x in s, f x ∂μ = ∫ x in t, f x ∂μ

Proof state:
case neg
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : 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 μ
⊢ ¬Integrable f (μ.restrict t)

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

Result:
no goals

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

Result:
no goals

Proof state:
case neg
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : 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 μ
⊢ ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in t, f x ∂μ

Tactic:
rw [integral_undef hfs, integral_undef]

Result:
case neg
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : 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 μ
⊢ ¬Integrable f (μ.restrict t)

Proof state:
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in t, f x ∂μ

Tactic:
by_cases hfs : IntegrableOn f s μ

Result:
case pos
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : 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 μ
⊢ ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in t, f x ∂μ

case neg
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : 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 μ
⊢ ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in t, f x ∂μ

Proof state:
case pos
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : 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 μ
⊢ ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in t, f x ∂μ

Tactic:
have hft : IntegrableOn f t μ := by rwa [ht.integrableOn_iff hs hf]

Result:
case pos
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : 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 : α) in s, f x ∂μ = ∫ (x : α) in t, f x ∂μ

Proof state:
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : 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 μ
⊢ ∑' (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]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : 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:
rwa [ht.integrableOn_iff hs hf]

Result:
no goals