awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : IsFiniteMeasureOnCompacts μ
inst_7 : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst_1] k
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set G
hUk : k ⊆ U
hU : IsOpen[inst_1] U
hμUk : (μ : (a : Set G) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) k : ℝ≥0∞) ε
V : Set G
hV1 : Membership.mem (γ := Filter G) (𝓝 1) V
hVkU : V * k ⊆ U
g : G
hg : g ∈ V
⊢ (μ : (a : Set G) → ℝ≥0∞) (U \ k) < ε

Tactic:
measure_diff_lt_of_lt_add h'k.nullMeasurableSet hUk hk.measure_lt_top.ne hμUk

Premises used: MeasureTheory.measure_diff_lt_of_lt_add, IsCompact.measure_lt_top, IsClosed.nullMeasurableSet, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : IsFiniteMeasureOnCompacts μ
inst_7 : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst_1] k
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set G
hUk : k ⊆ U
hU : IsOpen[inst_1] U
hμUk : (μ : (a : Set G) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) k : ℝ≥0∞) ε
V : Set G
hV1 : Membership.mem (γ := Filter G) (𝓝 1) V
hVkU : V * k ⊆ U
g : G
hg : g ∈ V
μ₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (g • k \ k) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (U \ k) : ℝ≥0∞)
⊢ (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < ε

Tactic:
calc
    μ (g • k \ k) ≤ μ (U \ k) := by
      gcongr
      exact (smul_set_subset_smul hg).trans hVkU
    _ < ε := measure_diff_lt_of_lt_add h'k.nullMeasurableSet hUk hk.measure_lt_top.ne hμUk

Premises used: MeasureTheory.measure_diff_lt_of_lt_add, SDiff.sdiff, IsCompact.measure_lt_top, IsClosed.nullMeasurableSet, HSMul.hSMul, DFunLike.coe, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : IsFiniteMeasureOnCompacts μ
inst_7 : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst_1] k
⊢ Tendsto (β := ℝ≥0∞) (fun (g : G) ↦ (μ : (a : Set G) → ℝ≥0∞) (g • k \ k)) (𝓝 1) (𝓝 0)

Tactic:
ENNReal.nhds_zero_basis.tendsto_right_iff.mpr <| fun _ h ↦
    eventually_nhds_one_measure_smul_diff_lt hk h'k h.ne'

Premises used: Iff.mpr, LT.lt.ne', ENNReal.nhds_zero_basis, MeasureTheory.eventually_nhds_one_measure_smul_diff_lt, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.IsOpenPosMeasure

Tactic:
⟨fun U hU hne => ?_⟩

Premises used: MeasureTheory.Measure.IsOpenPosMeasure.mk
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
refine :
  ∀ (U : Set G) (hU : IsOpen[inst_1] U) (hne : U.Nonempty),
    Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.IsOpenPosMeasure

Tactic:
refine ⟨fun U hU hne => ?_⟩
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set G
hU : IsOpen[inst_1] U
hne : U.Nonempty
contrapose :
  ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
contrapose h
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen[inst_1] U
hne : U.Nonempty
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen[inst_1] U
hne : U.Nonempty
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (interior U).Nonempty

Tactic:
rw [← hU.interior_eq] at hne

Premises used: IsOpen.interior_eq
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen[inst_1] U
hne : U.Nonempty
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
hne₁ : (interior U).Nonempty
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← hU.interior_eq] at hne

Premises used: IsOpen.interior_eq
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen[inst_1] U
hne : (interior U).Nonempty
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (t : Finset G), K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' U

Tactic:
compact_covered_by_mul_left_translates hK hne

Premises used: compact_covered_by_mul_left_translates
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen[inst_1] U
hne : (interior U).Nonempty
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
obtain :
  ∀ (t : Finset G) (hKt : K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' U),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
obtain ⟨t, hKt⟩ : ∃ t : Finset G, K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h : G => g * h) ⁻¹' U :=
    compact_covered_by_mul_left_translates hK hne

