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 : SigmaFinite μ'
⊢ MeasurableSet (QuotientGroup.mk ⁻¹' V)

Tactic:
exact measurableSet_quotient.mp meas_V

Premises used: Iff.mp, measurableSet_quotient
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
h : covolume (↥Γ.op) G ν = (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ
obtain : ∀ (s : Set G) (fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν), QuotientMeasureEqMeasurePreimage ν μ
⊢ QuotientMeasureEqMeasurePreimage ν μ

Tactic:
obtain ⟨s, fund_dom_s⟩ := hasFun.ExistsIsFundamentalDomain

Premises used: MeasureTheory.HasFundamentalDomain.ExistsIsFundamentalDomain
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
h : covolume (↥Γ.op) G ν = (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have finiteCovol : μ univ < ⊤ := measure_lt_top μ univ
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
h : covolume (↥Γ.op) G ν = (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
rw [fund_dom_s.covolume_eq_volume] at h

Premises used: MeasureTheory.IsFundamentalDomain.covolume_eq_volume
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
h : covolume (↥Γ.op) G ν = (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
h₁ : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ IsFundamentalDomain (↥Γ.op) s ν

Tactic:
rw [fund_dom_s.covolume_eq_volume] at h

Premises used: MeasureTheory.IsFundamentalDomain.covolume_eq_volume
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
h : covolume (↥Γ.op) G ν = (μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
h₁ : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s₁ : IsFundamentalDomain (↥Γ.op) s ν
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [fund_dom_s.covolume_eq_volume] at h

Premises used: MeasureTheory.IsFundamentalDomain.covolume_eq_volume
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
pos :
  ∀ (meas_s_ne_zero : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    QuotientMeasureEqMeasurePreimage ν μ
neg :
  ∀ (meas_s_ne_zero : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    QuotientMeasureEqMeasurePreimage ν μ
⊢ QuotientMeasureEqMeasurePreimage ν μ

Tactic:
by_cases meas_s_ne_zero : ν s = 0

Premises used: DFunLike.coe
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
meas_s_ne_zero : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ QuotientMeasureEqMeasurePreimage (G := ↥Γ.op) ν 0

Tactic:
fund_dom_s.quotientMeasureEqMeasurePreimage_of_zero meas_s_ne_zero

Premises used: MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_of_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 ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
inst_10 : Countable.{u_1 + 1} ↥Γ
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
meas_s_ne_zero : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h₁ : μ = 0
⊢ QuotientMeasureEqMeasurePreimage ν μ

Tactic:
convert! fund_dom_s.quotientMeasureEqMeasurePreimage_of_zero meas_s_ne_zero

Premises used: MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_of_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 ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
inst_10 : Countable.{u_1 + 1} ↥Γ
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
meas_s_ne_zero : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
h₂ : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h₃ h₄ : Eq (α := ℝ≥0∞) 0 0
⊢ μ = 0

Tactic:
rw [← @measure_univ_eq_zero, ← h, meas_s_ne_zero]

Premises used: MeasureTheory.Measure.measure_univ_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 ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
inst_10 : Countable.{u_1 + 1} ↥Γ
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
meas_s_ne_zero : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
neg : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
neg₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk univ ∩ s) : ℝ≥0∞)
neg₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ QuotientMeasureEqMeasurePreimage ν μ

Tactic:
apply IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set (fund_dom_s := fund_dom_s)
    (meas_V := MeasurableSet.univ)

Premises used: MeasureTheory.Measure.IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set, MeasurableSet.univ
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
meas_s_ne_zero : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
neg : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← h]
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
meas_s_ne_zero : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
meas_s_ne_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 ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
inst_10 : Countable.{u_1 + 1} ↥Γ
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
meas_s_ne_zero : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact meas_s_ne_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 ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
inst_10 : Countable.{u_1 + 1} ↥Γ
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
meas_s_ne_zero : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
neg :
  Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk univ ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk univ ∩ s) : ℝ≥0∞)

Tactic:
rw [← h]
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
meas_s_ne_zero : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk univ ∩ s) : ℝ≥0∞)

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 ⧸ Γ)
ν : Measure G
inst_9 : ν.IsMulLeftInvariant
inst_10 : Countable.{u_1 + 1} ↥Γ
inst_11 : ν.IsMulRightInvariant
inst_12 : SigmaFinite ν
inst_13 : μ.IsMulLeftInvariant
inst_14 : SigmaFinite μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
meas_s_ne_zero : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
neg : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← h]
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
meas_s_ne_zero : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteCovol.ne

Premises used: LT.lt.ne
-- 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 μ
inst_15 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
meas_s_ne_zero : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
convert! finiteCovol.ne

Premises used: LT.lt.ne
-- 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 ν μ
i : HasFundamentalDomain (↥Γ.op) G ν
inst_14 : IsFiniteMeasure μ
obtain : ∀ (K : PositiveCompacts G), μ.IsHaarMeasure
⊢ μ.IsHaarMeasure

Tactic:
obtain ⟨K⟩ := PositiveCompacts.nonempty' (α := G)

Premises used: TopologicalSpace.PositiveCompacts.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 ⧸ Γ)
μ : Measure (G ⧸ Γ)
inst_9 : Countable.{u_1 + 1} ↥Γ
ν : Measure G
inst_10 : ν.IsHaarMeasure
inst_11 : ν.IsMulRightInvariant
inst_12 : LocallyCompactSpace G
inst_13 : QuotientMeasureEqMeasurePreimage ν μ
i : HasFundamentalDomain (↥Γ.op) G ν
inst_14 : IsFiniteMeasure μ
K : PositiveCompacts G
K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K
⊢ μ.IsMulLeftInvariant

Tactic:
haveI : IsMulLeftInvariant μ :=
    MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient ν
-- 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 ν μ
i : HasFundamentalDomain (↥Γ.op) G ν
inst_14 : IsFiniteMeasure μ
K : PositiveCompacts G
K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K
this : μ.IsMulLeftInvariant
rw :
  (HSMul.hSMul (α := ℝ≥0∞) (β := Measure (G ⧸ Γ)) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K' : Set (G ⧸ Γ)) : ℝ≥0∞)
      (haarMeasure K')).IsHaarMeasure
⊢ μ.IsHaarMeasure

Tactic:
rw [haarMeasure_unique μ K']

Premises used: MeasureTheory.Measure.haarMeasure_unique