-- Mathlib/MeasureTheory/Measure/Haar/Quotient.lean
/-- Given a quotient space `G ⧸ Γ` where `Γ` is `Countable`, and the restriction,
  `μ_𝓕`, of a right-invariant measure `μ` on `G` to a fundamental domain `𝓕`, a set
  in the quotient which has `μ_𝓕`-measure zero, also has measure zero under the
  folding of `μ` under the quotient. Note that, if `Γ` is infinite, then the folded map
  will take the value `∞` on any open set in the quotient! -/
@[to_additive "Given an additive quotient space `G ⧸ Γ` where `Γ` is `Countable`, and the
  restriction, `μ_𝓕`, of a right-invariant measure `μ` on `G` to a fundamental domain `𝓕`, a set
  in the quotient which has `μ_𝓕`-measure zero, also has measure zero under the
  folding of `μ` under the quotient. Note that, if `Γ` is infinite, then the folded map
  will take the value `∞` on any open set in the quotient!"]
lemma _root_.MeasureTheory.IsFundamentalDomain.absolutelyContinuous_map
    [μ.IsMulRightInvariant] :
    map (QuotientGroup.mk : G → G ⧸ Γ) μ ≪ map (QuotientGroup.mk : G → G ⧸ Γ) (μ.restrict 𝓕)

Proof state:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
⊢ map QuotientGroup.mk μ ≪ map QuotientGroup.mk (μ.restrict 𝓕)

Tactic:
set π : G → G ⧸ Γ := QuotientGroup.mk

Result:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
⊢ map π μ ≪ map π (μ.restrict 𝓕)

Proof state:
case h
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
s_meas : MeasurableSet s
hs : (μ.restrict 𝓕) (π ⁻¹' s) = 0
⊢ MeasurableSet (π ⁻¹' s)

Tactic:
exact MeasurableSet.preimage s_meas meas_π

Result:
no goals

Proof state:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
⊢ map π μ ≪ map π (μ.restrict 𝓕)

Tactic:
have meas_π : Measurable π := continuous_quotient_mk'.measurable

Result:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
⊢ map π μ ≪ map π (μ.restrict 𝓕)

Proof state:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
s_meas : MeasurableSet s
hs : μ (π ⁻¹' s ∩ 𝓕) = 0
γ : ↥Γ.op
⊢ γ • π ⁻¹' s = π ⁻¹' s

Tactic:
ext g

Result:
case h
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
s_meas : MeasurableSet s
hs : μ (π ⁻¹' s ∩ 𝓕) = 0
γ : ↥Γ.op
g : G
⊢ g ∈ γ • π ⁻¹' s ↔ g ∈ π ⁻¹' s

Proof state:
case h
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
s_meas : MeasurableSet s
hs : μ (π ⁻¹' s ∩ 𝓕) = 0
⊢ μ (π ⁻¹' s) = 0

Tactic:
apply h𝓕.measure_zero_of_invariant _ _ hs

Result:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
s_meas : MeasurableSet s
hs : μ (π ⁻¹' s ∩ 𝓕) = 0
⊢ ∀ (g : ↥Γ.op), g • π ⁻¹' s = π ⁻¹' s

Proof state:
case h
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
s_meas : MeasurableSet s
hs : μ (π ⁻¹' s ∩ 𝓕) = 0
γ : ↥Γ.op
g : G
⊢ π (γ⁻¹ • g) ∈ s ↔ π g ∈ s

Tactic:
congr! 1

Result:
case h.a.h.e'_5
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
s_meas : MeasurableSet s
hs : μ (π ⁻¹' s ∩ 𝓕) = 0
γ : ↥Γ.op
g : G
⊢ π (γ⁻¹ • g) = π g

Proof state:
case h.a.h.e'_5
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
s_meas : MeasurableSet s
hs : μ (π ⁻¹' s ∩ 𝓕) = 0
γ : ↥Γ.op
g : G
⊢ π (γ⁻¹ • g) = π g

Tactic:
convert QuotientGroup.mk_mul_of_mem g (γ⁻¹).2 using 1

Result:
no goals