-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
/-- If a measure `μ` on a quotient satisfies `QuotientMeasureEqMeasurePreimage` with respect to a
sigma-finite measure `ν`, then it is itself `SigmaFinite`. -/
@[to_additive]
lemma QuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient
    [i : SigmaFinite ν] [i' : HasFundamentalDomain G α ν]
    (μ : Measure (Quotient α_mod_G)) [QuotientMeasureEqMeasurePreimage ν μ] :
    SigmaFinite μ

Proof state:
case mk
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
ν : Measure α
inst✝⁴ : SMulInvariantMeasure G α ν
inst✝³ : Countable G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), A i ∈ {s | MeasurableSet s}
hA : ∀ (i : ℕ), ν (A i) < ⊤
hA' : ⋃ i, A i = univ
⊢ Nonempty (μ.FiniteSpanningSetsIn univ)

Tactic:
simp only [mem_setOf_eq] at hA_meas

Result:
case mk
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
ν : Measure α
inst✝⁴ : SMulInvariantMeasure G α ν
inst✝³ : Countable G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), ν (A i) < ⊤
hA' : ⋃ i, A i = univ
⊢ Nonempty (μ.FiniteSpanningSetsIn univ)

Proof state:
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
ν : Measure α
inst✝⁴ : SMulInvariantMeasure G α ν
inst✝³ : Countable G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
⊢ SigmaFinite μ

Tactic:
rw [sigmaFinite_iff]

Result:
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
ν : Measure α
inst✝⁴ : SMulInvariantMeasure G α ν
inst✝³ : Countable G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
⊢ Nonempty (μ.FiniteSpanningSetsIn univ)

Proof state:
case mk.refine_1.mk.intro
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
ν : Measure α
inst✝⁴ : SMulInvariantMeasure G α ν
inst✝³ : Countable G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), ν (A i) < ⊤
hA' : ⋃ i, A i = univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' (Quotient.mk α_mod_G '' A n) = ⋃ g, (fun x => g • x) '' A n
measπAn : MeasurableSet (Quotient.mk α_mod_G '' A n)
⊢ ν (⋃ i, (fun x => i • x) '' A n ∩ s) ≤ ν (A n)

Tactic:
rw [fund_dom_s.measure_eq_tsum (A n)]

Result:
case mk.refine_1.mk.intro
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
ν : Measure α
inst✝⁴ : SMulInvariantMeasure G α ν
inst✝³ : Countable G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), ν (A i) < ⊤
hA' : ⋃ i, A i = univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' (Quotient.mk α_mod_G '' A n) = ⋃ g, (fun x => g • x) '' A n
measπAn : MeasurableSet (Quotient.mk α_mod_G '' A n)
⊢ ν (⋃ i, (fun x => i • x) '' A n ∩ s) ≤ ∑' (g : G), ν (g • A n ∩ s)

Proof state:
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
ν : Measure α
inst✝⁴ : SMulInvariantMeasure G α ν
inst✝³ : Countable G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), ν (A i) < ⊤
hA' : ⋃ i, A i = univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' (Quotient.mk α_mod_G '' A n) = ⋃ g, (fun x => g • x) '' A n
x✝ : Setoid α := α_mod_G
⊢ MeasurableSet (⋃ g, (fun x => g • x) '' A n)

Tactic:
apply MeasurableSet.iUnion

Result:
case h
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
ν : Measure α
inst✝⁴ : SMulInvariantMeasure G α ν
inst✝³ : Countable G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), ν (A i) < ⊤
hA' : ⋃ i, A i = univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' (Quotient.mk α_mod_G '' A n) = ⋃ g, (fun x => g • x) '' A n
x✝ : Setoid α := α_mod_G
⊢ ∀ (b : G), MeasurableSet ((fun x => b • x) '' A n)

Proof state:
case mk.refine_1.mk.intro
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
ν : Measure α
inst✝⁴ : SMulInvariantMeasure G α ν
inst✝³ : Countable G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), ν (A i) < ⊤
hA' : ⋃ i, A i = univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' (Quotient.mk α_mod_G '' A n) = ⋃ g, (fun x => g • x) '' A n
⊢ μ ((fun n => Quotient.mk α_mod_G '' A n) n) < ⊤

Tactic:
have measπAn : MeasurableSet (π '' A n) := by
  let _ : Setoid α := α_mod_G
  rw [measurableSet_quotient, Quotient.mk''_eq_mk, this]
  apply MeasurableSet.iUnion
  exact fun g ↦ MeasurableSet.const_smul (hA_meas n) g

Result:
case mk.refine_1.mk.intro
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
ν : Measure α
inst✝⁴ : SMulInvariantMeasure G α ν
inst✝³ : Countable G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), ν (A i) < ⊤
hA' : ⋃ i, A i = univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' (Quotient.mk α_mod_G '' A n) = ⋃ g, (fun x => g • x) '' A n
measπAn : MeasurableSet (Quotient.mk α_mod_G '' A n)
⊢ μ ((fun n => Quotient.mk α_mod_G '' A n) n) < ⊤

Proof state:
case mk.refine_1.mk.intro
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
ν : Measure α
inst✝⁴ : SMulInvariantMeasure G α ν
inst✝³ : Countable G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), ν (A i) < ⊤
hA' : ⋃ i, A i = univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' (Quotient.mk α_mod_G '' A n) = ⋃ g, (fun x => g • x) '' A n
measπAn : MeasurableSet (Quotient.mk α_mod_G '' A n)
⊢ ν (⋃ i, (fun x => i • x) '' A n ∩ s) ≤ ∑' (g : G), ν (g • A n ∩ s)

Tactic:
exact measure_iUnion_le _

Result:
no goals