awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
this : IsFiniteMeasure ν
t : Set α
htm : MeasurableSet t
iht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
compl :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    (ν : (a : Set α) → ℝ≥0∞) tᶜ
compl₁ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
compl₂ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
compl₃ compl₄ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)

Tactic:
rw [measure_compl (h t htm) (by finiteness), measure_compl (h t htm) (by finiteness), iht,
      h_univ]

Premises used: MeasureTheory.measure_compl
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
this : IsFiniteMeasure ν
f : ℕ → Set α
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)

Tactic:
simp [measure_iUnion, hfd, h _ (hfm _), ihf]

Premises used: MeasureTheory.measure_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
empty : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞)
basic :
  ∀ (t : Set α) (ht : t ∈ C), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
compl :
  ∀ (t : Set α) (htm : MeasurableSet t)
    (iht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)
iUnion :
  ∀ (f : ℕ → Set α) (hfd : Pairwise (Disjoint on f)) (hfm : ∀ (i : ℕ), MeasurableSet (f i))
    (ihf : ∀ (i : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
induction s, hs using induction_on_inter hA hC with
  | empty => simp
  | basic t ht => exact hμν t ht
  | compl t htm iht =>
    rw [measure_compl (h t htm) (by finiteness), measure_compl (h t htm) (by finiteness), iht,
      h_univ]
  | iUnion f hfd hfm ihf =>
    simp [measure_iUnion, hfd, h _ (hfm _), ihf]

Premises used: Compl.compl, MeasureTheory.measure_iUnion, Set.iUnion
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
C : Set (Set α)
hA : m0 = generateFrom C
hC : IsPiSystem C
inst : IsFiniteMeasure μ
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ μ = ν

Tactic:
Measure.ext fun _s hs =>
    ext_on_measurableSpace_of_generate_finite m0 C hμν le_rfl hA hC h_univ hs

Premises used: le_rfl, MeasureTheory.ext_on_measurableSpace_of_generate_finite, MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : Filter α
h : f ≤ g
⊢ μ.FiniteAtFilter g → μ.FiniteAtFilter f

Tactic:
fun ⟨s, hs, hμ⟩ =>
  ⟨s, h hs, hμ⟩

Premises used: MeasureTheory.Measure.FiniteAtFilter, _private.0.MeasureTheory.Measure.FiniteAtFilter.filter_mono.match_1, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : Filter α
h : μ.FiniteAtFilter f
⊢ μ.FiniteAtFilter (f ⊓ g)

Tactic:
h.filter_mono inf_le_left

Premises used: MeasureTheory.Measure.FiniteAtFilter.filter_mono, inf_le_left
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : Filter α
h : μ.FiniteAtFilter g
⊢ μ.FiniteAtFilter (f ⊓ g)

Tactic:
h.filter_mono inf_le_right

Premises used: inf_le_right, MeasureTheory.Measure.FiniteAtFilter.filter_mono
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : Filter α
⊢ μ.FiniteAtFilter (f ⊓ ae μ) ↔ μ.FiniteAtFilter f

Tactic:
⟨?_, fun h => h.filter_mono inf_le_left⟩

Premises used: MeasureTheory.Measure.FiniteAtFilter.filter_mono, Iff.intro, inf_le_left
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : Filter α
refine : μ.FiniteAtFilter (f ⊓ ae μ) → μ.FiniteAtFilter f
⊢ μ.FiniteAtFilter (f ⊓ ae μ) ↔ μ.FiniteAtFilter f

Tactic:
refine ⟨?_, fun h => h.filter_mono inf_le_left⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : Filter α
t : Set α
ht : t ∈ f
u : Set α
hu : u ∈ ae μ
hμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) (∞ : ℝ≥0∞)
suffices : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
⊢ μ.FiniteAtFilter f

Tactic:
suffices μ t ≤ μ (t ∩ u) from ⟨t, ht, this.trans_lt hμ⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : Filter α
t : Set α
ht : t ∈ f
u : Set α
hu : u ∈ ae μ
hμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)

Tactic:
measure_mono_ae (mem_of_superset hu fun x hu ht => ⟨ht, hu⟩)

Premises used: MeasureTheory.measure_mono_ae, And.intro, Filter.mem_of_superset
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : Filter α
t : Set α
ht : t ∈ f
u : Set α
hu : u ∈ ae μ
hμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)

Tactic:
exact measure_mono_ae (mem_of_superset hu fun x hu ht => ⟨ht, hu⟩)

Premises used: MeasureTheory.measure_mono_ae, Filter.mem_of_superset
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : Filter α
h : f ⊓ ae μ ≤ g
hg : μ.FiniteAtFilter g
⊢ μ.FiniteAtFilter f

Tactic:
inf_ae_iff.1 (hg.filter_mono h)

Premises used: MeasureTheory.Measure.FiniteAtFilter.filter_mono, MeasureTheory.Measure.FiniteAtFilter.inf_ae_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : Filter α
h : μ ≤ ν
⊢ ν.FiniteAtFilter f → μ.FiniteAtFilter f

