awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
g : G
A : Set G
hA : MeasurableSet A
h :
  ∀ (g : G) {K : Compacts G},
    Eq (α := ℝ≥0∞) ((haarContent K₀ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) : ℝ≥0∞)
      ((haarContent K₀ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' A) : ℝ≥0∞)
    (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
apply Content.is_mul_left_invariant_outerMeasure

Premises used: MeasureTheory.Content.is_mul_left_invariant_outerMeasure
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
g : G
A : Set G
hA : MeasurableSet A
⊢ ∀ (g : G) {K : Compacts G},
    Eq (α := ℝ≥0∞) ((haarContent K₀ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) : ℝ≥0∞)
      ((haarContent K₀ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
apply is_left_invariant_haarContent

Premises used: MeasureTheory.Measure.haar.is_left_invariant_haarContent
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
⊢ LocallyCompactSpace G

Tactic:
haveI : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
h0 :
  Ne (α := ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
ht :
  Ne (α := ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((((haarContent K₀).measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G))⁻¹ : ℝ≥0∞)
      ((((haarContent K₀).measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) =
    1

Tactic:
rw [← K₀.isCompact.measure_closure,
    Content.measure_apply _ isClosed_closure.measurableSet, ENNReal.inv_mul_cancel]

Premises used: IsCompact.measure_closure, IsClosed.measurableSet, ENNReal.inv_mul_cancel, TopologicalSpace.PositiveCompacts.isCompact, isClosed_closure, MeasureTheory.Content.measure_apply
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ Ne (α := ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
(haarContent_outerMeasure_closure_pos K₀).ne'

Premises used: LT.lt.ne', MeasureTheory.Measure.haar.haarContent_outerMeasure_closure_pos
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ Ne (α := ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
exact (haarContent_outerMeasure_closure_pos K₀).ne'

Premises used: LT.lt.ne', MeasureTheory.Measure.haar.haarContent_outerMeasure_closure_pos
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ Ne (α := ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
(Content.outerMeasure_lt_top_of_isCompact _ K₀.isCompact.closure).ne

Premises used: IsCompact.closure, TopologicalSpace.PositiveCompacts.isCompact, MeasureTheory.Content.outerMeasure_lt_top_of_isCompact, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ Ne (α := ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
exact (Content.outerMeasure_lt_top_of_isCompact _ K₀.isCompact.closure).ne

Premises used: IsCompact.closure, TopologicalSpace.PositiveCompacts.isCompact, MeasureTheory.Content.outerMeasure_lt_top_of_isCompact, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
hx : Ne (α := ℝ≥0∞) (((((haarContent K₀).measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G))⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Regular (haarMeasure K₀)

Tactic:
apply Regular.smul

Premises used: MeasureTheory.Measure.Regular.smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
hx :
  Ne (α := ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) (((((haarContent K₀).measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G))⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← K₀.isCompact.measure_closure,
    Content.measure_apply _ isClosed_closure.measurableSet, ENNReal.inv_ne_top]

Premises used: IsCompact.measure_closure, ENNReal.inv_ne_top, IsClosed.measurableSet, TopologicalSpace.PositiveCompacts.isCompact, isClosed_closure, MeasureTheory.Content.measure_apply
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
rw : Eq (α := ℝ≥0∞) (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (1 : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) 1 1
⊢ Eq (α := ℝ≥0∞) (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [K₀.isCompact.measure_closure, haarMeasure_self]

Premises used: IsCompact.measure_closure, MeasureTheory.Measure.haarMeasure_self, TopologicalSpace.PositiveCompacts.isCompact
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : SecondCountableTopology G
K₀ : PositiveCompacts G
⊢ LocallyCompactSpace G

Tactic:
haveI : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : SecondCountableTopology G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ SigmaFinite (m0 := inst_3) (haarMeasure K₀)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
h : Ne (α := ℝ≥0∞) (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsHaarMeasure (haarMeasure K₀)

Tactic:
apply
    isHaarMeasure_of_isCompact_nonempty_interior (haarMeasure K₀) K₀ K₀.isCompact
      K₀.interior_nonempty

Premises used: MeasureTheory.Measure.isHaarMeasure_of_isCompact_nonempty_interior, TopologicalSpace.PositiveCompacts.interior_nonempty, MeasureTheory.Measure.haarMeasure, SetLike.coe, TopologicalSpace.PositiveCompacts.isCompact
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
h : Ne (α := ℝ≥0∞) 1 0
⊢ Ne (α := ℝ≥0∞) (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [haarMeasure_self]

Premises used: MeasureTheory.Measure.haarMeasure_self
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
⊢ Ne (α := ℝ≥0∞) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
⊢ Ne (α := ℝ≥0∞) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
⊢ Ne (α := ℝ≥0∞) (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [haarMeasure_self, ne_eq, ENNReal.one_ne_top, not_false_eq_true]

Premises used: MeasureTheory.Measure.haarMeasure_self, ne_eq, not_false_eq_true, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ.InnerRegularCompactLTTop
inst_7 : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEapprox : ∃ K ⊆ E, IsCompact K ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
obtain :
  ∀ (K : Set G) (hKE : K ⊆ E) (hK_comp : IsCompact K)
    (hK_meas : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)),
    ∃ K ⊆ E, IsCompact K ∧ IsClosed[inst_1] K ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ ∃ K ⊆ E, IsCompact K ∧ IsClosed[inst_1] K ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
obtain ⟨K, hKE, hK_comp, hK_meas⟩ := hEapprox
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ.InnerRegularCompactLTTop
inst_7 : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
K : Set G
hKE : K ⊆ E
hK_comp : IsCompact K
hK_meas rwa rwa₁ rwa₂ rwa₃ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (closure[inst_1] K) : ℝ≥0∞)

Tactic:
rwa [hK_comp.measure_closure]

Premises used: IsCompact.measure_closure
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ.InnerRegularCompactLTTop
inst_7 : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
K : Set G
hKE : K ⊆ E
hK_comp : IsCompact K
hK_meas : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ ∃ K ⊆ E, IsCompact K ∧ IsClosed[inst_1] K ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
exact ⟨closure K, hK_comp.closure_subset_measurableSet hE hKE, hK_comp.closure,
      isClosed_closure, by rwa [hK_comp.measure_closure]⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ.InnerRegularCompactLTTop
inst_7 : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEapprox : ∃ K ⊆ E, IsCompact K ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
obtain :
  ∀ (K : Set G) (hKE : K ⊆ E) (hK : IsCompact K) (K_closed : IsClosed[inst_1] K)
    (hKpos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)),
    Membership.mem (γ := Filter G) (𝓝 1) (E / E)
⊢ Membership.mem (γ := Filter G) (𝓝 1) (E / E)

Tactic:
obtain ⟨K, hKE, hK, K_closed, hKpos⟩ : ∃ K ⊆ E, IsCompact K ∧ IsClosed K ∧ 0 < μ K := by
    obtain ⟨K, hKE, hK_comp, hK_meas⟩ := hEapprox
    exact ⟨closure K, hK_comp.closure_subset_measurableSet hE hKE, hK_comp.closure,
      isClosed_closure, by rwa [hK_comp.measure_closure]⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ.InnerRegularCompactLTTop
inst_7 : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEapprox : ∃ K ⊆ E, IsCompact K ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
K : Set G
hKE : K ⊆ E
hK : IsCompact K
K_closed : IsClosed[inst_1] K
hKpos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
h :
  ∀ (g : G) (hg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (g • K \ K) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)),
    g ∈ E / E
⊢ Membership.mem (γ := Filter G) (𝓝 1) (E / E)

Tactic:
filter_upwards [eventually_nhds_one_measure_smul_diff_lt hK K_closed hKpos.ne' (μ := μ)] with g hg

Premises used: LT.lt.ne', MeasureTheory.eventually_nhds_one_measure_smul_diff_lt
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ.InnerRegularCompactLTTop
inst_7 : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEapprox : ∃ K ⊆ E, IsCompact K ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
K : Set G
hKE : K ⊆ E
hK : IsCompact K
K_closed : IsClosed[inst_1] K
hKpos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : G
hg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (g • K \ K) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
hd : Disjoint (g • K) K
⊢ False

Tactic:
simp [hd.symm.sdiff_eq_right, measure_smul] at hg

Premises used: Disjoint.sdiff_eq_right, Disjoint.symm, MeasureTheory.measure_smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ.InnerRegularCompactLTTop
inst_7 : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEapprox : ∃ K ⊆ E, IsCompact K ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
K : Set G
hKE : K ⊆ E
hK : IsCompact K
K_closed : IsClosed[inst_1] K
hKpos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : G
hg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (g • K \ K) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
h : ∀ (x : G) (hxK : x ∈ K) (hgxK : (fun (x : G) ↦ g • x) x ∈ K), g ∈ E / E
⊢ g ∈ E / E

Tactic:
obtain ⟨_, ⟨x, hxK, rfl⟩, hgxK⟩ : ∃ x ∈ g • K, x ∈ K :=
     not_disjoint_iff.1 fun hd ↦ by simp [hd.symm.sdiff_eq_right, measure_smul] at hg

Premises used: Set.not_disjoint_iff, Iff.mp, rfl
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ.InnerRegularCompactLTTop
inst_7 : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEapprox : ∃ K ⊆ E, IsCompact K ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
K : Set G
hKE : K ⊆ E
hK : IsCompact K
K_closed : IsClosed[inst_1] K
hKpos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : G
hg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (g • K \ K) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
x : G
hxK : x ∈ K
hgxK : (fun (x : G) ↦ g • x) x ∈ K
⊢ g ∈ E / E

Tactic:
simpa using div_mem_div (hKE hgxK) (hKE hxK)

Premises used: Set.div_mem_div
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.InnerRegularCompactLTTop
E : Set G
hE : MeasurableSet E
hEpos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) E : ℝ≥0∞)
hEfin : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Membership.mem (γ := Filter G) (𝓝 1) (E / E)

Tactic:
steinhaus_mul_aux μ E hE <| hE.exists_lt_isCompact_of_ne_top hEfin hEpos

Premises used: MeasurableSet.exists_lt_isCompact_of_ne_top, _private.0.MeasureTheory.Measure.steinhaus_mul_aux
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : LocallyCompactSpace G
inst_7 : μ.InnerRegular
E : Set G
hE : MeasurableSet E
hEpos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) E : ℝ≥0∞)
⊢ Membership.mem (γ := Filter G) (𝓝 1) (E / E)

Tactic:
steinhaus_mul_aux μ E hE <| hE.exists_lt_isCompact hEpos

Premises used: _private.0.MeasureTheory.Measure.steinhaus_mul_aux, MeasurableSet.exists_lt_isCompact
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : SecondCountableTopology G
μ : Measure G
inst_6 : SigmaFinite μ
inst_7 : μ.IsMulLeftInvariant
K₀ : PositiveCompacts G
⊢ (interior (closure[inst_1] (↑K₀ : Set G))).Nonempty

Tactic:
have A : Set.Nonempty (interior (closure (K₀ : Set G))) :=
    K₀.interior_nonempty.mono (interior_mono subset_closure)
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : SecondCountableTopology G
μ : Measure G
inst_6 : SigmaFinite μ
inst_7 : μ.IsMulLeftInvariant
K₀ : PositiveCompacts G
A : (interior (closure[inst_1] (↑K₀ : Set G))).Nonempty
⊢ μ =
    HSMul.hSMul (β := Measure G)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
        (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞))
      (haarMeasure K₀)

Tactic:
have := measure_eq_div_smul μ (haarMeasure K₀)
    (measure_pos_of_nonempty_interior _ A).ne' K₀.isCompact.closure.measure_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : SecondCountableTopology G
μ : Measure G
inst_6 : SigmaFinite μ
inst_7 : μ.IsMulLeftInvariant
K₀ : PositiveCompacts G
A : (interior (closure[inst_1] (↑K₀ : Set G))).Nonempty
this :
  μ =
    HSMul.hSMul (β := Measure G)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
        (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞))
      (haarMeasure K₀)
rwa :
  ∀
    (this :
      μ =
        HSMul.hSMul (β := Measure G)
          (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
            (1 : ℝ≥0∞))
          (haarMeasure K₀)),
    μ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)
rwa₁ :
  ∀
    (this :
      μ =
        HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
          (haarMeasure K₀)),
    μ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀
    (this :
      μ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)),
    μ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)
⊢ μ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)

Tactic:
rwa [haarMeasure_closure_self, div_one, K₀.isCompact.measure_closure] at this

Premises used: MeasureTheory.Measure.haarMeasure_closure_self, IsCompact.measure_closure, TopologicalSpace.PositiveCompacts.isCompact, div_one
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : SecondCountableTopology G
K₀ : PositiveCompacts G
μ : Measure G
inst_6 : SigmaFinite μ
inst_7 : μ.IsMulLeftInvariant
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (1 : ℝ≥0∞)
rw :
  haarMeasure K₀ =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)
rw₁ : haarMeasure K₀ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) 1 (haarMeasure K₀)
rw₂ rw₃ : Eq (α := Measure G) (haarMeasure K₀) (haarMeasure K₀)
⊢ haarMeasure K₀ = μ

Tactic:
rw [haarMeasure_unique μ K₀, h, one_smul]

Premises used: MeasureTheory.Measure.haarMeasure_unique, one_smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : SecondCountableTopology G
inst_6 : LocallyCompactSpace G
μ : Measure G
inst_7 : μ.IsHaarMeasure
K₀ : PositiveCompacts G
⊢ μ =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀.toCompacts : Set G) : ℝ≥0∞) (haarMeasure K₀)

Tactic:
haarMeasure_unique μ K₀

Premises used: MeasureTheory.Measure.haarMeasure_unique
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : SecondCountableTopology G
μ : Measure G
inst_6 : SigmaFinite μ
inst_7 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
h2K : (interior K).Nonempty
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  (HSMul.hSMul (α := ℝ≥0∞) (β := Measure G)
      ((μ : (a : Set G) → ℝ≥0∞)
          (↑{ carrier := K, isCompact' := hK, interior_nonempty' := h2K : PositiveCompacts G } : Set G) :
        ℝ≥0∞)
      (haarMeasure { carrier := K, isCompact' := hK, interior_nonempty' := h2K : PositiveCompacts G })).Regular
⊢ μ.Regular

Tactic:
rw [haarMeasure_unique μ ⟨⟨K, hK⟩, h2K⟩]

Premises used: MeasureTheory.Measure.haarMeasure_unique, TopologicalSpace.Compacts.mk, TopologicalSpace.PositiveCompacts.mk
-- Module: Mathlib.MeasureTheory.Measure.Haar.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : SecondCountableTopology G
μ : Measure G
inst_6 : SigmaFinite μ
inst_7 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
h2K : (interior K).Nonempty
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (HSMul.hSMul (α := ℝ≥0∞) (β := Measure G)
      ((μ : (a : Set G) → ℝ≥0∞)
          (↑{ carrier := K, isCompact' := hK, interior_nonempty' := h2K : PositiveCompacts G } : Set G) :
        ℝ≥0∞)
      (haarMeasure { carrier := K, isCompact' := hK, interior_nonempty' := h2K : PositiveCompacts G })).Regular

Tactic:
Regular.smul hμK

Premises used: MeasureTheory.Measure.Regular.smul