-- Mathlib/MeasureTheory/Measure/Haar/Quotient.lean
/-- If `μ` on `G ⧸ Γ` satisfies `QuotientMeasureEqMeasurePreimage` relative to a both left- and
  right-invariant measure on `G` and `Γ` is a normal subgroup, then `μ` is a left-invariant
  measure. -/
@[to_additive "If `μ` on `G ⧸ Γ` satisfies `AddQuotientMeasureEqMeasurePreimage` relative to a both
  left- and right-invariant measure on `G` and `Γ` is a normal subgroup, then `μ` is a
  left-invariant measure."]
lemma MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient
    [hasFun : HasFundamentalDomain Γ.op G ν] [QuotientMeasureEqMeasurePreimage ν μ] :
    μ.IsMulLeftInvariant where
  map_mul_left_eq_self x

Proof state:
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : BorelSpace G
inst✝⁵ : PolishSpace G
Γ : Subgroup G
inst✝⁴ : Γ.Normal
inst✝³ : T2Space (G ⧸ Γ)
inst✝² : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝¹ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
x : G ⧸ Γ
⊢ map (fun x_1 => x * x_1) μ = μ

Tactic:
ext A hA

Result:
case h
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : BorelSpace G
inst✝⁵ : PolishSpace G
Γ : Subgroup G
inst✝⁴ : Γ.Normal
inst✝³ : T2Space (G ⧸ Γ)
inst✝² : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝¹ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
⊢ (map (fun x_1 => x * x_1) μ) A = μ A

Proof state:
case h.intro
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : BorelSpace G
inst✝⁵ : PolishSpace G
Γ : Subgroup G
inst✝⁴ : Γ.Normal
inst✝³ : T2Space (G ⧸ Γ)
inst✝² : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝¹ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
x₁ : G
h : ⟦x₁⟧ = x
⊢ SMulInvariantMeasure G (G ⧸ Γ) μ

Tactic:
exact smulInvariantMeasure_quotient ν

Result:
no goals

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

Tactic:
obtain ⟨x₁, h⟩ := @Quotient.exists_rep _ (QuotientGroup.leftRel Γ) x

Result:
case h.intro
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : BorelSpace G
inst✝⁵ : PolishSpace G
Γ : Subgroup G
inst✝⁴ : Γ.Normal
inst✝³ : T2Space (G ⧸ Γ)
inst✝² : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝¹ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
x₁ : G
h : ⟦x₁⟧ = x
⊢ (map (fun x_1 => x * x_1) μ) A = μ A

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

Tactic:
simp [← MulAction.Quotient.coe_smul_out, ← Quotient.mk''_eq_mk]

Result:
no goals

Proof state:
case h.intro
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : BorelSpace G
inst✝⁵ : PolishSpace G
Γ : Subgroup G
inst✝⁴ : Γ.Normal
inst✝³ : T2Space (G ⧸ Γ)
inst✝² : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝¹ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
x₁ : G
h : ⟦x₁⟧ = x
⊢ (map (fun x_1 => x * x_1) μ) A = μ A

Tactic:
convert measure_preimage_smul μ x₁ A using 1

Result:
case h.e'_2
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : BorelSpace G
inst✝⁵ : PolishSpace G
Γ : Subgroup G
inst✝⁴ : Γ.Normal
inst✝³ : T2Space (G ⧸ Γ)
inst✝² : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝¹ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
x₁ : G
h : ⟦x₁⟧ = x
⊢ (map (fun x_1 => x * x_1) μ) A = μ ((fun x => x₁ • x) ⁻¹' A)

case h.intro
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : BorelSpace G
inst✝⁵ : PolishSpace G
Γ : Subgroup G
inst✝⁴ : Γ.Normal
inst✝³ : T2Space (G ⧸ Γ)
inst✝² : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝¹ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
x₁ : G
h : ⟦x₁⟧ = x
⊢ SMulInvariantMeasure G (G ⧸ Γ) μ

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

Tactic:
rw [← h, Measure.map_apply (measurable_const_mul _) hA]

Result:
case h.e'_2
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : BorelSpace G
inst✝⁵ : PolishSpace G
Γ : Subgroup G
inst✝⁴ : Γ.Normal
inst✝³ : T2Space (G ⧸ Γ)
inst✝² : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝¹ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
x₁ : G
h : ⟦x₁⟧ = x
⊢ μ ((fun x => ⟦x₁⟧ * x) ⁻¹' A) = μ ((fun x => x₁ • x) ⁻¹' A)