awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst_2 : QuotientMeasureEqMeasurePreimage ν μ
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
inst_5 : BorelSpace G
inst_6 : PolishSpace G
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
this :
  Eq (α := Set G) (preimage (β := G ⧸ Γ) QuotientGroup.mk ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A))
    ((fun (x : G) ↦ g * x) ⁻¹' π_preA)
rw :
  Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞)
        ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ preimage (β := G) (fun (x : G) ↦ g * x) ((fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕)) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' (π_preA ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕)) : ℝ≥0∞)

Tactic:
rw [preimage_inter]

Premises used: Set.preimage_inter
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst_2 : QuotientMeasureEqMeasurePreimage ν μ
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
inst_5 : BorelSpace G
inst_6 : PolishSpace G
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
this :
  Eq (α := Set G) (preimage (β := G ⧸ Γ) QuotientGroup.mk ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A))
    ((fun (x : G) ↦ g * x) ⁻¹' π_preA)
h : 𝓕 = preimage (β := G) (fun (x : G) ↦ g * x) ((fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞)
        ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ preimage (β := G) (fun (x : G) ↦ g * x) ((fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕)) :
      ℝ≥0∞)

Tactic:
congr 2
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst_2 : QuotientMeasureEqMeasurePreimage ν μ
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
inst_5 : BorelSpace G
inst_6 : PolishSpace G
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
this :
  Eq (α := Set G) (preimage (β := G ⧸ Γ) QuotientGroup.mk ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A))
    ((fun (x : G) ↦ g * x) ⁻¹' π_preA)
⊢ 𝓕 = preimage (β := G) (fun (x : G) ↦ g * x) ((fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕)

Tactic:
simp [Set.preimage]

Premises used: Set.preimage
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst_2 : QuotientMeasureEqMeasurePreimage ν μ
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
inst_5 : BorelSpace G
inst_6 : PolishSpace G
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
this :
  Eq (α := Set G) (preimage (β := G ⧸ Γ) QuotientGroup.mk ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A))
    ((fun (x : G) ↦ g * x) ⁻¹' π_preA)
rw rw₁ :
  Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' (π_preA ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕)) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕) : ℝ≥0∞)

Tactic:
rw [measure_preimage_mul]

Premises used: MeasureTheory.measure_preimage_mul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst_2 : QuotientMeasureEqMeasurePreimage ν μ
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
inst_5 : BorelSpace G
inst_6 : PolishSpace G
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
this :
  Eq (α := Set G) (preimage (β := G ⧸ Γ) QuotientGroup.mk ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A))
    ((fun (x : G) ↦ g * x) ⁻¹' π_preA)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕) : ℝ≥0∞)

Tactic:
have : ν ((g * ·) ⁻¹' π_preA ∩ 𝓕) = ν (π_preA ∩ (g⁻¹ * ·) ⁻¹' 𝓕) := by
      trans ν ((g * ·) ⁻¹' (π_preA ∩ (g⁻¹ * ·) ⁻¹' 𝓕))
      · rw [preimage_inter]
        congr 2
        simp [Set.preimage]
      rw [measure_preimage_mul]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst_2 : QuotientMeasureEqMeasurePreimage ν μ
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
inst_5 : BorelSpace G
inst_6 : PolishSpace G
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
this_1 :
  Eq (α := Set G) (preimage (β := G ⧸ Γ) QuotientGroup.mk ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A))
    ((fun (x : G) ↦ g * x) ⁻¹' π_preA)
this :
  Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕) : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ (fun (x : G) ↦ g⁻¹ • x) ⁻¹' 𝓕) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ g • 𝓕) : ℝ≥0∞)

Tactic:
rw [this, ← preimage_smul_inv]

