awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
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∞)
        ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ preimage (β := G) (fun (x : G) ↦ g * x) ((fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕)) :
      ℝ≥0∞)
have h : 𝓕 = preimage (β := G) (fun (x : G) ↦ g * x) ((fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
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 ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕)) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕) : ℝ≥0∞)
have 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∞)
Tactic: rw [measure_preimage_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (hypothesis)
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 ∩ g • 𝓕) : ℝ≥0∞)
have 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∞)
Tactic: have : ν ((g * ·) ⁻¹' π_preA ∩ 𝓕) = ν (π_preA ∩ (g⁻¹ * ·) ⁻¹' 𝓕) := by
      trans ν ((g * ·) ⁻¹' (π_preA ∩ (g⁻¹ * ·) ⁻¹' 𝓕))
      · rw [preimage_inter]
        congr 2
        simp [Set.preimage]
      rw [measure_preimage_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
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∞) ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ g • 𝓕) : ℝ≥0∞)
have 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∞)
Tactic: rw [this, ← preimage_smul_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
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 ⧸ Γ
⊢ map (fun (x_1 : G ⧸ Γ) ↦ x * x_1) μ = μ
have 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∞)
Tactic: ext A hA
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
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
⊢ Eq (α := ℝ≥0∞) (((map (fun (x_1 : G ⧸ Γ) ↦ x * x_1) μ : Measure (G ⧸ Γ)) : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)
    ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)
have 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∞)
Tactic: obtain ⟨x₁, h⟩ := @Quotient.exists_rep _ (QuotientGroup.leftRel Γ) x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
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∞) (((map (fun (x_1 : G ⧸ Γ) ↦ x * x_1) μ : Measure (G ⧸ Γ)) : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)
    ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)
have 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∞)
Tactic: convert! measure_preimage_smul μ x₁ A using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((map (fun (x_1 : G ⧸ Γ) ↦ x * x_1) μ : Measure (G ⧸ Γ)) : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)
    ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)
have h₂ : SMulInvariantMeasure G (G ⧸ Γ) μ
Tactic: convert! measure_preimage_smul μ x₁ A using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
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∞) (((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∞)
have 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∞)
Tactic: rw [← h, Measure.map_apply (measurable_const_mul _) hA]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
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∞)
⊢ QuotientMeasureEqMeasurePreimage ν μ
have apply : μ = map (Quotient.mk (MulAction.orbitRel (↥Γ.op) G)) (ν.restrict s)
Tactic: apply fund_dom_s.quotientMeasureEqMeasurePreimage
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
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∞)
⊢ μ = map (Quotient.mk (MulAction.orbitRel (↥Γ.op) G)) (ν.restrict s)
have 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∞)
Tactic: ext U _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (hypothesis)
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
⊢ 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∞)
have meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
Tactic: have meas_π : Measurable (QuotientGroup.mk : G → G ⧸ Γ) := continuous_quotient_mk'.measurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (hypothesis)
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)
⊢ 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∞)
have has_fund : HasFundamentalDomain (↥Γ.op) G ν
Tactic: haveI has_fund : HasFundamentalDomain Γ.op G ν := ⟨⟨s, fund_dom_s⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (hypothesis)
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 ν
⊢ 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∞)
have i : QuotientMeasureEqMeasurePreimage ν μ'
Tactic: have i : QuotientMeasureEqMeasurePreimage ν μ' :=
    fund_dom_s.quotientMeasureEqMeasurePreimage_quotientMeasure
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (hypothesis)
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 ν μ'
⊢ 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∞)
have this : μ'.IsMulLeftInvariant
Tactic: have : μ'.IsMulLeftInvariant :=
    MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
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 ν μ'
this_1 : μ'.IsMulLeftInvariant
this : μ = μ'
⊢ 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∞)
have rw : 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∞)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
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 ν μ'
this : μ'.IsMulLeftInvariant
⊢ 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∞)
have h : μ = μ'
Tactic: suffices μ = μ' by
    rw [this]
    rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (hypothesis)
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 ν μ'
this : μ'.IsMulLeftInvariant
⊢ μ = μ'
have this₁ : SigmaFinite μ'
Tactic: have : SigmaFinite μ' := i.sigmaFiniteQuotient