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
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
contrapose : ∀ (H : z ∈ (z * x⁻¹) • k), x ∈ k
⊢ z ∉ (z * x⁻¹) • k

Tactic:
contrapose 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 : z ∈ (z * x⁻¹) • k
⊢ x ∈ k

Tactic:
simpa [mem_smul_set_iff_inv_smul_mem] using H

Premises used: Set.mem_smul_set_iff_inv_smul_mem
-- 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
⊢ 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
-- 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
this : k ∩ ((z * x⁻¹) • k)ᶜ ∈ 𝓝[k] z
⊢ 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
-- 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
this_1 : k ∩ ((z * x⁻¹) • k)ᶜ ∈ 𝓝[k] z
this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (k \ (z * x⁻¹) • k) : ℝ≥0∞)
⊢ False

Tactic:
lt_irrefl _ (C.le.trans_lt this)

Premises used: lt_irrefl, Eq.le, LE.le.trans_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
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_1 : k ∩ ((z * x⁻¹) • k)ᶜ ∈ 𝓝[k] z
this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (k \ (z * x⁻¹) • k) : ℝ≥0∞)
⊢ False

Tactic:
exact lt_irrefl _ (C.le.trans_lt this)

Premises used: lt_irrefl, Eq.le, LE.le.trans_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
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
⊢ μ.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∞)

Tactic:
apply InnerRegularWRT.trans _ innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group

Premises used: MeasureTheory.Measure.InnerRegularWRT.trans, MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_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
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
⊢ (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

Tactic:
⟨K_comp, K_closed⟩
-- 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
K_comp : IsCompact K
K_closed : IsClosed[inst_1] K
r : ℝ≥0∞
hr : r < (μ : (a : Set G) → ℝ≥0∞) K
L : Set G := μ.everywherePosSubset K
⊢ IsCompact L

Tactic:
have L_comp : IsCompact L := K_comp.everywherePosSubset
-- 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
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
⊢ IsClosed[inst_1] L

Tactic:
have L_closed : IsClosed L := K_closed.everywherePosSubset
-- 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
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

Tactic:
⟨L, everywherePosSubset_subset μ K, ?_, ?_⟩

Premises used: And.intro, Exists.intro, MeasureTheory.Measure.everywherePosSubset_subset
-- 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
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
refine_2 : r < (μ : (a : Set G) → ℝ≥0∞) 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

Tactic:
refine ⟨L, everywherePosSubset_subset μ K, ?_, ?_⟩
-- 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
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
⊢ μ.IsEverywherePos L

Tactic:
have : μ.IsEverywherePos L :=
      isEverywherePos_everywherePosSubset_of_measure_ne_top K_closed.measurableSet
      K_comp.measure_lt_top.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
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
⊢ IsGδ L

Tactic:
have L_Gδ : IsGδ L := this.IsGdelta_of_isMulLeftInvariant L_comp L_closed
-- 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
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
⊢ ∃ (f : C(G, ℝ)),
    L = preimage (β := ℝ) (⇑f : (a : G) → ℝ) {1} ∧
      EqOn (α := G) (β := ℝ) (⇑f : (a : G) → ℝ) 0 ∅ ∧
        HasCompactSupport (α := G) (β := ℝ) (⇑f : (a : G) → ℝ) ∧
          ∀ (x : G), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : G) → ℝ) x : ℝ)

Tactic:
exists_continuous_one_zero_of_isCompact_of_isGδ L_comp L_Gδ isClosed_empty
        (disjoint_empty L)

Premises used: isClosed_empty, Set.disjoint_empty, exists_continuous_one_zero_of_isCompact_of_isGδ
-- 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
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
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
⊢ (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)

Premises used: isClosed_empty, Set.disjoint_empty, exists_continuous_one_zero_of_isCompact_of_isGδ
-- 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
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
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:
⟨f, f_cont, f_comp, Lf⟩

Premises used: And.intro, Exists.intro
-- 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
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
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:
exact ⟨f, f_cont, f_comp, Lf⟩
-- 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
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
⊢ r < (μ : (a : Set G) → ℝ≥0∞) K

Tactic:
hr
-- 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
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
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) L : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ r < (μ : (a : Set G) → ℝ≥0∞) L

Tactic:
convert! hr using 1
-- 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
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
h : L =ᶠ[ae μ] K
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) L : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
apply measure_congr

Premises used: MeasureTheory.measure_congr
-- 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
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
⊢ L =ᶠ[ae μ] K

Tactic:
everywherePosSubset_ae_eq_of_measure_ne_top K_closed.measurableSet
      K_comp.measure_lt_top.ne

Premises used: IsClosed.measurableSet, MeasureTheory.Measure.everywherePosSubset_ae_eq_of_measure_ne_top, IsCompact.measure_lt_top, LT.lt.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
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
⊢ L =ᶠ[ae μ] K

Tactic:
exact everywherePosSubset_ae_eq_of_measure_ne_top K_closed.measurableSet
      K_comp.measure_lt_top.ne

Premises used: IsClosed.measurableSet, MeasureTheory.Measure.everywherePosSubset_ae_eq_of_measure_ne_top, IsCompact.measure_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
s t : Set Ω
μ : FiniteMeasure Ω
⊢ IsFiniteMeasure (↑μ : Measure Ω)

Tactic:
μ.prop

Premises used: Subtype.prop, MeasureTheory.FiniteMeasure.toMeasure
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : FiniteMeasure Ω
⊢ (↑ν : Measure Ω) = (↑ν : Measure Ω)

Tactic:
rfl

Premises used: MeasureTheory.FiniteMeasure.toMeasure, rfl
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := FiniteMeasure Ω) toMeasure

Tactic:
Subtype.coe_injective

Premises used: MeasureTheory.FiniteMeasure, Subtype.coe_injective, MeasureTheory.FiniteMeasure.toMeasure
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
s_1 t : Set Ω
μ ν : FiniteMeasure Ω
h :
  Eq.{max (u_1 + 1) 1} (α := (a : Set Ω) → ℝ≥0)
    ((fun (μ : FiniteMeasure Ω) (s : Set Ω) ↦ ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s)) μ)
    ((fun (μ : FiniteMeasure Ω) (s : Set Ω) ↦ ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s)) ν)
s : Set Ω
h_1 : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simpa [ENNReal.toNNReal_eq_toNNReal_iff, measure_ne_top] using congr_fun h s

Premises used: ENNReal.toNNReal_eq_toNNReal_iff, MeasureTheory.measure_ne_top, congr_fun