Premises used: Set.preimage_smul_inv
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst_2 : QuotientMeasureEqMeasurePreimage ν μ
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
inst_5 : BorelSpace G
inst_6 : PolishSpace G
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
this_1 :
  Eq (α := Set G) (preimage (β := G ⧸ Γ) QuotientGroup.mk ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A))
    ((fun (x : G) ↦ g * x) ⁻¹' π_preA)
this :
  Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ (fun (x : G) ↦ g⁻¹ • x) ⁻¹' 𝓕) : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : PolishSpace G
Γ : Subgroup G
inst_6 : Γ.Normal
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
inst_10 : QuotientMeasureEqMeasurePreimage ν μ
x : G ⧸ Γ
h :
  ∀ (A : Set (G ⧸ Γ)) (hA : MeasurableSet A),
    Eq (α := ℝ≥0∞) (((map (fun (x_1 : G ⧸ Γ) ↦ x * x_1) μ : Measure (G ⧸ Γ)) : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)
      ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)
⊢ map (fun (x_1 : G ⧸ Γ) ↦ x * x_1) μ = μ

Tactic:
ext A hA
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : PolishSpace G
Γ : Subgroup G
inst_6 : Γ.Normal
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
inst_10 : QuotientMeasureEqMeasurePreimage ν μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
h :
  ∀ (x₁ : G) (h : ⟦x₁⟧ = x),
    Eq (α := ℝ≥0∞) (((map (fun (x_1 : G ⧸ Γ) ↦ x * x_1) μ : Measure (G ⧸ Γ)) : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)
      ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map (fun (x_1 : G ⧸ Γ) ↦ x * x_1) μ : Measure (G ⧸ Γ)) : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)
    ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)

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

Premises used: Quotient.exists_rep
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : PolishSpace G
Γ : Subgroup G
inst_6 : Γ.Normal
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
inst_10 : QuotientMeasureEqMeasurePreimage ν μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
x₁ : G
h : ⟦x₁⟧ = x
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) ((fun (x : G ⧸ Γ) ↦ x₁ • x) ⁻¹' A) : ℝ≥0∞)
    ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
measure_preimage_smul μ x₁ A

Premises used: MeasureTheory.measure_preimage_smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : PolishSpace G
Γ : Subgroup G
inst_6 : Γ.Normal
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
inst_10 : QuotientMeasureEqMeasurePreimage ν μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
x₁ : G
h : ⟦x₁⟧ = x
h₁ :
  Eq (α := ℝ≥0∞) (((map (fun (x_1 : G ⧸ Γ) ↦ x * x_1) μ : Measure (G ⧸ Γ)) : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)
    ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) ((fun (x : G ⧸ Γ) ↦ x₁ • x) ⁻¹' A) : ℝ≥0∞)
h₂ : SMulInvariantMeasure G (G ⧸ Γ) μ
⊢ Eq (α := ℝ≥0∞) (((map (fun (x_1 : G ⧸ Γ) ↦ x * x_1) μ : Measure (G ⧸ Γ)) : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)
    ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
convert! measure_preimage_smul μ x₁ A using 1
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : PolishSpace G
Γ : Subgroup G
inst_6 : Γ.Normal
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
inst_10 : QuotientMeasureEqMeasurePreimage ν μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
x₁ : G
h : ⟦x₁⟧ = x
h₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) ((fun (x : G ⧸ Γ) ↦ ⟦x₁⟧ * x) ⁻¹' A) : ℝ≥0∞)
    ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) ((fun (x : G ⧸ Γ) ↦ x₁ • x) ⁻¹' A) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map (fun (x_1 : G ⧸ Γ) ↦ x * x_1) μ : Measure (G ⧸ Γ)) : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)
    ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) ((fun (x : G ⧸ Γ) ↦ x₁ • x) ⁻¹' A) : ℝ≥0∞)

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

Premises used: MeasureTheory.Measure.map_apply, MeasurableMul.measurable_const_mul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : PolishSpace G
Γ : Subgroup G
inst_6 : Γ.Normal
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
inst_10 : QuotientMeasureEqMeasurePreimage ν μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
x₁ : G
h : ⟦x₁⟧ = x
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) ((fun (x : G ⧸ Γ) ↦ ⟦x₁⟧ * x) ⁻¹' A) : ℝ≥0∞)
    ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) ((fun (x : G ⧸ Γ) ↦ x₁ • x) ⁻¹' A) : ℝ≥0∞)

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

Premises used: MulAction.Quotient.coe_smul_out, Quotient.mk''_eq_mk
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : PolishSpace G
Γ : Subgroup G
inst_6 : Γ.Normal
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
inst_10 : QuotientMeasureEqMeasurePreimage ν μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
x₁ : G
h : ⟦x₁⟧ = x
⊢ SMulInvariantMeasure G (G ⧸ Γ) μ

Tactic:
smulInvariantMeasure_quotient ν

Premises used: MeasureTheory.QuotientMeasureEqMeasurePreimage.smulInvariantMeasure_quotient
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : PolishSpace G
Γ : Subgroup G
inst_6 : Γ.Normal
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
inst_10 : QuotientMeasureEqMeasurePreimage ν μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
x₁ : G
h : ⟦x₁⟧ = x
⊢ SMulInvariantMeasure G (G ⧸ Γ) μ

Tactic:
exact smulInvariantMeasure_quotient ν

Premises used: MeasureTheory.QuotientMeasureEqMeasurePreimage.smulInvariantMeasure_quotient
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : PolishSpace G
Γ : Subgroup G
inst_6 : Γ.Normal
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
inst_10 : Countable.{u_1 + 1} ↥Γ
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
V : Set (G ⧸ Γ)
meas_V : MeasurableSet V
neZeroV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (0 : ℝ≥0∞)
hV :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
apply : μ = map (Quotient.mk (MulAction.orbitRel (↥Γ.op) G)) (ν.restrict s)
⊢ QuotientMeasureEqMeasurePreimage ν μ

Tactic:
apply fund_dom_s.quotientMeasureEqMeasurePreimage

Premises used: MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : PolishSpace G
Γ : Subgroup G
inst_6 : Γ.Normal
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
inst_10 : Countable.{u_1 + 1} ↥Γ
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
V : Set (G ⧸ Γ)
meas_V : MeasurableSet V
neZeroV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (0 : ℝ≥0∞)
hV :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ (U : Set (G ⧸ Γ)),
    MeasurableSet U →
      Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) U : ℝ≥0∞)
        (((map (Quotient.mk (MulAction.orbitRel (↥Γ.op) G)) (ν.restrict s) :
                Measure (Quotient (MulAction.orbitRel (↥Γ.op) G))) :
              (a : Set (G ⧸ Γ)) → ℝ≥0∞)
            U :
          ℝ≥0∞)
⊢ μ = map (Quotient.mk (MulAction.orbitRel (↥Γ.op) G)) (ν.restrict s)

Tactic:
ext U _
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : PolishSpace G
Γ : Subgroup G
inst_6 : Γ.Normal
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
inst_10 : Countable.{u_1 + 1} ↥Γ
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
V : Set (G ⧸ Γ)
meas_V : MeasurableSet V
neZeroV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (0 : ℝ≥0∞)
hV :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set (G ⧸ Γ)
h : MeasurableSet U
⊢ Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk

Tactic:
have meas_π : Measurable (QuotientGroup.mk : G → G ⧸ Γ) := continuous_quotient_mk'.measurable
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : PolishSpace G
Γ : Subgroup G
inst_6 : Γ.Normal
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
inst_10 : Countable.{u_1 + 1} ↥Γ
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
V : Set (G ⧸ Γ)
meas_V : MeasurableSet V
neZeroV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (0 : ℝ≥0∞)
hV :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set (G ⧸ Γ)
h : MeasurableSet U
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)
⊢ HasFundamentalDomain (↥Γ.op) G ν

