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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : LocallyCompactSpace G
inst_13 : QuotientMeasureEqMeasurePreimage ν μ
inst_14 : IsFiniteMeasure μ
K : PositiveCompacts G
K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K
this : μ.IsMulLeftInvariant
s : Set G
finiteCovol : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
ctop :
  LE.le (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G)) ∩ s) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G)) ∩ s) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
refine lt_of_le_of_lt ?_ finiteCovol.lt_top

Premises used: lt_of_le_of_lt, Ne.lt_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 ⧸ Γ)
μ : Measure (G ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : LocallyCompactSpace G
inst_13 : QuotientMeasureEqMeasurePreimage ν μ
inst_14 : IsFiniteMeasure μ
K : PositiveCompacts G
K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K
this : μ.IsMulLeftInvariant
s : Set G
finiteCovol : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
ctop : preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G)) ∩ s ⊆ s
⊢ LE.le (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G)) ∩ s) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
apply measure_mono

Premises used: MeasureTheory.measure_mono
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : LocallyCompactSpace G
inst_13 : QuotientMeasureEqMeasurePreimage ν μ
inst_14 : IsFiniteMeasure μ
K : PositiveCompacts G
K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K
this : μ.IsMulLeftInvariant
s : Set G
finiteCovol : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
⊢ preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G)) ∩ s ⊆ s

Tactic:
inter_subset_right

Premises used: Set.inter_subset_right
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : LocallyCompactSpace G
inst_13 : QuotientMeasureEqMeasurePreimage ν μ
inst_14 : IsFiniteMeasure μ
K : PositiveCompacts G
K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K
this : μ.IsMulLeftInvariant
s : Set G
finiteCovol : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
⊢ preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G)) ∩ s ⊆ s

Tactic:
exact inter_subset_right

Premises used: Set.inter_subset_right
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
V : Set (G ⧸ Γ)
hV : (interior V).Nonempty
meas_V : MeasurableSet V
hμK :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
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 ∩ 𝓕) : ℝ≥0∞)
neTopV₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ QuotientMeasureEqMeasurePreimage ν μ

Tactic:
apply IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set (fund_dom_s := h𝓕)
    (meas_V := meas_V)

