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 ⧸ Γ)
ν : 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∞)
⊢ QuotientMeasureEqMeasurePreimage ν μ
have neg₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞)
  ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk univ ∩ s) : ℝ≥0∞)
Tactic: apply IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set (fund_dom_s := fund_dom_s)
    (meas_V := MeasurableSet.univ)
-- 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 ⧸ Γ)
ν : 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∞)
⊢ QuotientMeasureEqMeasurePreimage ν μ
have neg₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set (fund_dom_s := fund_dom_s)
    (meas_V := MeasurableSet.univ)
-- 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 ⧸ Γ)
ν : 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 : ℝ≥0∞)
have neg : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← h]
-- 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 ⧸ Γ)
ν : 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∞) univ : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk univ ∩ s) : ℝ≥0∞)
have neg : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
  ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk univ ∩ s) : ℝ≥0∞)
Tactic: rw [← h]
-- 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 ⧸ Γ)
ν : 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∞)
have neg : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← h]
-- 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 ν μ
i : HasFundamentalDomain (↥Γ.op) G ν
inst_14 : IsFiniteMeasure μ
⊢ μ.IsHaarMeasure
have obtain : ∀ (K : PositiveCompacts G), μ.IsHaarMeasure
Tactic: obtain ⟨K⟩ := PositiveCompacts.nonempty' (α := 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 ⧸ Γ)
μ : 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
⊢ μ.IsHaarMeasure
have this : μ.IsMulLeftInvariant
Tactic: haveI : IsMulLeftInvariant μ :=
    MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient ν
-- 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 ν μ
i : HasFundamentalDomain (↥Γ.op) G ν
inst_14 : IsFiniteMeasure μ
K : PositiveCompacts G
K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K
this : μ.IsMulLeftInvariant
⊢ μ.IsHaarMeasure
have rw : (HSMul.hSMul (α := ℝ≥0∞) (β := Measure (G ⧸ Γ)) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K' : Set (G ⧸ Γ)) : ℝ≥0∞)
    (haarMeasure K')).IsHaarMeasure
Tactic: rw [haarMeasure_unique μ 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 ⧸ Γ)
μ : 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
⊢ (HSMul.hSMul (α := ℝ≥0∞) (β := Measure (G ⧸ Γ)) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K' : Set (G ⧸ Γ)) : ℝ≥0∞)
      (haarMeasure K')).IsHaarMeasure
have finiteCovol : covolume (↥Γ.op) G ν ≠ ∞
Tactic: have finiteCovol : covolume Γ.op G ν ≠ ⊤ :=
    ne_top_of_lt <| QuotientMeasureEqMeasurePreimage.covolume_ne_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 ν μ
i : HasFundamentalDomain (↥Γ.op) G ν
inst_14 : IsFiniteMeasure μ
K : PositiveCompacts G
K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K
this : μ.IsMulLeftInvariant
finiteCovol : covolume (↥Γ.op) G ν ≠ ∞
⊢ (HSMul.hSMul (α := ℝ≥0∞) (β := Measure (G ⧸ Γ)) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K' : Set (G ⧸ Γ)) : ℝ≥0∞)
      (haarMeasure K')).IsHaarMeasure
have 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
Tactic: obtain ⟨s, fund_dom_s⟩ := i
Cleared hypotheses: i
-- 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 ⧸ Γ)
μ : 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 ν
⊢ (HSMul.hSMul (α := ℝ≥0∞) (β := Measure (G ⧸ Γ)) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K' : Set (G ⧸ Γ)) : ℝ≥0∞)
      (haarMeasure K')).IsHaarMeasure
have finiteCovol₁ : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [fund_dom_s.covolume_eq_volume] at finiteCovol
Cleared hypotheses: finiteCovol, fund_dom_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 ν
⊢ (HSMul.hSMul (α := ℝ≥0∞) (β := Measure (G ⧸ Γ)) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) (↑K' : Set (G ⧸ Γ)) : ℝ≥0∞)
      (haarMeasure K')).IsHaarMeasure
have rw : (HSMul.hSMul (α := ℝ≥0∞) (β := Measure (G ⧸ Γ))
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
    (haarMeasure K')).IsHaarMeasure
Tactic: rw [fund_dom_s.projection_respects_measure_apply μ 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 ⧸ Γ)
μ : 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 ν
⊢ (HSMul.hSMul (α := ℝ≥0∞) (β := Measure (G ⧸ Γ))
      ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
      (haarMeasure K')).IsHaarMeasure
have cpos : Ne (α := ℝ≥0∞)
  ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply IsHaarMeasure.smul
-- 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 ν
cpos :
  Ne (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
    (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
have ctop : Ne (α := ℝ≥0∞)
  ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply IsHaarMeasure.smul
-- 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 ⧸ Γ)
μ : 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∞)
⊢ False
have i' : ν.IsOpenPosMeasure
Tactic: have i' : IsOpenPosMeasure (ν : Measure G) := inferInstance
-- 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 ν
h :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (↑K' : Set (G ⧸ Γ)) ∩ s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
i' : ν.IsOpenPosMeasure
⊢ False
have cpos : IsOpen (interior (↑K : Set G))
Tactic: apply IsOpenPosMeasure.open_pos (interior K) (μ := ν) (self := i')
-- 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 ν
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))
⊢ False
have cpos₁ : (interior (↑K : Set G)).Nonempty
Tactic: apply IsOpenPosMeasure.open_pos (interior K) (μ := ν) (self := i')
-- 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 ν
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
⊢ False
have cpos₂ : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (interior (↑K : Set G)) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply IsOpenPosMeasure.open_pos (interior K) (μ := ν) (self := i')
-- 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 ν
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∞)
have cpos : (↑K : Set G) ⊆ (⇑(QuotientGroup.mk' Γ) : (a : G) → G ⧸ Γ) ⁻¹' (↑K' : Set (G ⧸ Γ))
Tactic: refine measure_mono_null (interior_subset.trans ?_) <|
      fund_dom_s.measure_zero_of_invariant _ (fun g ↦ QuotientGroup.sound _ _ g) h
-- 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 ν
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) ⊆ QuotientGroup.mk ⁻¹' (↑K' : Set (G ⧸ Γ))
have cpos : (↑K : Set G) ⊆ preimage (β := G ⧸ Γ) QuotientGroup.mk (QuotientGroup.mk '' (↑K : Set G))
Tactic: change (K : Set G) ⊆ π ⁻¹' π '' K