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
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 : μ = μ'
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∞)
⊢ 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]
-- 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 ν μ'
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∞)

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
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 : μ'.IsMulLeftInvariant
h : μ = μ'
⊢ 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:
suffices μ = μ' by
    rw [this]
    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
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
⊢ SigmaFinite μ'

Tactic:
have : SigmaFinite μ' := i.sigmaFiniteQuotient
-- 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_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∞) V : ℝ≥0∞)
        ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) •
      μ
⊢ μ = μ'

Tactic:
rw [measure_eq_div_smul μ' μ neZeroV neTopV, hV]

Premises used: MeasureTheory.measure_eq_div_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
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∞) V : ℝ≥0∞)
        ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) •
      μ =
    μ
⊢ μ =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
        ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) •
      μ

Tactic:
symm
-- 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 ν μ'
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 μ = μ
rw₁ rw₂ : μ = μ
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
        ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) •
      μ =
    μ

Tactic:
rw [this, one_smul]

Premises used: one_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
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∞) 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∞) •
      μ =
    μ

Tactic:
suffices (μ' V / ν (QuotientGroup.mk ⁻¹' V ∩ s)) = 1 by rw [this, one_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
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
h₁ : MeasurableSet (QuotientGroup.mk ⁻¹' V)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
      ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) =
    1

Tactic:
rw [Measure.map_apply meas_π meas_V, Measure.restrict_apply]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.restrict_apply
-- 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 ν μ'
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

Tactic:
ENNReal.div_self ..

Premises used: ENNReal.div_self
-- 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_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∞)
h₁ : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥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

Tactic:
convert! ENNReal.div_self ..

Premises used: ENNReal.div_self
-- 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 ν μ'
this_1 : μ'.IsMulLeftInvariant
this : SigmaFinite μ'
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
trans hV.symm neZeroV

Premises used: Trans.trans, Eq.symm
-- 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 ν μ'
this_1 : μ'.IsMulLeftInvariant
this : SigmaFinite μ'
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact trans hV.symm neZeroV

Premises used: Trans.trans, Eq.symm
-- 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 ν μ'
this_1 : μ'.IsMulLeftInvariant
this : SigmaFinite μ'
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
trans hV.symm neTopV

Premises used: Trans.trans, Eq.symm
-- 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 ν μ'
this_1 : μ'.IsMulLeftInvariant
this : SigmaFinite μ'
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact trans hV.symm neTopV

Premises used: Trans.trans, Eq.symm
-- 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 ν μ'
this_1 : μ'.IsMulLeftInvariant
this : SigmaFinite μ'
⊢ MeasurableSet (QuotientGroup.mk ⁻¹' V)

Tactic:
measurableSet_quotient.mp meas_V

Premises used: Iff.mp, measurableSet_quotient