awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
⊢ ∀ (n : ℕ), ∃ (W : Set G), IsOpen[inst_1] W ∧ 1 ∈ W ∧ ∀ g ∈ W * W, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n

Tactic:
have : ∀ n, ∃ (W : Set G), IsOpen W ∧ 1 ∈ W ∧ ∀ g ∈ W * W, μ ((g • k) \ k) < u n :=
    fun n ↦ exists_open_nhds_one_mul_subset
      (eventually_nhds_one_measure_smul_diff_lt hk h'k (u_mem n).1.ne')
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
this : ∀ (n : ℕ), ∃ (W : Set G), IsOpen[inst_1] W ∧ 1 ∈ W ∧ ∀ g ∈ W * W, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
choose :
  ∀ (W : (n : ℕ) → Set G) (W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)) (mem_W : ∀ (n : ℕ), 1 ∈ W n)
    (hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n), IsGδ k
⊢ IsGδ k

Tactic:
choose W W_open mem_W hW using this
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
this : ⋂ (n : ℕ), V n * k ⊆ k
apply : ∀ (n : ℕ), k ⊆ V n * k
⊢ k = ⋂ (n : ℕ), V n * k

Tactic:
apply Subset.antisymm (subset_iInter_iff.2 (fun n ↦ ?_)) this

Premises used: Set.Subset.antisymm, Iff.mpr, Set.subset_iInter_iff
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
this : ⋂ (n : ℕ), V n * k ⊆ k
n : ℕ
⊢ 1 ∈ V n

Tactic:
simp [V, mem_W]
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
this : ⋂ (n : ℕ), V n * k ⊆ k
n : ℕ
⊢ k ⊆ V n * k

Tactic:
exact subset_mul_right k (by simp [V, mem_W])

Premises used: Set.subset_mul_right
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
this : ⋂ (n : ℕ), V n * k ⊆ k
⊢ k = ⋂ (n : ℕ), V n * k

Tactic:
replace : k = ⋂ n, V n * k := by
      apply Subset.antisymm (subset_iInter_iff.2 (fun n ↦ ?_)) this
      exact subset_mul_right k (by simp [V, mem_W])
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
this : k = ⋂ (n : ℕ), V n * k
rw : IsGδ.{u_2} (X := G) (⋂ (n : ℕ), V n * k)
⊢ IsGδ k

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
this : k = ⋂ (n : ℕ), V n * k
⊢ IsGδ.{u_2} (X := G) (⋂ (n : ℕ), V n * k)

Tactic:
.iInter_of_isOpen fun n ↦ ?_

Premises used: IsGδ.iInter_of_isOpen
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
this : k = ⋂ (n : ℕ), V n * k
refine : ∀ (n : ℕ), IsOpen[inst_1] (V n * k)
⊢ IsGδ.{u_2} (X := G) (⋂ (n : ℕ), V n * k)

Tactic:
refine .iInter_of_isOpen fun n ↦ ?_
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
this : k = ⋂ (n : ℕ), V n * k
n : ℕ
⊢ IsOpen[inst_1] (V n * k)

Tactic:
.mul_right (isOpen_biInter_finset (fun i _hi ↦ W_open i))

Premises used: isOpen_biInter_finset, IsOpen.mul_right
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
this : k = ⋂ (n : ℕ), V n * k
n : ℕ
⊢ IsOpen[inst_1] (V n * k)

Tactic:
exact .mul_right (isOpen_biInter_finset (fun i _hi ↦ W_open i))
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
suffices : ⋂ (n : ℕ), V n * k ⊆ k
⊢ IsGδ k

Tactic:
suffices ⋂ n, V n * k ⊆ k by
    replace : k = ⋂ n, V n * k := by
      apply Subset.antisymm (subset_iInter_iff.2 (fun n ↦ ?_)) this
      exact subset_mul_right k (by simp [V, mem_W])
    rw [this]
    refine .iInter_of_isOpen fun n ↦ ?_
    exact .mul_right (isOpen_biInter_finset (fun i _hi ↦ W_open i))
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
x : G
hx : Membership.mem (γ := Set G) (⋂ (n : ℕ), V n * k) x
choose :
  ∀ (v : (i : ℕ) → G) (hv : ∀ (i : ℕ), v i ∈ V i) (y : (i : ℕ) → G) (hy : ∀ (i : ℕ), y i ∈ k)
    (hvy : ∀ (i : ℕ), (fun (x1 x2 : G) ↦ x1 * x2) (v i) (y i) = x), x ∈ k