Premises used: MeasureTheory.Measure.IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
V : Set (G ⧸ Γ)
hV : (interior V).Nonempty
meas_V : MeasurableSet V
hμK :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
neZeroV : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (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 ⧸ Γ)
μ : Measure (G ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
V : Set (G ⧸ Γ)
hV : (interior V).Nonempty
meas_V : MeasurableSet V
hμK :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
c_eq_zero : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)
neZeroV : IsOpen (interior (QuotientGroup.mk ⁻¹' V))
neZeroV₁ : (interior (QuotientGroup.mk ⁻¹' V)).Nonempty
neZeroV₂ : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (interior (QuotientGroup.mk ⁻¹' V)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False

Tactic:
apply IsOpenPosMeasure.open_pos (interior (π ⁻¹' V)) (μ := ν)
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
V : Set (G ⧸ Γ)
hV : (interior V).Nonempty
meas_V : MeasurableSet V
hμK :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
c_eq_zero : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ IsOpen (interior (QuotientGroup.mk ⁻¹' V))

Tactic:
simp
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
V : Set (G ⧸ Γ)
hV : (interior V).Nonempty
meas_V : MeasurableSet V
hμK :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
c_eq_zero : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)
neZeroV : (QuotientGroup.mk ⁻¹' interior V).Nonempty
⊢ (interior (QuotientGroup.mk ⁻¹' V)).Nonempty

Tactic:
apply Set.Nonempty.mono (preimage_interior_subset_interior_preimage continuous_coinduced_rng)

Premises used: preimage_interior_subset_interior_preimage, Set.Nonempty.mono, continuous_coinduced_rng
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
V : Set (G ⧸ Γ)
hV : (interior V).Nonempty
meas_V : MeasurableSet V
hμK :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
c_eq_zero : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)
neZeroV : interior V ⊆ range QuotientGroup.mk
⊢ (QuotientGroup.mk ⁻¹' interior V).Nonempty

Tactic:
apply hV.preimage'

Premises used: Set.Nonempty.preimage'
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
V : Set (G ⧸ Γ)
hV : (interior V).Nonempty
meas_V : MeasurableSet V
hμK :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
c_eq_zero : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ interior V ⊆ range QuotientGroup.mk

Tactic:
simp
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
V : Set (G ⧸ Γ)
hV : (interior V).Nonempty
meas_V : MeasurableSet V
hμK :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
c_eq_zero : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)
neZeroV : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (interior (QuotientGroup.mk ⁻¹' V)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply measure_mono_null (h := interior_subset)

Premises used: interior_subset, MeasureTheory.measure_mono_null
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
V : Set (G ⧸ Γ)
hV : (interior V).Nonempty
meas_V : MeasurableSet V
hμK :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
c_eq_zero : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)
neZeroV :
  Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((⇑(QuotientGroup.mk' Γ) : (a : G) → G ⧸ Γ) ⁻¹' V ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply h𝓕.measure_zero_of_invariant (ht := fun g ↦ QuotientGroup.sound _ _ g)

Premises used: MeasureTheory.IsFundamentalDomain.measure_zero_of_invariant, QuotientGroup.sound
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
V : Set (G ⧸ Γ)
hV : (interior V).Nonempty
meas_V : MeasurableSet V
hμK :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
c_eq_zero : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((⇑(QuotientGroup.mk' Γ) : (a : G) → G ⧸ Γ) ⁻¹' V ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
c_eq_zero
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
V : Set (G ⧸ Γ)
hV : (interior V).Nonempty
meas_V : MeasurableSet V
hμK :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
c_eq_zero : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((⇑(QuotientGroup.mk' Γ) : (a : G) → G ⧸ Γ) ⁻¹' V ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact c_eq_zero
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
V : Set (G ⧸ Γ)
hV : (interior V).Nonempty
meas_V : MeasurableSet V
hμK :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥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 ⧸ Γ)
μ : Measure (G ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
V : Set (G ⧸ Γ)
hV : (interior V).Nonempty
meas_V : MeasurableSet V
hμK :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥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 ⧸ Γ)
μ : Measure (G ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
V : Set (G ⧸ Γ)
hV : (interior V).Nonempty
meas_V : MeasurableSet V
hμK :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
neTopV
-- 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 ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
V : Set (G ⧸ Γ)
hV : (interior V).Nonempty
meas_V : MeasurableSet V
hμK :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞)
neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact neTopV
-- 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∞)
set :
  let c : ℝ≥0∞ := (ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' (↑K : Set (G ⧸ Γ)) ∩ 𝓕);
  QuotientMeasureEqMeasurePreimage ν (HSMul.hSMul (β := Measure (G ⧸ Γ)) c (haarMeasure K))
⊢ QuotientMeasureEqMeasurePreimage ν
    (HSMul.hSMul (α := ℝ≥0∞) (β := Measure (G ⧸ Γ))
      ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' (↑K : Set (G ⧸ Γ)) ∩ 𝓕) : ℝ≥0∞) (haarMeasure K))

Tactic:
set c := ν ((π ⁻¹' (K : Set (G ⧸ Γ))) ∩ 𝓕)
-- 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 ≠ ∞

Tactic:
have c_ne_top : c ≠ ∞ := measure_inter_ne_top_of_right_ne_top h𝓕_finite
-- 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 ≠ ∞
set :
  let μ := HSMul.hSMul (β := Measure (G ⧸ Γ)) c (haarMeasure K);
  QuotientMeasureEqMeasurePreimage ν μ
⊢ QuotientMeasureEqMeasurePreimage ν (HSMul.hSMul (β := Measure (G ⧸ Γ)) c (haarMeasure K))

Tactic:
set μ := c • haarMeasure K

Premises used: MeasureTheory.Measure.haarMeasure