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
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 : SigmaFinite μ'
⊢ μ = μ'
have h : μ =
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
      ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) •
    μ
Tactic: rw [measure_eq_div_smul μ' μ neZeroV neTopV, hV]
-- 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 : SigmaFinite μ'
⊢ μ =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
        ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) •
      μ
have h : HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
      ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) •
    μ =
  μ
Tactic: symm
-- 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_2 : SigmaFinite μ'
this :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
      ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) =
    1
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
        ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) •
      μ =
    μ
have rw : HSMul.hSMul (α := ℝ≥0∞) 1 μ = μ
Tactic: rw [this, one_smul]
-- 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_2 : SigmaFinite μ'
this :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
      ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) =
    1
rw : HSMul.hSMul (α := ℝ≥0∞) 1 μ = μ
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
        ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) •
      μ =
    μ
have rw₁ : μ = μ
Tactic: rw [this, one_smul]
-- 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 : SigmaFinite μ'
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
        ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) •
      μ =
    μ
have h : HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) =
  1
Tactic: suffices (μ' V / ν (QuotientGroup.mk ⁻¹' V ∩ s)) = 1 by rw [this, one_smul]
-- 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 : SigmaFinite μ'
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
      ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) =
    1
have h : HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) =
  1
Tactic: rw [Measure.map_apply meas_π meas_V, Measure.restrict_apply]
-- 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_1 : 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 : SigmaFinite μ'
h :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞)
      ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) =
    1
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
      ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) =
    1
have h₁ : MeasurableSet (QuotientGroup.mk ⁻¹' V)
Tactic: rw [Measure.map_apply meas_π meas_V, Measure.restrict_apply]
-- 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 : SigmaFinite μ'
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞)
      ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) =
    1
have h : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: convert! ENNReal.div_self ..
-- 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_1 : 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 : SigmaFinite μ'
h : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞)
      ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) =
    1
have h₁ : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: convert! ENNReal.div_self ..
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
h : covolume (↥Γ.op) G ν = (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ
⊢ QuotientMeasureEqMeasurePreimage ν μ
have obtain : ∀ (s : Set G) (fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν), QuotientMeasureEqMeasurePreimage ν μ
Tactic: obtain ⟨s, fund_dom_s⟩ := hasFun.ExistsIsFundamentalDomain
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
h : covolume (↥Γ.op) G ν = (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
⊢ QuotientMeasureEqMeasurePreimage ν μ
have finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have finiteCovol : μ univ < ⊤ := measure_lt_top μ univ
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
h : covolume (↥Γ.op) G ν = (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ QuotientMeasureEqMeasurePreimage ν μ
have h₁ : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [fund_dom_s.covolume_eq_volume] at h
Cleared hypotheses: h, fund_dom_s, finiteCovol
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ QuotientMeasureEqMeasurePreimage ν μ
have pos : ∀ (meas_s_ne_zero : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), QuotientMeasureEqMeasurePreimage ν μ
Tactic: by_cases meas_s_ne_zero : ν s = 0
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
pos :
  ∀ (meas_s_ne_zero : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    QuotientMeasureEqMeasurePreimage ν μ
⊢ QuotientMeasureEqMeasurePreimage ν μ
have neg : ∀ (meas_s_ne_zero : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  QuotientMeasureEqMeasurePreimage ν μ
Tactic: by_cases meas_s_ne_zero : ν s = 0
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
meas_s_ne_zero : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ QuotientMeasureEqMeasurePreimage ν μ
have h₁ : μ = 0
Tactic: convert! fund_dom_s.quotientMeasureEqMeasurePreimage_of_zero meas_s_ne_zero
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
meas_s_ne_zero : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ = 0
have h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← @measure_univ_eq_zero, ← h, meas_s_ne_zero]
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
meas_s_ne_zero : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
h₂ : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ = 0
have h₃ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [← @measure_univ_eq_zero, ← h, meas_s_ne_zero]
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
meas_s_ne_zero : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ QuotientMeasureEqMeasurePreimage ν μ
have neg : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set (fund_dom_s := fund_dom_s)
    (meas_V := MeasurableSet.univ)