Tactic:
fun ⟨s, hs, hν⟩ => ⟨s, hs, (Measure.le_iff'.1 h s).trans_lt hν⟩

Premises used: MeasureTheory.Measure.le_iff', MeasureTheory.Measure.FiniteAtFilter, _private.0.MeasureTheory.Measure.FiniteAtFilter.filter_mono.match_1, And.intro, Exists.intro, Iff.mp, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f g : Filter α
hf : f ≤ g
hμ : μ ≤ ν
⊢ ν.FiniteAtFilter g → μ.FiniteAtFilter f

Tactic:
fun h => (h.filter_mono hf).measure_mono hμ

Premises used: MeasureTheory.Measure.FiniteAtFilter.filter_mono, MeasureTheory.Measure.FiniteAtFilter.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : Filter α
h : μ.FiniteAtFilter f
⊢ ∀ᶠ (s : Set α) in f.smallSets, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(eventually_smallSets' fun _s _t hst ht => (measure_mono hst).trans_lt ht).2 h

Premises used: Iff.mpr, MeasureTheory.measure_mono, Filter.eventually_smallSets', LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : Filter α
⊢ μ.FiniteAtFilter f → μ.FiniteAtFilter g → μ.FiniteAtFilter (f ⊔ g)

Tactic:
fun ⟨s, hsf, hsμ⟩ ⟨t, htg, htμ⟩ =>
  ⟨s ∪ t, union_mem_sup hsf htg, (measure_union_le s t).trans_lt (ENNReal.add_lt_top.2 ⟨hsμ, htμ⟩)⟩

Premises used: Iff.mpr, MeasureTheory.Measure.FiniteAtFilter, _private.0.MeasureTheory.Measure.FiniteAtFilter.filter_mono.match_1, Max.max, Filter.union_mem_sup, And.intro, Exists.intro, Union.union, ENNReal.add_lt_top, LE.le.trans_lt, MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
_m0 : MeasurableSpace α
μ : Measure α
inst_1 : IsLocallyFiniteMeasure μ
x : α
s : Set α
⊢ μ.FiniteAtFilter (𝓝[s] x)

Tactic:
(finiteAt_nhds μ x).inf_of_left

Premises used: MeasureTheory.Measure.finiteAt_nhds, MeasureTheory.Measure.FiniteAtFilter.inf_of_left, nhdsWithin
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ.FiniteAtFilter (𝓟 s) ↔ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
⟨fun ⟨_t, ht, hμ⟩ => (measure_mono ht).trans_lt hμ, fun h => ⟨s, mem_principal_self s, h⟩⟩

Premises used: Filter.mem_principal_self, And.intro, LT.lt, Iff.intro, MeasureTheory.measure_mono, Exists.intro, _private.0.MeasureTheory.Measure.finiteAt_principal.match_1, Top.top, LE.le.trans_lt, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
_m : MeasurableSpace α
μ ν : Measure α
H : IsLocallyFiniteMeasure μ
h : ν ≤ μ
⊢ IsLocallyFiniteMeasure ν

Tactic:
let F := H.finiteAtNhds
  ⟨fun x => (F x).measure_mono h⟩

Premises used: MeasureTheory.IsLocallyFiniteMeasure.finiteAtNhds, MeasureTheory.IsLocallyFiniteMeasure.mk, MeasureTheory.Measure.FiniteAtFilter.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∃ U ⊇ s, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
IsCompact.induction_on h ?_ ?_ ?_ ?_

Premises used: IsCompact.induction_on
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
refine_1 : ∃ U ⊇ ∅, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 :
  ∀ ⦃s t : Set α⦄,
    s ⊆ t →
      (∃ U ⊇ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)) →
        ∃ U ⊇ s, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_3 :
  ∀ ⦃s t : Set α⦄,
    (∃ U ⊇ s, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)) →
      (∃ U ⊇ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)) →
        ∃ U ⊇ s ∪ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_4 :
  ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ U ⊇ s, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine IsCompact.induction_on h ?_ ?_ ?_ ?_
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
h₁ : Superset.{u_1} (α := Set α) ∅ ∅ ∧ IsOpen[inst] ∅ ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ U ⊇ ∅, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
use ∅
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ Superset.{u_1} (α := Set α) ∅ ∅ ∧ IsOpen[inst] ∅ ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [Superset]

Premises used: Superset
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s_1 : Set α
h : IsCompact s_1
hμ : ∀ x ∈ s_1, μ.FiniteAtFilter (𝓝 x)
s t : Set α
hst : s ⊆ t
U : Set α
htU : U ⊇ t
hUo : IsOpen[inst] U
hU : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ U ⊇ s, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
⟨U, hst.trans htU, hUo, hU⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s_1 : Set α
h : IsCompact s_1
hμ : ∀ x ∈ s_1, μ.FiniteAtFilter (𝓝 x)
s t : Set α
hst : s ⊆ t
U : Set α
htU : U ⊇ t
hUo : IsOpen[inst] U
hU : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ U ⊇ s, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ⟨U, hst.trans htU, hUo, hU⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s_1 : Set α
h : IsCompact s_1
hμ : ∀ x ∈ s_1, μ.FiniteAtFilter (𝓝 x)
s t U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst] U
hU : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set α
htV : V ⊇ t
hVo : IsOpen[inst] V
hV : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ U ⊇ s ∪ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
⟨U ∪ V, union_subset_union hsU htV, hUo.union hVo,
        (measure_union_le _ _).trans_lt <| ENNReal.add_lt_top.2 ⟨hU, hV⟩⟩

