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

Tactic:
rw [fund_dom_s.projection_respects_measure_apply (μ := μ) measπAn, this, iUnion_inter]

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

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

Tactic:
let _ : Setoid α := α_mod_G

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

Tactic:
have : π ⁻¹' (π '' (A n)) = _ := MulAction.quotient_preimage_image_eq_union_mul (A n) (G := 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
⊢ μ ((fun n => Quotient.mk α_mod_G '' A n) n) < ⊤

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
⊢ ∀ (i : ℕ), (fun n => Quotient.mk α_mod_G '' A n) i ∈ univ

Tactic:
simp

Result:
no goals

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 : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), ν (A i) < ⊤
hA' : ⋃ i, A i = univ
⊢ Nonempty (μ.FiniteSpanningSetsIn univ)

Tactic:
refine ⟨⟨fun n ↦ π '' (A n), by simp, fun n ↦ ?_, ?_⟩⟩

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

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

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 ν μ
⊢ Nonempty (μ.FiniteSpanningSetsIn univ)

Tactic:
obtain ⟨A, hA_meas, hA, hA'⟩ := Measure.toFiniteSpanningSetsIn (h := i)

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 : ℕ), A i ∈ {s | MeasurableSet s}
hA : ∀ (i : ℕ), ν (A i) < ⊤
hA' : ⋃ i, A i = univ
⊢ Nonempty (μ.FiniteSpanningSetsIn univ)