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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0∞ := (ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' (↑K : Set (G ⧸ Γ)) ∩ 𝓕)
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := HSMul.hSMul (β := Measure (G ⧸ Γ)) c (haarMeasure K)
⊢ (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = c

Tactic:
simp [μ, haarMeasure_self]

Premises used: MeasureTheory.Measure.haarMeasure_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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0∞ := (ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' (↑K : Set (G ⧸ Γ)) ∩ 𝓕)
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := HSMul.hSMul (β := Measure (G ⧸ Γ)) c (haarMeasure K)
⊢ (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = c

Tactic:
have hμK : μ K = c := by simp [μ, haarMeasure_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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0∞ := (ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' (↑K : Set (G ⧸ Γ)) ∩ 𝓕)
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := HSMul.hSMul (β := Measure (G ⧸ Γ)) c (haarMeasure K)
hμK : (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = c
clear_value :
  ∀ (c : ℝ≥0∞) (c_ne_top : c ≠ ∞),
    let μ := HSMul.hSMul (β := Measure (G ⧸ Γ)) c (haarMeasure K);
    ∀ (hμK : (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = c), SigmaFinite μ
⊢ SigmaFinite μ

Tactic:
clear_value c
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0∞
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := HSMul.hSMul (β := Measure (G ⧸ Γ)) c (haarMeasure K)
hμK : (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = c
⊢ c ≠ ∞

Tactic:
c_ne_top
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0∞
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := HSMul.hSMul (β := Measure (G ⧸ Γ)) c (haarMeasure K)
hμK : (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = c
lift :
  ∀ (c : ℝ≥0),
    let μ := HSMul.hSMul (β := Measure (G ⧸ Γ)) (↑c : ℝ≥0∞) (haarMeasure K);
    ∀ (hμK : (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = (↑c : ℝ≥0∞)), SigmaFinite μ
⊢ SigmaFinite μ

Tactic:
lift c to NNReal using c_ne_top

Premises used: NNReal
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0
μ : Measure (G ⧸ Γ) := HSMul.hSMul (β := Measure (G ⧸ Γ)) (↑c : ℝ≥0∞) (haarMeasure K)
hμK : (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = (↑c : ℝ≥0∞)
⊢ SigmaFinite μ

Tactic:
SMul.sigmaFinite c

Premises used: MeasureTheory.SMul.sigmaFinite
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0
μ : Measure (G ⧸ Γ) := HSMul.hSMul (β := Measure (G ⧸ Γ)) (↑c : ℝ≥0∞) (haarMeasure K)
hμK : (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = (↑c : ℝ≥0∞)
⊢ SigmaFinite μ

Tactic:
exact SMul.sigmaFinite c

Premises used: MeasureTheory.SMul.sigmaFinite
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0∞ := (ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' (↑K : Set (G ⧸ Γ)) ∩ 𝓕)
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := HSMul.hSMul (β := Measure (G ⧸ Γ)) c (haarMeasure K)
hμK : (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = c
⊢ SigmaFinite μ

Tactic:
haveI : SigmaFinite μ := by
    clear_value c
    lift c to NNReal using c_ne_top
    exact SMul.sigmaFinite c
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0∞ := (ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' (↑K : Set (G ⧸ Γ)) ∩ 𝓕)
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := HSMul.hSMul (β := Measure (G ⧸ Γ)) c (haarMeasure K)
hμK : (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = c
this : SigmaFinite μ
hV : (interior (↑K : Set (G ⧸ Γ))).Nonempty
hμK₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' (↑K : Set (G ⧸ Γ)) ∩ 𝓕) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ QuotientMeasureEqMeasurePreimage ν μ

Tactic:
apply IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_HaarMeasure (h𝓕 := h𝓕)
    (meas_V := K.isCompact.measurableSet) (μ := μ)

Premises used: IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_HaarMeasure, TopologicalSpace.PositiveCompacts.isCompact, IsCompact.measurableSet
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0∞ := (ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' (↑K : Set (G ⧸ Γ)) ∩ 𝓕)
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := HSMul.hSMul (β := Measure (G ⧸ Γ)) c (haarMeasure K)
hμK : (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = c
this : SigmaFinite μ
⊢ (interior (↑K : Set (G ⧸ Γ))).Nonempty

Tactic:
K.interior_nonempty

Premises used: TopologicalSpace.PositiveCompacts.interior_nonempty
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0∞ := (ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' (↑K : Set (G ⧸ Γ)) ∩ 𝓕)
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := HSMul.hSMul (β := Measure (G ⧸ Γ)) c (haarMeasure K)
hμK : (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = c
this : SigmaFinite μ
⊢ (interior (↑K : Set (G ⧸ Γ))).Nonempty

Tactic:
exact K.interior_nonempty

Premises used: TopologicalSpace.PositiveCompacts.interior_nonempty
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0∞ := (ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' (↑K : Set (G ⧸ Γ)) ∩ 𝓕)
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := HSMul.hSMul (β := Measure (G ⧸ Γ)) c (haarMeasure K)
hμK : (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = c
this : SigmaFinite μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' (↑K : Set (G ⧸ Γ)) ∩ 𝓕) : ℝ≥0∞)

Tactic:
hμK
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0∞ := (ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' (↑K : Set (G ⧸ Γ)) ∩ 𝓕)
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := HSMul.hSMul (β := Measure (G ⧸ Γ)) c (haarMeasure K)
hμK : (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = c
this : SigmaFinite μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' (↑K : Set (G ⧸ Γ)) ∩ 𝓕) : ℝ≥0∞)

Tactic:
exact hμK
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0∞ := (ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' (↑K : Set (G ⧸ Γ)) ∩ 𝓕)
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := HSMul.hSMul (β := Measure (G ⧸ Γ)) c (haarMeasure K)
hμK : (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = c
this : SigmaFinite μ
neTopV : c ≠ ∞
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [hμK]
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0∞ := (ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' (↑K : Set (G ⧸ Γ)) ∩ 𝓕)
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := HSMul.hSMul (β := Measure (G ⧸ Γ)) c (haarMeasure K)
hμK : (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = c
this : SigmaFinite μ
⊢ c ≠ ∞

Tactic:
c_ne_top
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0∞ := (ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' (↑K : Set (G ⧸ Γ)) ∩ 𝓕)
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := HSMul.hSMul (β := Measure (G ⧸ Γ)) c (haarMeasure K)
hμK : (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = c
this : SigmaFinite μ
⊢ c ≠ ∞

Tactic:
exact c_ne_top
-- 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
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable (_m := inst_6) g (map QuotientGroup.mk (μ.restrict 𝓕))
⊢ Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk

Tactic:
have hπ : 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
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable (_m := inst_6) g (map QuotientGroup.mk (μ.restrict 𝓕))
hπ : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
rw : essSup (g ∘ QuotientGroup.mk) (μ.restrict 𝓕) = essSup (fun (x : G) ↦ g (↑x : G ⧸ Γ)) μ
⊢ @essSup _ _ _ inst_6 g (map QuotientGroup.mk (μ.restrict 𝓕)) = essSup (fun (x : G) ↦ g (↑x : G ⧸ Γ)) μ

Tactic:
rw [essSup_map_measure g_ae_measurable hπ.aemeasurable]

Premises used: Measurable.aemeasurable, essSup_map_measure
-- 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
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable (_m := inst_6) g (map QuotientGroup.mk (μ.restrict 𝓕))
hπ : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
⊢ essSup (g ∘ QuotientGroup.mk) (μ.restrict 𝓕) = essSup (fun (x : G) ↦ g (↑x : G ⧸ Γ)) μ

Tactic:
h𝓕.essSup_measure_restrict ?_

Premises used: MeasureTheory.IsFundamentalDomain.essSup_measure_restrict
-- 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
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable (_m := inst_6) g (map QuotientGroup.mk (μ.restrict 𝓕))
hπ : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
refine : ∀ (γ : ↥Γ.op) (x : G), (g ∘ QuotientGroup.mk) (γ • x) = (g ∘ QuotientGroup.mk) x
⊢ essSup (g ∘ QuotientGroup.mk) (μ.restrict 𝓕) = essSup (fun (x : G) ↦ g (↑x : G ⧸ Γ)) μ

Tactic:
refine h𝓕.essSup_measure_restrict ?_

Premises used: MeasureTheory.IsFundamentalDomain.essSup_measure_restrict
-- 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
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable (_m := inst_6) g (map QuotientGroup.mk (μ.restrict 𝓕))
hπ : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
γ : Gᵐᵒᵖ
hγ : γ ∈ Γ.op
x : G
dsimp : g (↑(x * MulOpposite.unop γ) : G ⧸ Γ) = g (↑x : G ⧸ Γ)
⊢ (g ∘ QuotientGroup.mk) (Subtype.mk (p := fun (x : Gᵐᵒᵖ) ↦ x ∈ Γ.op) γ hγ • x) = (g ∘ QuotientGroup.mk) x

Tactic:
dsimp
-- 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
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable (_m := inst_6) g (map QuotientGroup.mk (μ.restrict 𝓕))
hπ : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
γ : Gᵐᵒᵖ
hγ : γ ∈ Γ.op
x : G
e_a : Eq (α := G ⧸ Γ) (↑(x * MulOpposite.unop γ) : G ⧸ Γ) (↑x : G ⧸ Γ)
⊢ g (↑(x * MulOpposite.unop γ) : G ⧸ Γ) = g (↑x : G ⧸ Γ)

Tactic:
congr 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
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable (_m := inst_6) g (map QuotientGroup.mk (μ.restrict 𝓕))
hπ : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
γ : Gᵐᵒᵖ
hγ : γ ∈ Γ.op
x : G
⊢ Eq (α := G ⧸ Γ) (↑(x * MulOpposite.unop γ) : G ⧸ Γ) (↑x : G ⧸ Γ)

Tactic:
QuotientGroup.mk_mul_of_mem x hγ

Premises used: QuotientGroup.mk_mul_of_mem
-- 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
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable (_m := inst_6) g (map QuotientGroup.mk (μ.restrict 𝓕))
hπ : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
γ : Gᵐᵒᵖ
hγ : γ ∈ Γ.op
x : G
⊢ Eq (α := G ⧸ Γ) (↑(x * MulOpposite.unop γ) : G ⧸ Γ) (↑x : G ⧸ Γ)

Tactic:
exact QuotientGroup.mk_mul_of_mem x hγ

Premises used: QuotientGroup.mk_mul_of_mem
-- 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
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
set :
  let π : G → G ⧸ Γ := QuotientGroup.mk;
  AbsolutelyContinuous (_m0 := inst_6) (map π μ) (map π (μ.restrict 𝓕))
⊢ AbsolutelyContinuous (α := G ⧸ Γ) (_m0 := inst_6) (map QuotientGroup.mk μ) (map QuotientGroup.mk (μ.restrict 𝓕))

Tactic:
set π : G → G ⧸ Γ := QuotientGroup.mk

Premises used: QuotientGroup.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
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
⊢ Measurable π

Tactic:
have meas_π : Measurable π := 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
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
h :
  ∀ ⦃s : Set (G ⧸ Γ)⦄,
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((map π (μ.restrict 𝓕) : Measure (G ⧸ Γ)) : (a : Set (G ⧸ Γ)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
        Eq (α := ℝ≥0∞) (((map π μ : Measure (G ⧸ Γ)) : (a : Set (G ⧸ Γ)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ AbsolutelyContinuous (_m0 := inst_6) (map π μ) (map π (μ.restrict 𝓕))

Tactic:
apply AbsolutelyContinuous.mk

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk