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)
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
⊢ n ∈ Finset.range i

Tactic:
simp [ni]
-- 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
⊢ V i ⊆ W n

Tactic:
have I : V i ⊆ W n := iInter₂_subset n (by simp [ni])
-- 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
I : V i ⊆ W n
⊢ x * (y i)⁻¹ ∈ V i

Tactic:
simpa [← hvy i] using hv 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
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)⁻¹ ∈ V i

Tactic:
have J : x * (y i)⁻¹ ∈ V i := by simpa [← hvy i] using hv 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
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
J : x * (y i)⁻¹ ∈ V i
⊢ x * (y i)⁻¹ ∈ W n

Tactic:
I J
-- 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
I : V i ⊆ W n
J : x * (y i)⁻¹ ∈ V i
⊢ x * (y i)⁻¹ ∈ W n

Tactic:
exact I J
-- 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 : ℕ), (μ : (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
-- 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
A : ∀ (n : ℕ), (μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) ≤ u n
⊢ 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
-- 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
A : ∀ (n : ℕ), (μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) ≤ u n
B rwa rwa₁ rwa₂ rwa₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((x * z⁻¹) • k \ k) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((z * x⁻¹) • ((x * z⁻¹) • k \ k)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rwa [measure_smul]

Premises used: MeasureTheory.measure_smul
-- 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
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∞) ((z * x⁻¹) • ((x * z⁻¹) • k \ k)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have : μ ((z * x⁻¹) • (((x * z⁻¹) • k) \ k)) = 0 := by rwa [measure_smul]
-- 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
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∞)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (k \ (z * x⁻¹) • k) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← this, smul_set_sdiff, smul_smul]

Premises used: smul_smul, Set.smul_set_sdiff
-- 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
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∞)
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∞)
⊢ 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:
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
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 * HPow.hPow (β := ℤ) x (-1)) • k) : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞) (HSMul.hSMul (α := G) 1 k \ (z * HPow.hPow (β := ℤ) x (-1)) • k) : ℝ≥0∞)

Tactic:
simp
-- 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
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∞)

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
-- 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
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∞)
by_contra : ∀ (H : ¬x ∈ k), False
⊢ x ∈ k

Tactic:
by_contra H
-- 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
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
apply : ((z * x⁻¹) • k)ᶜ ∈ 𝓝 z
⊢ k ∩ ((z * x⁻¹) • k)ᶜ ∈ 𝓝[k] z

Tactic:
apply inter_mem_nhdsWithin k

Premises used: inter_mem_nhdsWithin
-- 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
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
⊢ IsOpen[inst_1] ((z * x⁻¹) • k)ᶜ

Tactic:
simpa using h'k.smul _

Premises used: IsClosed.smul
-- 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
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
apply : z ∈ ((z * x⁻¹) • k)ᶜ
⊢ ((z * x⁻¹) • k)ᶜ ∈ 𝓝 z

Tactic:
apply IsOpen.mem_nhds (by simpa using h'k.smul _)

Premises used: IsOpen.mem_nhds