Premises used: Iff.mpr, Set.union_subset_union, IsOpen.union, And.intro, Exists.intro, Union.union, ENNReal.add_lt_top, LE.le.trans_lt, MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s_1 : Set α
h : IsCompact s_1
hμ : ∀ x ∈ s_1, μ.FiniteAtFilter (𝓝 x)
s t U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst] U
hU : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set α
htV : V ⊇ t
hVo : IsOpen[inst] V
hV : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ U ⊇ s ∪ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine
      ⟨U ∪ V, union_subset_union hsU htV, hUo.union hVo,
        (measure_union_le _ _).trans_lt <| ENNReal.add_lt_top.2 ⟨hU, hV⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
x : α
hx : x ∈ s
refine_4 :
  ∀ (U : Set α) (hU : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)) (hx : x ∈ U)
    (hUo : IsOpen[inst] U),
    ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rcases (hμ x hx).exists_mem_basis (nhds_basis_opens _) with ⟨U, ⟨hx, hUo⟩, hU⟩

Premises used: nhds_basis_opens, MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
x : α
hx_1 : x ∈ s
U : Set α
hU : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hx : x ∈ U
hUo : IsOpen[inst] U
⊢ ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
⟨U, nhdsWithin_le_nhds (hUo.mem_nhds hx), U, Subset.rfl, hUo, hU⟩

Premises used: nhdsWithin_le_nhds, Set.Subset.rfl, And.intro, IsOpen.mem_nhds, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
x : α
hx_1 : x ∈ s
U : Set α
hU : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hx : x ∈ U
hUo : IsOpen[inst] U
⊢ ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ⟨U, nhdsWithin_le_nhds (hUo.mem_nhds hx), U, Subset.rfl, hUo, hU⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
h : IsCompact s
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
⊢ ∃ U ⊇ s, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
h.exists_open_superset_measure_lt_top' fun x _ => μ.finiteAt_nhds x

Premises used: MeasureTheory.Measure.finiteAt_nhds, IsCompact.exists_open_superset_measure_lt_top'
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝[s] x)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsCompact s
⊢ (∀ a ∈ s, ∃ t ∈ 𝓝[s] a, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa only [← compl_mem_ae_iff] using hs.compl_mem_sets_of_nhdsWithin

Premises used: IsCompact.compl_mem_sets_of_nhdsWithin, MeasureTheory.compl_mem_ae_iff
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
x : MeasurableSpace α
μ : Measure α
inst_1 : IsLocallyFiniteMeasure μ
⊢ IsFiniteMeasureOnCompacts μ

Tactic:
⟨fun _s hs => hs.measure_lt_top_of_nhdsWithin fun _ _ => μ.finiteAt_nhdsWithin _ _⟩

Premises used: MeasureTheory.IsFiniteMeasureOnCompacts.mk, MeasureTheory.Measure.finiteAt_nhdsWithin, IsCompact.measure_lt_top_of_nhdsWithin
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : CompactSpace α
mp : IsFiniteMeasure μ → IsFiniteMeasureOnCompacts μ
mpr : IsFiniteMeasureOnCompacts μ → IsFiniteMeasure μ
⊢ IsFiniteMeasure μ ↔ IsFiniteMeasureOnCompacts μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : CompactSpace α
h : IsFiniteMeasure μ
⊢ IsFiniteMeasureOnCompacts μ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : CompactSpace α
h : IsFiniteMeasureOnCompacts μ
⊢ IsFiniteMeasure μ

Tactic:
CompactSpace.isFiniteMeasure

Premises used: MeasureTheory.CompactSpace.isFiniteMeasure
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : CompactSpace α
h : IsFiniteMeasureOnCompacts μ
⊢ IsFiniteMeasure μ

Tactic:
exact CompactSpace.isFiniteMeasure

Premises used: MeasureTheory.CompactSpace.isFiniteMeasure
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
suffices : Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
⊢ μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K}

Tactic:
suffices H : Nonempty (μ.FiniteSpanningSetsIn { K | IsOpen K }) from H.some
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
inl : IsEmpty α → Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
inr : Nonempty α → Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
⊢ Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
h : IsEmpty α
x : ℕ
⊢ Membership.mem (γ := Set (Set α)) {K : Set α | IsOpen[inst] K} ∅

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
h : IsEmpty α
x : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
h : IsEmpty α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), ∅) univ

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
h : IsEmpty α
⊢ Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})

Tactic:
exact
      ⟨{  set := fun _ => ∅
          set_mem := fun _ => by simp
          finite := fun _ => by simp
          spanning := by simp [eq_iff_true_of_subsingleton] }⟩