Premises used: Finset, compact_covered_by_mul_left_translates
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen[inst_1] U
hne : (interior U).Nonempty
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
t : Finset G
hKt : K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' U
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞) (⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' U) : ℝ≥0∞)

Tactic:
measure_mono hKt

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen[inst_1] U
hne : (interior U).Nonempty
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
t : Finset G
hKt : K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' U
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' U) : ℝ≥0∞)
    (∑ g ∈ t, (μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' U) : ℝ≥0∞)

Tactic:
measure_biUnion_finset_le _ _

Premises used: MeasureTheory.measure_biUnion_finset_le
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen[inst_1] U
hne : (interior U).Nonempty
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
t : Finset G
hKt : K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' U
⊢ Eq (α := ℝ≥0∞) (∑ g ∈ t, (μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' U)) 0

Tactic:
simp [measure_preimage_mul, h]

Premises used: MeasureTheory.measure_preimage_mul
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen[inst_1] U
hne : (interior U).Nonempty
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
t : Finset G
hKt : K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' U
μ₁ : Eq (α := ℝ≥0∞) (∑ g ∈ t, (μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' U)) 0
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
calc
    μ K ≤ μ (⋃ (g : G) (_ : g ∈ t), (fun h : G => g * h) ⁻¹' U) := measure_mono hKt
    _ ≤ ∑ g ∈ t, μ ((fun h : G => g * h) ⁻¹' U) := measure_biUnion_finset_le _ _
    _ = 0 := by simp [measure_preimage_mul, h]

Premises used: HMul.hMul, MeasureTheory.measure_biUnion_finset_le, Set.preimage, MeasureTheory.measure_mono, DFunLike.coe, Set.iUnion
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : TopologicalSpace G
inst_3 : BorelSpace G
μ : Measure G
inst_4 : Group G
inst_5 : IsTopologicalGroup G
inst_6 : μ.IsMulLeftInvariant
inst_7 : μ.Regular
inst_8 : NeZero μ
⊢ μ.IsOpenPosMeasure

Tactic:
let ⟨K, hK, h2K⟩ := Regular.exists_isCompact_not_null.mpr (NeZero.ne μ)
  isOpenPosMeasure_of_mulLeftInvariant_of_compact K hK h2K

Premises used: Iff.mpr, _private.0.MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_regular.match_1, MeasureTheory.Measure.IsOpenPosMeasure, MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_compact, MeasureTheory.Measure.Regular.exists_isCompact_not_null, NeZero.ne
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : TopologicalSpace G
inst_3 : BorelSpace G
μ : Measure G
inst_4 : Group G
inst_5 : IsTopologicalGroup G
inst_6 : μ.IsMulLeftInvariant
inst_7 : μ.InnerRegular
inst_8 : NeZero μ
⊢ μ.IsOpenPosMeasure

Tactic:
let ⟨K, hK, h2K⟩ := InnerRegular.exists_isCompact_not_null.mpr (NeZero.ne μ)
  isOpenPosMeasure_of_mulLeftInvariant_of_compact K hK h2K

Premises used: Iff.mpr, _private.0.MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_regular.match_1, MeasureTheory.Measure.IsOpenPosMeasure, MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_compact, MeasureTheory.Measure.InnerRegular.exists_isCompact_not_null, NeZero.ne
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
inst_6 : μ.Regular
s : Set G
hs : IsOpen[inst_1] s
inl :
  ∀ [IsMulLeftInvariant.{u_1} (G := G) 0] [Regular.{u_1} (α := G) 0],
    Eq (α := ℝ≥0∞) (((0 : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
      s = ∅ ∨ Eq.{u_1 + 1} (α := Measure G) 0 0
inr : ∀ (hμ : NeZero μ), Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔ s = ∅ ∨ μ = 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔ s = ∅ ∨ μ = 0

Tactic:
rcases eq_zero_or_neZero μ with rfl | hμ

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
s : Set G
hs : IsOpen[inst_1] s
inst_5 : IsMulLeftInvariant.{u_1} (G := G) 0
inst_6 : Regular.{u_1} (α := G) 0
⊢ Eq (α := ℝ≥0∞) (((0 : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    s = ∅ ∨ Eq.{u_1 + 1} (α := Measure G) 0 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
inst_6 : μ.Regular
s : Set G
hs : IsOpen[inst_1] s
hμ : NeZero μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔ s = ∅ ∨ μ = 0

Tactic:
simp only [or_false, hs.measure_eq_zero_iff μ, NeZero.ne μ]

Premises used: or_false, IsOpen.measure_eq_zero_iff, NeZero.ne
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
inst_6 : μ.Regular
hμ : μ ≠ 0
s : Set G
hs : IsOpen[inst_1] s
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔ s.Nonempty

Tactic:
simpa [null_iff_of_isMulLeftInvariant (μ := μ) hs, hμ] using nonempty_iff_ne_empty.symm

Premises used: Set.nonempty_iff_ne_empty, MeasureTheory.null_iff_of_isMulLeftInvariant, Iff.symm
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
inst_6 : μ.Regular
h3μ : μ ≠ 0
s : Set G
hs : IsOpen[inst_1] s
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ↔ s.Nonempty

Tactic:
pos_iff_ne_zero.trans <| measure_ne_zero_iff_nonempty_of_isMulLeftInvariant h3μ hs

Premises used: MeasureTheory.measure_ne_zero_iff_nonempty_of_isMulLeftInvariant, Iff.trans, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
U : Set G
hU : IsOpen[inst_1] U
h'U : U.Nonempty
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
K : Set G
hK : IsCompact K
rw :
  ∀ (h'U : (interior U).Nonempty) (h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)) {K : Set G}
    (hK : IsCompact K), LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← hU.interior_eq] at h'U

Premises used: IsOpen.interior_eq
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
U : Set G
hU : IsOpen[inst_1] U
h'U : (interior U).Nonempty
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
K : Set G
hK : IsCompact K
⊢ ∃ (t : Finset G), K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' U

Tactic:
compact_covered_by_mul_left_translates hK h'U

Premises used: compact_covered_by_mul_left_translates
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
U : Set G
hU : IsOpen[inst_1] U
h'U : (interior U).Nonempty
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
K : Set G
hK : IsCompact K
obtain :
  ∀ (t : Finset G) (hKt : K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' U),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
obtain ⟨t, hKt⟩ : ∃ t : Finset G, K ⊆ ⋃ g ∈ t, (fun h : G => g * h) ⁻¹' U :=
    compact_covered_by_mul_left_translates hK h'U

Premises used: Finset, compact_covered_by_mul_left_translates
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
U : Set G
hU : IsOpen[inst_1] U
h'U : (interior U).Nonempty
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
K : Set G
hK : IsCompact K
t : Finset G
hKt : K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' U
⊢ ∀ i ∈ (↑t : Set G), LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ i * h) ⁻¹' U) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [h.lt_top]

Premises used: Ne.lt_top
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
U : Set G
hU : IsOpen[inst_1] U
h'U : (interior U).Nonempty
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
K : Set G
hK : IsCompact K
t : Finset G
hKt : K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' U
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact (measure_mono hKt).trans_lt <| measure_biUnion_lt_top t.finite_toSet <| by simp [h.lt_top]

Premises used: MeasureTheory.measure_biUnion_lt_top, MeasureTheory.measure_mono, Finset.finite_toSet, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
U : Set G
hU : (interior U).Nonempty
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
K : Set G
hK : IsCompact K
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_lt_top_of_isCompact_of_isMulLeftInvariant (interior U) isOpen_interior hU
    ((measure_mono interior_subset).trans_lt (lt_top_iff_ne_top.2 h)).ne hK

Premises used: Iff.mpr, interior_subset, isOpen_interior, MeasureTheory.measure_lt_top_of_isCompact_of_isMulLeftInvariant, lt_top_iff_ne_top, interior, MeasureTheory.measure_mono, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
⊢ ∃ (K : Set G), Membership.mem (γ := Filter G) (𝓝 1) K ∧ IsCompact K ∧ IsClosed[inst_1] K

Tactic:
exists_mem_nhds_isCompact_isClosed 1

Premises used: exists_mem_nhds_isCompact_isClosed, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
obtain :
  ∀ (K : Set G) (K1 : Membership.mem (γ := Filter G) (𝓝 1) K) (hK : IsCompact K) (Kclosed : IsClosed[inst_1] K),
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
obtain ⟨K, K1, hK, Kclosed⟩ : ∃ K ∈ 𝓝 (1 : G), IsCompact K ∧ IsClosed K :=
    exists_mem_nhds_isCompact_isClosed 1

Premises used: nhds, exists_mem_nhds_isCompact_isClosed, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
have K_pos : 0 < μ K := measure_pos_of_mem_nhds μ K1
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ ∀ (L : Set G), IsCompact L → ∃ (g : G), Disjoint L (g • K)

Tactic:
have A : ∀ L : Set G, IsCompact L → ∃ g : G, Disjoint L (g • K) := fun L hL =>
    exists_disjoint_smul_of_isCompact hL hK
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
A : ∀ (L : Set G), IsCompact L → ∃ (g : G), Disjoint L (g • K)
choose! :
  ∀ (g : (L : Set G) → G) (hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
choose! g hg using A
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : (L : Set G) → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun (n : ℕ) ↦ (fun (T : Set G) ↦ T ∪ g T • K)^[n] K
⊢ IsCompact (L 0)

Tactic:
hK

Premises used: Nat.iterate
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : (L : Set G) → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun (n : ℕ) ↦ (fun (T : Set G) ↦ T ∪ g T • K)^[n] K
⊢ IsCompact (L 0)

Tactic:
exact hK
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : (L : Set G) → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun (n : ℕ) ↦ (fun (T : Set G) ↦ T ∪ g T • K)^[n] K
n : ℕ
IH : IsCompact (L n)
succ : IsCompact (X := G) (((fun (T : Set G) ↦ T ∪ g T • K) ∘ (fun (T : Set G) ↦ T ∪ g T • K)^[n]) K)
⊢ IsCompact (L (n + 1))

Tactic:
simp_rw [L, iterate_succ']

Premises used: Function.iterate_succ'