⊢ x ∈ k

Tactic:
choose v hv y hy hvy using mem_iInter.1 hx

Premises used: Set.mem_iInter, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
x : G
hx : Membership.mem (γ := Set G) (⋂ (n : ℕ), V n * k) x
v : (i : ℕ) → G
hv : ∀ (i : ℕ), v i ∈ V i
y : (i : ℕ) → G
hy : ∀ (i : ℕ), y i ∈ k
hvy : ∀ (i : ℕ), (fun (x1 x2 : G) ↦ x1 * x2) (v i) (y i) = x
⊢ Filter.map y atTop ≤ 𝓟 k

Tactic:
simp [hy]
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
x : G
hx : Membership.mem (γ := Set G) (⋂ (n : ℕ), V n * k) x
v : (i : ℕ) → G
hv : ∀ (i : ℕ), v i ∈ V i
y : (i : ℕ) → G
hy : ∀ (i : ℕ), y i ∈ k
hvy : ∀ (i : ℕ), (fun (x1 x2 : G) ↦ x1 * x2) (v i) (y i) = x
obtain : ∀ (z : G) (zk : z ∈ k) (hz : MapClusterPt z atTop y), x ∈ k
⊢ x ∈ k

Tactic:
obtain ⟨z, zk, hz⟩ : ∃ z ∈ k, MapClusterPt z atTop y := hk.exists_mapClusterPt (by simp [hy])

Premises used: IsCompact.exists_mapClusterPt
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
x : G
hx : Membership.mem (γ := Set G) (⋂ (n : ℕ), V n * k) x
v : (i : ℕ) → G
hv : ∀ (i : ℕ), v i ∈ V i
y : (i : ℕ) → G
hy : ∀ (i : ℕ), y i ∈ k
hvy : ∀ (i : ℕ), (fun (x1 x2 : G) ↦ x1 * x2) (v i) (y i) = x
z : G
zk : z ∈ k
hz : MapClusterPt z atTop y
n : ℕ
apply : x * z⁻¹ ∈ W n * W n
⊢ (μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) ≤ u n

Tactic:
apply le_of_lt (hW _ _ ?_)

Premises used: le_of_lt
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
x : G
hx : Membership.mem (γ := Set G) (⋂ (n : ℕ), V n * k) x
v : (i : ℕ) → G
hv : ∀ (i : ℕ), v i ∈ V i
y : (i : ℕ) → G
hy : ∀ (i : ℕ), y i ∈ k
hvy : ∀ (i : ℕ), (fun (x1 x2 : G) ↦ x1 * x2) (v i) (y i) = x
z : G
zk : z ∈ k
hz : MapClusterPt z atTop y
n : ℕ
⊢ z ∈ W n * {z}

Tactic:
simp [mem_W]
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
x : G
hx : Membership.mem (γ := Set G) (⋂ (n : ℕ), V n * k) x
v : (i : ℕ) → G
hv : ∀ (i : ℕ), v i ∈ V i
y : (i : ℕ) → G
hy : ∀ (i : ℕ), y i ∈ k
hvy : ∀ (i : ℕ), (fun (x1 x2 : G) ↦ x1 * x2) (v i) (y i) = x
z : G
zk : z ∈ k
hz : MapClusterPt z atTop y
n : ℕ
⊢ W n * {z} ∈ 𝓝 z

Tactic:
have : W n * {z} ∈ 𝓝 z := (IsOpen.mul_right (W_open n)).mem_nhds (by simp [mem_W])
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
x : G
hx : Membership.mem (γ := Set G) (⋂ (n : ℕ), V n * k) x
v : (i : ℕ) → G
hv : ∀ (i : ℕ), v i ∈ V i
y : (i : ℕ) → G
hy : ∀ (i : ℕ), y i ∈ k
hvy : ∀ (i : ℕ), (fun (x1 x2 : G) ↦ x1 * x2) (v i) (y i) = x
z : G
zk : z ∈ k
hz : MapClusterPt z atTop y
n : ℕ
this : W n * {z} ∈ 𝓝 z
⊢ ∃ (i : ℕ), y i ∈ W n * {z} ∧ n < i

