-- 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 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)

Tactic:
exact fun g ↦ MeasurableSet.const_smul (hA_meas n) g

Result:
no goals

Proof state:
case mk.refine_1
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
n : ℕ
⊢ μ ((fun n => Quotient.mk α_mod_G '' A n) n) < ⊤

Tactic:
obtain ⟨s, fund_dom_s⟩ := i'

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 ν
⊢ μ ((fun n => Quotient.mk α_mod_G '' A n) n) < ⊤

Proof state:
case mk.refine_2
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
⊢ ⋃ i, (fun n => Quotient.mk α_mod_G '' A n) i = univ

Tactic:
rw [← image_iUnion, hA']

Result:
case mk.refine_2
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
⊢ Quotient.mk α_mod_G '' univ = univ

Proof state:
case mk.refine_2
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
⊢ Quotient.mk α_mod_G '' univ = univ

Tactic:
refine image_univ_of_surjective (by convert Quotient.mk'_surjective)

Result:
no goals

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 ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), ν (A i) < ⊤
hA' : ⋃ i, A i = univ
⊢ Surjective (Quotient.mk α_mod_G)

Tactic:
convert Quotient.mk'_surjective

Result:
no goals

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 (Quotient.mk α_mod_G '' A n)

Tactic:
rw [measurableSet_quotient, Quotient.mk''_eq_mk, this]

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 ν
μ : 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)

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) < ⊤

Tactic:
refine lt_of_le_of_lt ?_ (hA 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) ≤ ν (A n)