-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem IsFundamentalDomain.quotientMeasureEqMeasurePreimage_of_zero
    {s : Set α} (fund_dom_s : IsFundamentalDomain G s ν)
    (vol_s : ν s = 0) :
    QuotientMeasureEqMeasurePreimage ν (0 : Measure (Quotient α_mod_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 α
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
vol_s : ν s = 0
⊢ QuotientMeasureEqMeasurePreimage ν 0

Tactic:
apply fund_dom_s.quotientMeasureEqMeasurePreimage

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 α
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
vol_s : ν s = 0
⊢ 0 = Measure.map (Quotient.mk α_mod_G) (ν.restrict s)

Proof state:
case h.e'_3
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 α
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
vol_s : ν s = 0
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
⊢ (Measure.map (Quotient.mk α_mod_G) (ν.restrict s)) U = ν (Quotient.mk α_mod_G ⁻¹' U ∩ s)

Tactic:
rw [measure_map_restrict_apply (meas_U := meas_U)]

Result:
no goals

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 α
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
vol_s : ν s = 0
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
⊢ 0 = (Measure.map (Quotient.mk α_mod_G) (ν.restrict s)) U

Tactic:
convert (measure_inter_null_of_null_right (h := vol_s) (Quotient.mk α_mod_G ⁻¹' U)).symm

Result:
case h.e'_3
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 α
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
vol_s : ν s = 0
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
⊢ (Measure.map (Quotient.mk α_mod_G) (ν.restrict s)) U = ν (Quotient.mk α_mod_G ⁻¹' U ∩ 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 α
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
vol_s : ν s = 0
⊢ 0 = Measure.map (Quotient.mk α_mod_G) (ν.restrict s)

Tactic:
ext U meas_U

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 α
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
vol_s : ν s = 0
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
⊢ 0 U = (Measure.map (Quotient.mk α_mod_G) (ν.restrict s)) U

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 α
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
vol_s : ν s = 0
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
⊢ 0 U = (Measure.map (Quotient.mk α_mod_G) (ν.restrict s)) U

Tactic:
simp only [Measure.coe_zero, Pi.zero_apply]

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 α
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
vol_s : ν s = 0
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
⊢ 0 = (Measure.map (Quotient.mk α_mod_G) (ν.restrict s)) U