awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
A : ∀ (n : ℕ), (μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) ≤ u n
⊢ x ∈ k
have B : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have B : μ (((x * z⁻¹) • k) \ k) = 0 :=
    le_antisymm (ge_of_tendsto u_lim (Eventually.of_forall A)) bot_le
-- 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
A : ∀ (n : ℕ), (μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) ≤ u n
B : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (k \ (z * x⁻¹) • k) : ℝ≥0∞) (0 : ℝ≥0∞)
have this : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((z * x⁻¹) • ((x * z⁻¹) • k \ k)) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have : μ ((z * x⁻¹) • (((x * z⁻¹) • k) \ k)) = 0 := by rwa [measure_smul]
-- 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
A : ∀ (n : ℕ), (μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) ≤ u n
B : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) : ℝ≥0∞) (0 : ℝ≥0∞)
this : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((z * x⁻¹) • ((x * z⁻¹) • k \ k)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (k \ (z * x⁻¹) • k) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (k \ (z * x⁻¹) • k) : ℝ≥0∞)
  ((μ : (a : Set G) → ℝ≥0∞) ((z * x⁻¹ * (x * z⁻¹)) • k \ (z * x⁻¹) • k) : ℝ≥0∞)
Tactic: rw [← this, smul_set_sdiff, smul_smul]
-- 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
A : ∀ (n : ℕ), (μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) ≤ u n
B : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) : ℝ≥0∞) (0 : ℝ≥0∞)
this : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((z * x⁻¹) • ((x * z⁻¹) • k \ k)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (k \ (z * x⁻¹) • k) : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞) ((z * x⁻¹ * (x * z⁻¹)) • k \ (z * x⁻¹) • k) : ℝ≥0∞)
have group : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (k \ (z * HPow.hPow (β := ℤ) x (-1)) • k) : ℝ≥0∞)
  ((μ : (a : Set G) → ℝ≥0∞) (HSMul.hSMul (α := G) 1 k \ (z * HPow.hPow (β := ℤ) x (-1)) • k) : ℝ≥0∞)
Tactic: 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
A : ∀ (n : ℕ), (μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) ≤ u n
B : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ x ∈ k
have C : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (k \ (z * x⁻¹) • k) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have C : μ (k \ (z * x⁻¹) • k) = 0 := by
    have : μ ((z * x⁻¹) • (((x * z⁻¹) • k) \ k)) = 0 := by rwa [measure_smul]
    rw [← this, smul_set_sdiff, smul_smul]
    group
    simp
