awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
⊢ u ∩ s ∈ 𝓝[s] x

Tactic:
have : u ∩ s ∈ 𝓝[s] x := by rw [inter_comm]; exact inter_mem_nhdsWithin s u_mem
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
this : u ∩ s ∈ 𝓝[s] x
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)

Tactic:
hx.2 _ this

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
this : u ∩ s ∈ 𝓝[s] x
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)

Tactic:
exact hx.2 _ this

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)

Tactic:
have A : 0 < μ (u ∩ s) := by
    have : u ∩ s ∈ 𝓝[s] x := by rw [inter_comm]; exact inter_mem_nhdsWithin s u_mem
    exact hx.2 _ this
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
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∞)
⊢ u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s

Tactic:
have B : (u ∩ μ.everywherePosSubset s : Set α) =ᵐ[μ] (u ∩ s : Set α) :=
    ae_eq_set_inter (ae_eq_refl _) (everywherePosSubset_ae_eq hs)
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
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∞) (u ∩ μ.everywherePosSubset s) : ℝ≥0∞)

Tactic:
rw [← B.measure_eq] at A

Premises used: Filter.EventuallyEq.measure_eq
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
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
A₁ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ μ.everywherePosSubset s) : ℝ≥0∞)
⊢ u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s

Tactic:
rw [← B.measure_eq] at A

Premises used: Filter.EventuallyEq.measure_eq
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
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 ∩ μ.everywherePosSubset s) : ℝ≥0∞)
B : u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)

Tactic:
A.trans_le (measure_mono hu)

Premises used: LT.lt.trans_le, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
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 ∩ μ.everywherePosSubset s) : ℝ≥0∞)
B : u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)

Tactic:
exact A.trans_le (measure_mono hu)

Premises used: LT.lt.trans_le, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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
rcases :
  ∀ (u : Set α) (u_mem : u ∈ 𝓝 x) (hu : u ∩ μ.everywherePosSubset s ⊆ n),
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)

Tactic:
rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 hn with ⟨u, u_mem, hu⟩

Premises used: Iff.mp, mem_nhdsWithin_iff_exists_mem_nhds_inter
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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
rw : s ∩ u ∈ 𝓝[s] x
⊢ u ∩ s ∈ 𝓝[s] x

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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
⊢ s ∩ u ∈ 𝓝[s] x

Tactic:
inter_mem_nhdsWithin s u_mem

Premises used: inter_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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
⊢ s ∩ u ∈ 𝓝[s] x

Tactic:
exact inter_mem_nhdsWithin s u_mem

Premises used: inter_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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
⊢ u ∩ s ∈ 𝓝[s] x

Tactic:
have : u ∩ s ∈ 𝓝[s] x := by rw [inter_comm]; exact inter_mem_nhdsWithin s u_mem
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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
this : u ∩ s ∈ 𝓝[s] x
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)

Tactic:
hx.2 _ this

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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
this : u ∩ s ∈ 𝓝[s] x
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)

Tactic:
exact hx.2 _ this

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)

Tactic:
have A : 0 < μ (u ∩ s) := by
    have : u ∩ s ∈ 𝓝[s] x := by rw [inter_comm]; exact inter_mem_nhdsWithin s u_mem
    exact hx.2 _ this
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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∞)
⊢ u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s

Tactic:
have B : (u ∩ μ.everywherePosSubset s : Set α) =ᵐ[μ] (u ∩ s : Set α) :=
    ae_eq_set_inter (ae_eq_refl _) (everywherePosSubset_ae_eq_of_measure_ne_top hs h's)
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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∞) (u ∩ μ.everywherePosSubset s) : ℝ≥0∞)

Tactic:
rw [← B.measure_eq] at A

Premises used: Filter.EventuallyEq.measure_eq
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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
A₁ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ μ.everywherePosSubset s) : ℝ≥0∞)
⊢ u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s

Tactic:
rw [← B.measure_eq] at A

Premises used: Filter.EventuallyEq.measure_eq
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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 ∩ μ.everywherePosSubset s) : ℝ≥0∞)
B : u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)

