-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem QuotientMeasureEqMeasurePreimage.covolume_ne_top
    (μ : Measure (Quotient α_mod_G)) [QuotientMeasureEqMeasurePreimage ν μ] [IsFiniteMeasure μ] :
    covolume G α ν < ∞

Proof state:
case pos.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 α
μ : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
hasFun : HasFundamentalDomain G α ν
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
⊢ covolume G α ν < ⊤

Tactic:
have H : μ univ < ∞ := IsFiniteMeasure.measure_univ_lt_top

Result:
case pos.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 α
μ : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
hasFun : HasFundamentalDomain G α ν
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
H : μ univ < ⊤
⊢ covolume G α ν < ⊤

Proof state:
case pos
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 α
μ : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
hasFun : HasFundamentalDomain G α ν
⊢ covolume G α ν < ⊤

Tactic:
obtain ⟨𝓕, h𝓕⟩ := hasFun.ExistsIsFundamentalDomain

Result:
case pos.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 α
μ : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
hasFun : HasFundamentalDomain G α ν
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
⊢ covolume G α ν < ⊤

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 α
μ : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
⊢ covolume G α ν < ⊤

Tactic:
by_cases hasFun : HasFundamentalDomain G α ν

Result:
case pos
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 α
μ : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
hasFun : HasFundamentalDomain G α ν
⊢ covolume G α ν < ⊤

case neg
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 α
μ : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
hasFun : ¬HasFundamentalDomain G α ν
⊢ covolume G α ν < ⊤

Proof state:
case pos.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 α
μ : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
hasFun : HasFundamentalDomain G α ν
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
H : μ univ < ⊤
⊢ covolume G α ν < ⊤

Tactic:
rw [h𝓕.projection_respects_measure_apply (μ := μ) MeasurableSet.univ] at H

Result:
case pos.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 α
μ : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
hasFun : HasFundamentalDomain G α ν
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
H : ν (Quotient.mk α_mod_G ⁻¹' univ ∩ 𝓕) < ⊤
⊢ covolume G α ν < ⊤

Proof state:
case neg
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 α
μ : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
hasFun : ¬HasFundamentalDomain G α ν
⊢ covolume G α ν < ⊤

Tactic:
simp [covolume, hasFun]

Result:
no goals

Proof state:
case pos.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 α
μ : Measure (Quotient α_mod_G)
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
hasFun : HasFundamentalDomain G α ν
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
H : ν (Quotient.mk α_mod_G ⁻¹' univ ∩ 𝓕) < ⊤
⊢ covolume G α ν < ⊤

Tactic:
simpa [h𝓕.covolume_eq_volume ν] using H

Result:
no goals