-- Mathlib/MeasureTheory/Measure/Haar/Quotient.lean
/-- If `μ` satisfies `QuotientMeasureEqMeasurePreimage` relative to a both left- and right-
  invariant measure `ν` on `G`, then it is a `G` invariant measure on `G ⧸ Γ`. -/
@[to_additive]
lemma MeasureTheory.QuotientMeasureEqMeasurePreimage.smulInvariantMeasure_quotient
    [IsMulLeftInvariant ν] [hasFun : HasFundamentalDomain Γ.op G ν] :
    SMulInvariantMeasure G (G ⧸ Γ) μ where
  measure_preimage_smul g A hA

Proof state:
case intro
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst✝⁷ : QuotientMeasureEqMeasurePreimage ν μ
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : PolishSpace G
inst✝² : T2Space (G ⧸ Γ)
inst✝¹ : SecondCountableTopology (G ⧸ Γ)
inst✝ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
⊢ ν (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' ((fun x => g • x) ⁻¹' A) ∩ 𝓕) =
    ν (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' A ∩ g • 𝓕)

Tactic:
change ν ((π ⁻¹' _) ∩ _) = ν ((π ⁻¹' _) ∩ _)

Result:
case intro
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst✝⁷ : QuotientMeasureEqMeasurePreimage ν μ
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : PolishSpace G
inst✝² : T2Space (G ⧸ Γ)
inst✝¹ : SecondCountableTopology (G ⧸ Γ)
inst✝ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
⊢ ν (QuotientGroup.mk ⁻¹' ((fun x => g • x) ⁻¹' A) ∩ 𝓕) = ν (QuotientGroup.mk ⁻¹' A ∩ g • 𝓕)

Proof state:
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst✝⁷ : QuotientMeasureEqMeasurePreimage ν μ
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : PolishSpace G
inst✝² : T2Space (G ⧸ Γ)
inst✝¹ : SecondCountableTopology (G ⧸ Γ)
inst✝ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
⊢ μ ((fun x => g • x) ⁻¹' A) = μ A

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

Result:
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst✝⁷ : QuotientMeasureEqMeasurePreimage ν μ
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : PolishSpace G
inst✝² : T2Space (G ⧸ Γ)
inst✝¹ : SecondCountableTopology (G ⧸ Γ)
inst✝ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable QuotientGroup.mk
⊢ μ ((fun x => g • x) ⁻¹' A) = μ A

Proof state:
case h.e_6.h.e_a
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst✝⁷ : QuotientMeasureEqMeasurePreimage ν μ
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : PolishSpace G
inst✝² : T2Space (G ⧸ Γ)
inst✝¹ : SecondCountableTopology (G ⧸ Γ)
inst✝ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
this : QuotientGroup.mk ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
⊢ 𝓕 = (fun x => g * x) ⁻¹' ((fun x => g⁻¹ * x) ⁻¹' 𝓕)

Tactic:
simp [Set.preimage]

Result:
no goals

Proof state:
case intro
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst✝⁷ : QuotientMeasureEqMeasurePreimage ν μ
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : PolishSpace G
inst✝² : T2Space (G ⧸ Γ)
inst✝¹ : SecondCountableTopology (G ⧸ Γ)
inst✝ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
⊢ μ ((fun x => g • x) ⁻¹' A) = μ A

Tactic:
erw [h𝓕.projection_respects_measure_apply (μ := μ)
  (meas_π (measurableSet_preimage (measurable_const_smul g) hA)),
  h𝓕_translate_fundom.projection_respects_measure_apply (μ := μ) hA]

Result:
case intro
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst✝⁷ : QuotientMeasureEqMeasurePreimage ν μ
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : PolishSpace G
inst✝² : T2Space (G ⧸ Γ)
inst✝¹ : SecondCountableTopology (G ⧸ Γ)
inst✝ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
⊢ ν (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' ((fun x => g • x) ⁻¹' A) ∩ 𝓕) =
    ν (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' A ∩ g • 𝓕)

Proof state:
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst✝⁷ : QuotientMeasureEqMeasurePreimage ν μ
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : PolishSpace G
inst✝² : T2Space (G ⧸ Γ)
inst✝¹ : SecondCountableTopology (G ⧸ Γ)
inst✝ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
this : QuotientGroup.mk ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
⊢ ν ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) =
    ν ((fun x => g * x) ⁻¹' π_preA ∩ (fun x => g * x) ⁻¹' ((fun x => g⁻¹ * x) ⁻¹' 𝓕))

Tactic:
congr 2

Result:
case h.e_6.h.e_a
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst✝⁷ : QuotientMeasureEqMeasurePreimage ν μ
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : PolishSpace G
inst✝² : T2Space (G ⧸ Γ)
inst✝¹ : SecondCountableTopology (G ⧸ Γ)
inst✝ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
this : QuotientGroup.mk ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
⊢ 𝓕 = (fun x => g * x) ⁻¹' ((fun x => g⁻¹ * x) ⁻¹' 𝓕)