awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
A : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
B : u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)
have A₁ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ μ.everywherePosSubset s) : ℝ≥0∞)
Tactic: rw [← B.measure_eq] at A
Cleared hypotheses: A, B
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ.IsEverywherePos s
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
x : α
hx : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)
have rcases : ∀ (t : Set α) (t_mem : t ∈ 𝓝 x)
  (ht : ∀ u ⊆ t, Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)),
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)
Tactic: rcases h x hx with ⟨t, t_mem, ht⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ.IsEverywherePos s
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
x : α
hx : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
t : Set α
t_mem : t ∈ 𝓝 x
ht : ∀ u ⊆ t, Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)
have grw : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (n ∩ t) : ℝ≥0∞)
Tactic: grw [← inter_subset_left (s := n)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ ν : Measure α
s : Set α
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
⊢ ν.IsEverywherePos s ↔ μ.IsEverywherePos s
have refine : ∀ (H : ν.IsEverywherePos s),
  ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
Tactic: refine ⟨fun H ↦ H.of_forall_exists_nhds_eq ?_, fun H ↦ H.of_forall_exists_nhds_eq h⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ ν : Measure α
s : Set α
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
H : ν.IsEverywherePos s
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝 x, ∀ u ⊆ t, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
have rcases : ∀ (t : Set α) (ht : t ∈ 𝓝 x)
  (h't : ∀ u ⊆ t, Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)),
  ∃ t ∈ 𝓝 x, ∀ u ⊆ t, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
Tactic: rcases h x hx with ⟨t, ht, h't⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : μ.IsOpenPosMeasure
hs : IsOpen[inst] s
x : α
xs : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)
have rcases : ∀ (u : Set α) (u_open : IsOpen[inst] u) (xu : x ∈ u) (hu : u ∩ s ⊆ n),
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)
Tactic: rcases mem_nhdsWithin.1 hn with ⟨u, u_open, xu, hu⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : μ.IsOpenPosMeasure
hs : IsOpen[inst] s
x : α
xs : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
u : Set α
u_open : IsOpen[inst] u
xu : x ∈ u
hu : u ∩ s ⊆ n
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)
have apply : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
Tactic: apply lt_of_lt_of_le _ (measure_mono hu)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
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
⊢ IsGδ k
have obtain : ∀ (u : ℕ → ℝ≥0∞) (u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)) (u_lim : Tendsto u atTop (𝓝 0)),
  IsGδ k
Tactic: obtain ⟨u, -, u_mem, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo 0 1)
    ∧ Tendsto u atTop (𝓝 0) := exists_seq_strictAnti_tendsto' (zero_lt_one : (0 : ℝ≥0∞) < 1)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (hypothesis)
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)
⊢ IsGδ k
have this : ∀ (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')
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
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
⊢ IsGδ k
have 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
Tactic: choose W W_open mem_W hW using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
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
have apply : ∀ (n : ℕ), k ⊆ V n * k
Tactic: apply Subset.antisymm (subset_iInter_iff.2 (fun n ↦ ?_)) this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (hypothesis)
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
⊢ IsGδ k
have this₁ : 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])
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
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δ k
have rw : IsGδ.{u_2} (X := G) (⋂ (n : ℕ), V n * k)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
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)
have refine : ∀ (n : ℕ), IsOpen[inst_1] (V n * k)
Tactic: refine .iInter_of_isOpen fun n ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
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
⊢ IsGδ k
have suffices : ⋂ (n : ℕ), V n * k ⊆ 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))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
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
⊢ x ∈ k
have 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
Tactic: choose v hv y hy hvy using mem_iInter.1 hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
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
⊢ x ∈ k
have obtain : ∀ (z : G) (zk : z ∈ k) (hz : MapClusterPt z atTop y), x ∈ k
Tactic: obtain ⟨z, zk, hz⟩ : ∃ z ∈ k, MapClusterPt z atTop y := hk.exists_mapClusterPt (by simp [hy])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
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 : ℕ
⊢ (μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) ≤ u n
have apply : x * z⁻¹ ∈ W n * W n
Tactic: apply le_of_lt (hW _ _ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (hypothesis)
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 : ℕ
⊢ x * z⁻¹ ∈ W n * W n
have this : W n * {z} ∈ 𝓝 z
Tactic: have : W n * {z} ∈ 𝓝 z := (IsOpen.mul_right (W_open n)).mem_nhds (by simp [mem_W])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
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
⊢ x * z⁻¹ ∈ W n * W n
have obtain : ∀ (i : ℕ) (hi : y i ∈ W n * {z}) (ni : n < i), 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
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
⊢ x * z⁻¹ ∈ W n * W n
have refine : x * (y i)⁻¹ ∈ W n
Tactic: refine ⟨x * (y i) ⁻¹, ?_, y i * z⁻¹, by simpa using hi, by group⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (hypothesis)
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
⊢ x * (y i)⁻¹ ∈ W n
have I : V i ⊆ W n
Tactic: have I : V i ⊆ W n := iInter₂_subset n (by simp [ni])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (hypothesis)
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
I : V i ⊆ W n
⊢ x * (y i)⁻¹ ∈ W n
have J : x * (y i)⁻¹ ∈ V i
Tactic: have J : x * (y i)⁻¹ ∈ V i := by simpa [← hvy i] using hv i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (hypothesis)
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
⊢ x ∈ k
have A : ∀ (n : ℕ), (μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) ≤ u n
Tactic: have A n : μ (((x * z⁻¹) • k) \ k) ≤ u n := by
    apply le_of_lt (hW _ _ ?_)
    have : W n * {z} ∈ 𝓝 z := (IsOpen.mul_right (W_open n)).mem_nhds (by simp [mem_W])
    obtain ⟨i, hi, ni⟩ : ∃ i, y i ∈ W n * {z} ∧ n < i :=
      ((hz.frequently this).and_eventually (eventually_gt_atTop n)).exists
    refine ⟨x * (y i) ⁻¹, ?_, y i * z⁻¹, by simpa using hi, by group⟩
    have I : V i ⊆ W n := iInter₂_subset n (by simp [ni])
    have J : x * (y i)⁻¹ ∈ V i := by simpa [← hvy i] using hv i
    exact I J