-- 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
A : ∀ (n : ℕ), (μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) ≤ u n
B : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) : ℝ≥0∞) (0 : ℝ≥0∞)
C : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (k \ (z * x⁻¹) • k) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ x ∈ k
have by_contra : ∀ (H : ¬x ∈ k), False
Tactic: by_contra H
-- 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
A : ∀ (n : ℕ), (μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) ≤ u n
B : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) : ℝ≥0∞) (0 : ℝ≥0∞)
C : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (k \ (z * x⁻¹) • k) : ℝ≥0∞) (0 : ℝ≥0∞)
H : ¬x ∈ k
⊢ k ∩ ((z * x⁻¹) • k)ᶜ ∈ 𝓝[k] z
have apply : ((z * x⁻¹) • k)ᶜ ∈ 𝓝 z
Tactic: apply inter_mem_nhdsWithin k
-- 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
A : ∀ (n : ℕ), (μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) ≤ u n
B : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) : ℝ≥0∞) (0 : ℝ≥0∞)
C : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (k \ (z * x⁻¹) • k) : ℝ≥0∞) (0 : ℝ≥0∞)
H : ¬x ∈ k
⊢ ((z * x⁻¹) • k)ᶜ ∈ 𝓝 z
have apply : z ∈ ((z * x⁻¹) • k)ᶜ
Tactic: apply IsOpen.mem_nhds (by simpa using h'k.smul _)
-- 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
A : ∀ (n : ℕ), (μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) ≤ u n
B : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) : ℝ≥0∞) (0 : ℝ≥0∞)
C : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (k \ (z * x⁻¹) • k) : ℝ≥0∞) (0 : ℝ≥0∞)
H : ¬x ∈ k
⊢ z ∉ (z * x⁻¹) • k
have contrapose : ∀ (H : z ∈ (z * x⁻¹) • k), x ∈ k
Tactic: contrapose H
Cleared hypotheses: H
-- 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
A : ∀ (n : ℕ), (μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) ≤ u n
B : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) : ℝ≥0∞) (0 : ℝ≥0∞)
C : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (k \ (z * x⁻¹) • k) : ℝ≥0∞) (0 : ℝ≥0∞)
H : ¬x ∈ k
⊢ False
have this : k ∩ ((z * x⁻¹) • k)ᶜ ∈ 𝓝[k] z
Tactic: have : k ∩ ((z * x⁻¹) • k)ᶜ ∈ 𝓝[k] z := by
    apply inter_mem_nhdsWithin k
    apply IsOpen.mem_nhds (by simpa using h'k.smul _)
    push _ ∈ _
    contrapose H
    simpa [mem_smul_set_iff_inv_smul_mem] using H
-- 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
A : ∀ (n : ℕ), (μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) ≤ u n
B : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) : ℝ≥0∞) (0 : ℝ≥0∞)
C : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (k \ (z * x⁻¹) • k) : ℝ≥0∞) (0 : ℝ≥0∞)
H : ¬x ∈ k
this : k ∩ ((z * x⁻¹) • k)ᶜ ∈ 𝓝[k] z
⊢ False
have this₁ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (k \ (z * x⁻¹) • k) : ℝ≥0∞)
Tactic: have : 0 < μ (k \ ((z * x⁻¹) • k)) := h z zk _ 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
⊢ μ.InnerRegularWRT (fun (s : Set G) ↦ ∃ (f : G → ℝ), Continuous[inst_1, _] f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1})
    fun (s : Set G) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have apply : μ.InnerRegularWRT (fun (s : Set G) ↦ ∃ (f : G → ℝ), Continuous[inst_1, _] f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1})
  fun (s : Set G) ↦ IsCompact s ∧ IsClosed[inst_1] s
Tactic: apply InnerRegularWRT.trans _ innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group
-- 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
⊢ (fun (s : Set G) ↦ IsCompact s ∧ IsClosed[inst_1] s) K →
    ∀ r < (μ : (a : Set G) → ℝ≥0∞) K,
      ∃ K_1 ⊆ K,
        (fun (s : Set G) ↦ ∃ (f : G → ℝ), Continuous[inst_1, _] f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) K_1 ∧
          r < (μ : (a : Set G) → ℝ≥0∞) K_1
have this : ∀ (K_comp : IsCompact K) (K_closed : IsClosed[inst_1] K),
  ∀ r < (μ : (a : Set G) → ℝ≥0∞) K,
    ∃ K_1 ⊆ K,
      (fun (s : Set G) ↦ ∃ (f : G → ℝ), Continuous[inst_1, _] f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) K_1 ∧
        r < (μ : (a : Set G) → ℝ≥0∞) K_1
Tactic: ⟨K_comp, K_closed⟩
-- 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
K_comp : IsCompact K
K_closed : IsClosed[inst_1] K
r : ℝ≥0∞
hr : r < (μ : (a : Set G) → ℝ≥0∞) K
L : Set G := μ.everywherePosSubset K
⊢ ∃ K_1 ⊆ K,
    (fun (s : Set G) ↦ ∃ (f : G → ℝ), Continuous[inst_1, _] f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) K_1 ∧
      r < (μ : (a : Set G) → ℝ≥0∞) K_1
have L_comp : IsCompact L
Tactic: have L_comp : IsCompact L := K_comp.everywherePosSubset
-- 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
K_comp : IsCompact K
K_closed : IsClosed[inst_1] K
r : ℝ≥0∞
hr : r < (μ : (a : Set G) → ℝ≥0∞) K
L : Set G := μ.everywherePosSubset K
L_comp : IsCompact L
⊢ ∃ K_1 ⊆ K,
    (fun (s : Set G) ↦ ∃ (f : G → ℝ), Continuous[inst_1, _] f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) K_1 ∧
      r < (μ : (a : Set G) → ℝ≥0∞) K_1