Tactic:
haveI has_fund : HasFundamentalDomain Γ.op G ν := ⟨⟨s, fund_dom_s⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : PolishSpace G
Γ : Subgroup G
inst_6 : Γ.Normal
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
inst_10 : Countable.{u_1 + 1} ↥Γ
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
V : Set (G ⧸ Γ)
meas_V : MeasurableSet V
neZeroV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (0 : ℝ≥0∞)
hV :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set (G ⧸ Γ)
h : MeasurableSet U
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)
has_fund : HasFundamentalDomain (↥Γ.op) G ν
⊢ QuotientMeasureEqMeasurePreimage ν μ'

Tactic:
have i : QuotientMeasureEqMeasurePreimage ν μ' :=
    fund_dom_s.quotientMeasureEqMeasurePreimage_quotientMeasure
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : PolishSpace G
Γ : Subgroup G
inst_6 : Γ.Normal
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
inst_10 : Countable.{u_1 + 1} ↥Γ
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
V : Set (G ⧸ Γ)
meas_V : MeasurableSet V
neZeroV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (0 : ℝ≥0∞)
hV :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set (G ⧸ Γ)
h : MeasurableSet U
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)
has_fund : HasFundamentalDomain (↥Γ.op) G ν
i : QuotientMeasureEqMeasurePreimage ν μ'
⊢ μ'.IsMulLeftInvariant

Tactic:
have : μ'.IsMulLeftInvariant :=
    MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient ν