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 ν μ
i : HasFundamentalDomain (↥Γ.op) G ν
inst_14 : IsFiniteMeasure μ
K : PositiveCompacts G
K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K
this : μ.IsMulLeftInvariant
⊢ covolume (↥Γ.op) G ν ≠ ∞

Tactic:
have finiteCovol : covolume Γ.op G ν ≠ ⊤ :=
    ne_top_of_lt <| QuotientMeasureEqMeasurePreimage.covolume_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 ⧸ Γ)
μ : 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
finiteCovol : covolume (↥Γ.op) G ν ≠ ∞
obtain :
  ∀ (s : Set G) (fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν),
    (HSMul.hSMul (α := ℝ≥0∞) (β := Measure (G ⧸ Γ)) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K' : Set (G ⧸ Γ)) : ℝ≥0∞)
        (haarMeasure K')).IsHaarMeasure
⊢ (HSMul.hSMul (α := ℝ≥0∞) (β := Measure (G ⧸ Γ)) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K' : Set (G ⧸ Γ)) : ℝ≥0∞)
      (haarMeasure K')).IsHaarMeasure

Tactic:
obtain ⟨s, fund_dom_s⟩ := i
-- 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
finiteCovol : covolume (↥Γ.op) G ν ≠ ∞
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [fund_dom_s.covolume_eq_volume] at finiteCovol

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 ⧸ Γ)
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
finiteCovol : covolume (↥Γ.op) G ν ≠ ∞
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol₁ : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsFundamentalDomain (↥Γ.op) s ν

Tactic:
rw [fund_dom_s.covolume_eq_volume] at finiteCovol

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 ⧸ Γ)
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 ν
rw :
  (HSMul.hSMul (α := ℝ≥0∞) (β := Measure (G ⧸ Γ))
      ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
      (haarMeasure K')).IsHaarMeasure
⊢ (HSMul.hSMul (α := ℝ≥0∞) (β := Measure (G ⧸ Γ)) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K' : Set (G ⧸ Γ)) : ℝ≥0∞)
      (haarMeasure K')).IsHaarMeasure

Tactic:
rw [fund_dom_s.projection_respects_measure_apply μ K'.isCompact.measurableSet]

Premises used: TopologicalSpace.PositiveCompacts.isCompact, IsCompact.measurableSet, MeasureTheory.IsFundamentalDomain.projection_respects_measure_apply
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : PolishSpace G
Γ : Subgroup G
inst_6 : Γ.Normal
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
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 ν
cpos :
  Ne (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
ctop :
  Ne (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ (HSMul.hSMul (α := ℝ≥0∞) (β := Measure (G ⧸ Γ))
      ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
      (haarMeasure K')).IsHaarMeasure

Tactic:
apply IsHaarMeasure.smul

Premises used: MeasureTheory.Measure.IsHaarMeasure.smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : PolishSpace G
Γ : Subgroup G
inst_6 : Γ.Normal
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
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 ν
h :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ ν.IsOpenPosMeasure

Tactic:
have i' : IsOpenPosMeasure (ν : Measure G) := inferInstance
-- 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 ν
h :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
i' : ν.IsOpenPosMeasure
cpos : IsOpen (interior (↑K : Set G))
cpos₁ : (interior (↑K : Set G)).Nonempty
cpos₂ : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (interior (↑K : Set G)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False

Tactic:
apply IsOpenPosMeasure.open_pos (interior K) (μ := ν) (self := i')

Premises used: MeasureTheory.Measure.IsOpenPosMeasure.open_pos, SetLike.coe, interior
-- 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 ν
h :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
i' : ν.IsOpenPosMeasure
⊢ IsOpen (interior (↑K : Set G))

Tactic:
isOpen_interior

Premises used: isOpen_interior
-- 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 ν
h :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
i' : ν.IsOpenPosMeasure
⊢ IsOpen (interior (↑K : Set G))

Tactic:
exact isOpen_interior

Premises used: isOpen_interior
-- 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 ν
h :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
i' : ν.IsOpenPosMeasure
⊢ (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 ⧸ Γ)
μ : 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 ν
h :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
i' : ν.IsOpenPosMeasure
⊢ (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 ⧸ Γ)
μ : 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 ν
h :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
i' : ν.IsOpenPosMeasure
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (interior (↑K : Set G)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_mono_null (interior_subset.trans ?_) <|
      fund_dom_s.measure_zero_of_invariant _ (fun g ↦ QuotientGroup.sound _ _ g) h

Premises used: interior_subset, HasSubset.Subset.trans, MeasureTheory.measure_mono_null, 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 : 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 ν
h :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
i' : ν.IsOpenPosMeasure
cpos : (↑K : Set G) ⊆ (⇑(QuotientGroup.mk' Γ) : (a : G) → G ⧸ Γ) ⁻¹' (↑K' : Set (G ⧸ Γ))
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (interior (↑K : Set G)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine measure_mono_null (interior_subset.trans ?_) <|
      fund_dom_s.measure_zero_of_invariant _ (fun g ↦ QuotientGroup.sound _ _ g) h

Premises used: interior_subset, HasSubset.Subset.trans, MeasureTheory.measure_mono_null, 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 : 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 ν
h :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
i' : ν.IsOpenPosMeasure
cpos : (↑K : Set G) ⊆ preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G))
⊢ (↑K : Set G) ⊆ QuotientGroup.mk ⁻¹' (↑K' : Set (G ⧸ Γ))

Tactic:
change (K : Set G) ⊆ π ⁻¹' π '' K

Premises used: SetLike.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 ⧸ Γ)
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 ν
h :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
i' : ν.IsOpenPosMeasure
⊢ (↑K : Set G) ⊆ preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G))

Tactic:
subset_preimage_image π K

Premises used: QuotientGroup.mk, SetLike.coe, Set.subset_preimage_image
-- 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 ν
h :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
i' : ν.IsOpenPosMeasure
⊢ (↑K : Set G) ⊆ preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G))

Tactic:
exact subset_preimage_image π 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 : 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 :
  Ne (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G)) ∩ s) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
change ν (π ⁻¹' (π '' K) ∩ s) ≠ ⊤
-- 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 :
  LT.lt (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G)) ∩ s) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G)) ∩ s) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
apply ne_of_lt

Premises used: ne_of_lt
-- 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 ν
⊢ LT.lt (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G)) ∩ s) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
lt_of_le_of_lt ?_ finiteCovol.lt_top

Premises used: lt_of_le_of_lt, Ne.lt_top