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 ⧸ Γ)
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 ν
⊢ Ne (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have ctop : Ne (α := ℝ≥0∞)
  ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G)) ∩ s) : ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: change ν (π ⁻¹' (π '' K) ∩ s) ≠ ⊤
-- 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 ⧸ Γ)
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 ν
⊢ Ne (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G)) ∩ s) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have ctop : LT.lt (α := ℝ≥0∞)
  ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G)) ∩ s) : ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: apply ne_of_lt
-- 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 ⧸ Γ)
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 ν
⊢ LT.lt (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G)) ∩ s) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have 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∞)
Tactic: refine lt_of_le_of_lt ?_ finiteCovol.lt_top
-- 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 ⧸ Γ)
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 ν
⊢ LE.le (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G)) ∩ s) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have ctop : preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G)) ∩ s ⊆ s
Tactic: apply measure_mono
-- 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 ⧸ Γ)
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∞)
⊢ QuotientMeasureEqMeasurePreimage ν μ
have neZeroV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) V : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set (fund_dom_s := h𝓕)
    (meas_V := meas_V)
-- 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 ⧸ Γ)
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 : ℝ≥0∞)
have neZeroV : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [hμK]
-- 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 ⧸ Γ)
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∞)
⊢ False
have neZeroV : IsOpen (interior (QuotientGroup.mk ⁻¹' V))
Tactic: apply IsOpenPosMeasure.open_pos (interior (π ⁻¹' V)) (μ := ν)
-- 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 ⧸ Γ)
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))
⊢ False
have neZeroV₁ : (interior (QuotientGroup.mk ⁻¹' V)).Nonempty
Tactic: apply IsOpenPosMeasure.open_pos (interior (π ⁻¹' V)) (μ := ν)
-- 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 ⧸ Γ)
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
⊢ False
have neZeroV₂ : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (interior (QuotientGroup.mk ⁻¹' V)) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply IsOpenPosMeasure.open_pos (interior (π ⁻¹' V)) (μ := ν)
-- 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 ⧸ Γ)
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 (QuotientGroup.mk ⁻¹' V)).Nonempty
have neZeroV : (QuotientGroup.mk ⁻¹' interior V).Nonempty
Tactic: apply Set.Nonempty.mono (preimage_interior_subset_interior_preimage continuous_coinduced_rng)
-- 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 ⧸ Γ)
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∞)
⊢ (QuotientGroup.mk ⁻¹' interior V).Nonempty
have neZeroV : interior V ⊆ range QuotientGroup.mk
Tactic: apply hV.preimage'
-- 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 ⧸ Γ)
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∞) (interior (QuotientGroup.mk ⁻¹' V)) : ℝ≥0∞) (0 : ℝ≥0∞)
have neZeroV : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' V) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply measure_mono_null (h := interior_subset)
-- 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 ⧸ Γ)
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 ⁻¹' V) : ℝ≥0∞) (0 : ℝ≥0∞)
have neZeroV : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((⇑(QuotientGroup.mk' Γ) : (a : G) → G ⧸ Γ) ⁻¹' V ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply h𝓕.measure_zero_of_invariant (ht := fun g ↦ QuotientGroup.sound _ _ g)
-- 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 ⧸ Γ)
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 ⧸ Γ)) ∩ 𝓕)
⊢ QuotientMeasureEqMeasurePreimage ν (HSMul.hSMul (β := Measure (G ⧸ Γ)) c (haarMeasure K))
have c_ne_top : c ≠ ∞
Tactic: have c_ne_top : c ≠ ∞ := measure_inter_ne_top_of_right_ne_top h𝓕_finite
-- 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 ⧸ Γ)
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)
⊢ QuotientMeasureEqMeasurePreimage ν μ
have hμK : (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = c
Tactic: have hμK : μ K = c := by simp [μ, haarMeasure_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 ⧸ Γ)
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 μ
have 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 μ
Tactic: clear_value c
Cleared hypotheses: c, c_ne_top, μ, hμK
-- 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 ⧸ Γ)
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
⊢ SigmaFinite μ
have lift : ∀ (c : ℝ≥0),
  let μ := HSMul.hSMul (β := Measure (G ⧸ Γ)) (↑c : ℝ≥0∞) (haarMeasure K);
  ∀ (hμK : (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) = (↑c : ℝ≥0∞)), SigmaFinite μ
Tactic: lift c to NNReal using c_ne_top
Cleared hypotheses: c, c_ne_top, μ, hμK
-- 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 ⧸ Γ)
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
⊢ QuotientMeasureEqMeasurePreimage ν μ
have this : SigmaFinite μ
Tactic: haveI : SigmaFinite μ := by
    clear_value c
    lift c to NNReal using c_ne_top
    exact SMul.sigmaFinite c
-- 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 ⧸ Γ)
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 μ
⊢ QuotientMeasureEqMeasurePreimage ν μ
have hV : (interior (↑K : Set (G ⧸ Γ))).Nonempty
Tactic: apply IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_HaarMeasure (h𝓕 := h𝓕)
    (meas_V := K.isCompact.measurableSet) (μ := μ)
-- 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 ⧸ Γ)
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∞)
⊢ QuotientMeasureEqMeasurePreimage ν μ
have neTopV : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K : Set (G ⧸ Γ)) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_HaarMeasure (h𝓕 := h𝓕)
    (meas_V := K.isCompact.measurableSet) (μ := μ)
-- 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
μ : 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 𝓕))
⊢ @essSup _ _ _ inst_6 g (map QuotientGroup.mk (μ.restrict 𝓕)) = essSup (fun (x : G) ↦ g (↑x : G ⧸ Γ)) μ
have hπ : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
Tactic: have hπ : Measurable (QuotientGroup.mk : G → G ⧸ Γ) := continuous_quotient_mk'.measurable