Tactic:
A.trans_le (measure_mono hu)

Premises used: LT.lt.trans_le, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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 ∩ μ.everywherePosSubset s) : ℝ≥0∞)
B : u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)

Tactic:
exact A.trans_le (measure_mono hu)

Premises used: LT.lt.trans_le, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
hs : μ.IsEverywherePos s
c : ℝ≥0∞
hc : c ≠ 0
x : α
hx : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)

Tactic:
simpa [hc.bot_lt, hs x hx n hn] using hc.bot_lt

Premises used: Ne.bot_lt
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
hs : μ.IsEverywherePos s
c : ℝ≥0
hc : c ≠ 0
⊢ (↑c : ℝ≥0∞) ≠ 0

Tactic:
simpa using hc
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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
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∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)

Tactic:
rcases h x hx with ⟨t, t_mem, ht⟩
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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∞)
grw : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (n ∩ t) : ℝ≥0∞)
grw₁ : Set α
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)

Tactic:
grw [← inter_subset_left (s := n)]

Premises used: Set.inter_subset_left
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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 ∩ t) : ℝ≥0∞)

Tactic:
hs x hx _ (inter_mem hn (mem_nhdsWithin_of_mem_nhds t_mem))

Premises used: Filter.inter_mem, mem_nhdsWithin_of_mem_nhds
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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 ∩ t) : ℝ≥0∞)

Tactic:
exact hs x hx _ (inter_mem hn (mem_nhdsWithin_of_mem_nhds t_mem))

Premises used: Filter.inter_mem, mem_nhdsWithin_of_mem_nhds
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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

Tactic:
⟨fun H ↦ H.of_forall_exists_nhds_eq ?_, fun H ↦ H.of_forall_exists_nhds_eq h⟩

Premises used: Iff.intro, MeasureTheory.Measure.IsEverywherePos.of_forall_exists_nhds_eq
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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∞)
refine :
  ∀ (H : ν.IsEverywherePos s),
    ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
⊢ ν.IsEverywherePos s ↔ μ.IsEverywherePos s

Tactic:
refine ⟨fun H ↦ H.of_forall_exists_nhds_eq ?_, fun H ↦ H.of_forall_exists_nhds_eq h⟩
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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
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∞)
⊢ ∃ 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⟩
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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 : 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:
⟨t, ht, fun u hu ↦ (h't u hu).symm⟩

Premises used: And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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 : 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:
exact ⟨t, ht, fun u hu ↦ (h't u hu).symm⟩
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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
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∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)

Tactic:
rcases mem_nhdsWithin.1 hn with ⟨u, u_open, xu, hu⟩

Premises used: mem_nhdsWithin, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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
apply : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)

Tactic:
apply lt_of_lt_of_le _ (measure_mono hu)

Premises used: MeasureTheory.measure_mono, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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∞) (u ∩ s) : ℝ≥0∞)

Tactic:
(u_open.inter hs).measure_pos μ ⟨x, ⟨xu, xs⟩⟩

Premises used: IsOpen.measure_pos, And.intro, IsOpen.inter, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
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∞) (u ∩ s) : ℝ≥0∞)

Tactic:
exact (u_open.inter hs).measure_pos μ ⟨x, ⟨xu, xs⟩⟩

Premises used: IsOpen.measure_pos, And.intro, IsOpen.inter, 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
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst_1] k
⊢ ∃ (u : ℕ → ℝ≥0∞), StrictAnti u ∧ (∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)) ∧ Tendsto u atTop (𝓝 0)

Tactic:
exists_seq_strictAnti_tendsto' (zero_lt_one : (0 : ℝ≥0∞) < 1)

Premises used: exists_seq_strictAnti_tendsto', zero_lt_one
-- 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
obtain :
  ∀ (u : ℕ → ℝ≥0∞) (u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)) (u_lim : Tendsto u atTop (𝓝 0)),
    IsGδ k
⊢ 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)

Premises used: exists_seq_strictAnti_tendsto', zero_lt_one