Tactic:
((hz.frequently this).and_eventually (eventually_gt_atTop n)).exists

Premises used: Set.Mem, Filter.Frequently.and_eventually, Filter.Frequently.exists, MapClusterPt.frequently, Filter.eventually_gt_atTop
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
x : G
hx : Membership.mem (γ := Set G) (⋂ (n : ℕ), V n * k) x
v : (i : ℕ) → G
hv : ∀ (i : ℕ), v i ∈ V i
y : (i : ℕ) → G
hy : ∀ (i : ℕ), y i ∈ k
hvy : ∀ (i : ℕ), (fun (x1 x2 : G) ↦ x1 * x2) (v i) (y i) = x
z : G
zk : z ∈ k
hz : MapClusterPt z atTop y
n : ℕ
this : W n * {z} ∈ 𝓝 z
obtain : ∀ (i : ℕ) (hi : y i ∈ W n * {z}) (ni : n < i), x * z⁻¹ ∈ W n * W n
⊢ x * z⁻¹ ∈ W n * W n

Tactic:
obtain ⟨i, hi, ni⟩ : ∃ i, y i ∈ W n * {z} ∧ n < i :=
      ((hz.frequently this).and_eventually (eventually_gt_atTop n)).exists

Premises used: Filter.Frequently.and_eventually, Filter.Frequently.exists, MapClusterPt.frequently, Filter.eventually_gt_atTop
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
x : G
hx : Membership.mem (γ := Set G) (⋂ (n : ℕ), V n * k) x
v : (i : ℕ) → G
hv : ∀ (i : ℕ), v i ∈ V i
y : (i : ℕ) → G
hy : ∀ (i : ℕ), y i ∈ k
hvy : ∀ (i : ℕ), (fun (x1 x2 : G) ↦ x1 * x2) (v i) (y i) = x
z : G
zk : z ∈ k
hz : MapClusterPt z atTop y
n : ℕ
this : W n * {z} ∈ 𝓝 z
i : ℕ
hi : y i ∈ W n * {z}
ni : n < i
⊢ y i * z⁻¹ ∈ W n

Tactic:
simpa using hi
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
x : G
hx : Membership.mem (γ := Set G) (⋂ (n : ℕ), V n * k) x
v : (i : ℕ) → G
hv : ∀ (i : ℕ), v i ∈ V i
y : (i : ℕ) → G
hy : ∀ (i : ℕ), y i ∈ k
hvy : ∀ (i : ℕ), (fun (x1 x2 : G) ↦ x1 * x2) (v i) (y i) = x
z : G
zk : z ∈ k
hz : MapClusterPt z atTop y
n : ℕ
this : W n * {z} ∈ 𝓝 z
i : ℕ
hi : y i ∈ W n * {z}
ni : n < i
⊢ (fun (x1 x2 : G) ↦ x1 * x2) (x * (y i)⁻¹) (y i * z⁻¹) = x * z⁻¹

Tactic:
group
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
W : (n : ℕ) → Set G
W_open : ∀ (n : ℕ), IsOpen[inst_1] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < u n
V : (n : ℕ) → Set G := fun (n : ℕ) ↦ ⋂ i ∈ Finset.range n, W i
x : G
hx : Membership.mem (γ := Set G) (⋂ (n : ℕ), V n * k) x
v : (i : ℕ) → G
hv : ∀ (i : ℕ), v i ∈ V i
y : (i : ℕ) → G
hy : ∀ (i : ℕ), y i ∈ k
hvy : ∀ (i : ℕ), (fun (x1 x2 : G) ↦ x1 * x2) (v i) (y i) = x
z : G
zk : z ∈ k
hz : MapClusterPt z atTop y
n : ℕ
this : W n * {z} ∈ 𝓝 z
i : ℕ
hi : y i ∈ W n * {z}
ni : n < i
refine : x * (y i)⁻¹ ∈ W n
⊢ x * z⁻¹ ∈ W n * W n

Tactic:
refine ⟨x * (y i) ⁻¹, ?_, y i * z⁻¹, by simpa using hi, by group⟩