have L_closed : IsClosed[inst_1] L
Tactic: have L_closed : IsClosed L := K_closed.everywherePosSubset
-- 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
K_comp : IsCompact K
K_closed : IsClosed[inst_1] K
r : ℝ≥0∞
hr : r < (μ : (a : Set G) → ℝ≥0∞) K
L : Set G := μ.everywherePosSubset K
L_comp : IsCompact L
L_closed : IsClosed[inst_1] L
⊢ ∃ K_1 ⊆ K,
    (fun (s : Set G) ↦ ∃ (f : G → ℝ), Continuous[inst_1, _] f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) K_1 ∧
      r < (μ : (a : Set G) → ℝ≥0∞) K_1
have refine_1 : (fun (s : Set G) ↦ ∃ (f : G → ℝ), Continuous[inst_1, _] f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) L
Tactic: refine ⟨L, everywherePosSubset_subset μ K, ?_, ?_⟩
-- 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
K_comp : IsCompact K
K_closed : IsClosed[inst_1] K
r : ℝ≥0∞
hr : r < (μ : (a : Set G) → ℝ≥0∞) K
L : Set G := μ.everywherePosSubset K
L_comp : IsCompact L
L_closed : IsClosed[inst_1] L
refine_1 : (fun (s : Set G) ↦ ∃ (f : G → ℝ), Continuous[inst_1, _] f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) L
⊢ ∃ K_1 ⊆ K,
    (fun (s : Set G) ↦ ∃ (f : G → ℝ), Continuous[inst_1, _] f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) K_1 ∧
      r < (μ : (a : Set G) → ℝ≥0∞) K_1
have refine_2 : r < (μ : (a : Set G) → ℝ≥0∞) L
Tactic: refine ⟨L, everywherePosSubset_subset μ K, ?_, ?_⟩
-- 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
K_comp : IsCompact K
K_closed : IsClosed[inst_1] K
r : ℝ≥0∞
hr : r < (μ : (a : Set G) → ℝ≥0∞) K
L : Set G := μ.everywherePosSubset K
L_comp : IsCompact L
L_closed : IsClosed[inst_1] L
⊢ (fun (s : Set G) ↦ ∃ (f : G → ℝ), Continuous[inst_1, _] f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) L
have this : μ.IsEverywherePos L
Tactic: have : μ.IsEverywherePos L :=
      isEverywherePos_everywherePosSubset_of_measure_ne_top K_closed.measurableSet
      K_comp.measure_lt_top.ne
-- 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
K_comp : IsCompact K
K_closed : IsClosed[inst_1] K
r : ℝ≥0∞
hr : r < (μ : (a : Set G) → ℝ≥0∞) K
L : Set G := μ.everywherePosSubset K
L_comp : IsCompact L
L_closed : IsClosed[inst_1] L
this : μ.IsEverywherePos L
⊢ (fun (s : Set G) ↦ ∃ (f : G → ℝ), Continuous[inst_1, _] f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) L
have L_Gδ : IsGδ L
Tactic: have L_Gδ : IsGδ L := this.IsGdelta_of_isMulLeftInvariant L_comp L_closed
-- 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
K_comp : IsCompact K
K_closed : IsClosed[inst_1] K
r : ℝ≥0∞
hr : r < (μ : (a : Set G) → ℝ≥0∞) K
L : Set G := μ.everywherePosSubset K
L_comp : IsCompact L
L_closed : IsClosed[inst_1] L
this : μ.IsEverywherePos L
L_Gδ : IsGδ L
⊢ (fun (s : Set G) ↦ ∃ (f : G → ℝ), Continuous[inst_1, _] f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) L
have refine_1 : ∀ (f : G → ℝ) (f_cont : Continuous[inst_1, _] f)
  (Lf : L = preimage (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) {1})
  (f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)),
  (fun (s : Set G) ↦ ∃ (f : G → ℝ), Continuous[inst_1, _] f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) L
Tactic: obtain ⟨⟨f, f_cont⟩, Lf, -, f_comp, -⟩ : ∃ f : C(G, ℝ), L = f ⁻¹' {1} ∧ EqOn f 0 ∅
        ∧ HasCompactSupport f ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 :=
      exists_continuous_one_zero_of_isCompact_of_isGδ L_comp L_Gδ isClosed_empty
        (disjoint_empty L)