awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Nonempty α
inr : ∀ (inhabited_h : Inhabited α), Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
⊢ Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})

Tactic:
inhabit α
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
⊢ ∃ (T : Set (Set α)), T.Countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S

Tactic:
isOpen_sUnion_countable S fun s hs => hs.1

Premises used: And.left, TopologicalSpace.isOpen_sUnion_countable
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
inr :
  ∀ (T : Set (Set α)) (T_count : T.Countable) (TS : T ⊆ S) (hT : ⋃₀ T = ⋃₀ S),
    Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
⊢ Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})

Tactic:
obtain ⟨T, T_count, TS, hT⟩ : ∃ T : Set (Set α), T.Countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S :=
    isOpen_sUnion_countable S fun s hs => hs.1

Premises used: And.left, TopologicalSpace.isOpen_sUnion_countable, Set
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = ⋃₀ S
⊢ ⋃₀ T = univ

Tactic:
rw [μ.isTopologicalBasis_isOpen_lt_top.sUnion_eq] at hT

Premises used: MeasureTheory.Measure.isTopologicalBasis_isOpen_lt_top, TopologicalSpace.IsTopologicalBasis.sUnion_eq
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
by_contra : ∀ (h'T : ¬T.Nonempty), False
⊢ T.Nonempty

Tactic:
by_contra h'T
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
h'T : ¬T.Nonempty
⊢ Eq.{u_1 + 1} (α := Set α) ∅ univ

Tactic:
rw [not_nonempty_iff_eq_empty.1 h'T, sUnion_empty] at hT

Premises used: Set.not_nonempty_iff_eq_empty, Iff.mp, Set.sUnion_empty
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
h'T : ¬T.Nonempty
hT₁ : Eq.{u_1 + 1} (α := Set α) ∅ univ
⊢ ¬T.Nonempty

Tactic:
rw [not_nonempty_iff_eq_empty.1 h'T, sUnion_empty] at hT

Premises used: Set.not_nonempty_iff_eq_empty, Iff.mp, Set.sUnion_empty
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : Eq.{u_1 + 1} (α := Set α) ∅ univ
h'T : ¬T.Nonempty
⊢ False

Tactic:
simpa only [← hT] using mem_univ (default : α)

Premises used: Inhabited.default, Set.mem_univ
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
⊢ T.Nonempty

Tactic:
have T_ne : T.Nonempty := by
    by_contra h'T
    rw [not_nonempty_iff_eq_empty.1 h'T, sUnion_empty] at hT
    simpa only [← hT] using mem_univ (default : α)
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
⊢ ∃ (f : ℕ → Set α), T = range f

Tactic:
T_count.exists_eq_range T_ne

Premises used: Set.Countable.exists_eq_range
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
inr : ∀ (f : ℕ → Set α) (hf : T = range f), Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
⊢ Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})

Tactic:
obtain ⟨f, hf⟩ : ∃ f : ℕ → Set α, T = range f := T_count.exists_eq_range T_ne

Premises used: Set.Countable.exists_eq_range
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
n : ℕ
a : f n ∈ T
⊢ f n ∈ S

Tactic:
apply TS
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
n : ℕ
a : f n ∈ range f
⊢ f n ∈ T

Tactic:
rw [hf]
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
n : ℕ
⊢ f n ∈ range f

Tactic:
mem_range_self n

Premises used: Set.mem_range_self
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
n : ℕ
⊢ f n ∈ range f

Tactic:
exact mem_range_self n

Premises used: Set.mem_range_self
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
⊢ ∀ (n : ℕ), f n ∈ S

Tactic:
have fS : ∀ n, f n ∈ S := by
    intro n
    apply TS
    rw [hf]
    exact mem_range_self n
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
⊢ Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})

Tactic:
⟨{  set := f
        set_mem := fun n => (fS n).1
        finite := fun n => (fS n).2
        spanning := ?_ }⟩

Premises used: MeasureTheory.Measure.FiniteSpanningSetsIn.mk, Nonempty.intro, And.right, And.left
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
inr : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) univ
⊢ Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})

Tactic:
refine
    ⟨{  set := f
        set_mem := fun n => (fS n).1
        finite := fun n => (fS n).2
        spanning := ?_ }⟩
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) univ

Tactic:
eq_univ_of_forall fun x => ?_

Premises used: Set.eq_univ_of_forall
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
inr : ∀ (x : α), Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) univ

Tactic:
refine eq_univ_of_forall fun x => ?_

Premises used: Set.eq_univ_of_forall
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
x : α
⊢ x ∈ ⋃₀ T

Tactic:
simp only [hT, mem_univ]

Premises used: Set.mem_univ
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
x : α
⊢ x ∈ ⋃₀ T

Tactic:
have : x ∈ ⋃₀ T := by simp only [hT, mem_univ]
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
x : α
this : x ∈ ⋃₀ T
⊢ ∃ t ∈ range f, x ∈ t

Tactic:
simpa only [mem_sUnion, exists_prop, ← hf]

Premises used: exists_prop, Set.mem_sUnion
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
x : α
inr : ∀ (t : Set α) (tT : t ∈ range f) (xt : x ∈ t), Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x

Tactic:
obtain ⟨t, tT, xt⟩ : ∃ t : Set α, t ∈ range f ∧ x ∈ t := by
    have : x ∈ ⋃₀ T := by simp only [hT, mem_univ]
    simpa only [mem_sUnion, exists_prop, ← hf]

Premises used: Set.range, Set
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
x : α
t : Set α
tT : t ∈ range f
xt : x ∈ t
⊢ ∃ (n : ℕ), f n = t

Tactic:
simpa only using tT
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
x : α
t : Set α
tT : t ∈ range f
xt : x ∈ t
inr : ∀ (n : ℕ) (tT : f n ∈ range f) (xt : x ∈ f n), Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x

Tactic:
obtain ⟨n, rfl⟩ : ∃ n : ℕ, f n = t := by simpa only using tT

Premises used: rfl
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
x : α
n : ℕ
tT : f n ∈ range f
xt : x ∈ f n
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x

Tactic:
mem_iUnion_of_mem _ xt

Premises used: Set.mem_iUnion_of_mem
-- 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 : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
x : α
n : ℕ
tT : f n ∈ range f
xt : x ∈ f n
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x

Tactic:
exact mem_iUnion_of_mem _ xt

Premises used: Set.mem_iUnion_of_mem
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : CompactIccSpace α
m : MeasurableSpace α
μ : Measure α
inst_3 : IsLocallyFiniteMeasure μ
a b : α
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Icc a b) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
isCompact_Icc.measure_lt_top

Premises used: CompactIccSpace.isCompact_Icc, IsCompact.measure_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : CompactIccSpace α
m : MeasurableSpace α
μ : Measure α
inst_3 : IsLocallyFiniteMeasure μ
a b : α
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ico a b) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_mono Ico_subset_Icc_self).trans_lt measure_Icc_lt_top

Premises used: Set.Ico_subset_Icc_self, measure_Icc_lt_top, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : CompactIccSpace α
m : MeasurableSpace α
μ : Measure α
inst_3 : IsLocallyFiniteMeasure μ
a b : α
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ioc a b) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_mono Ioc_subset_Icc_self).trans_lt measure_Icc_lt_top

Premises used: Set.Ioc_subset_Icc_self, measure_Icc_lt_top, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : CompactIccSpace α
m : MeasurableSpace α
μ : Measure α
inst_3 : IsLocallyFiniteMeasure μ
a b : α
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ioo a b) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_mono Ioo_subset_Icc_self).trans_lt measure_Icc_lt_top

Premises used: Set.Ioo_subset_Icc_self, measure_Icc_lt_top, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
s : Set α
hs : s.Subsingleton
μ : Measure α
inst : NoAtoms μ
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)

Tactic:
hs.induction_on (p := fun s => μ s = 0) measure_empty measure_singleton

Premises used: Set.Subsingleton.induction_on, MeasureTheory.measure_empty, MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
a : α
⊢ μ.restrict {a} = 0

Tactic:
simp only [measure_singleton, Measure.restrict_eq_zero]

Premises used: MeasureTheory.Measure.restrict_eq_zero, MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s_1 : Set α
inst : NoAtoms μ
s : Set α
⊢ NoAtoms (μ.restrict s)

Tactic:
⟨fun x => ?_⟩

Premises used: MeasureTheory.NoAtoms.mk
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s_1 : Set α
inst : NoAtoms μ
s : Set α
refine : ∀ (x : α), Eq (α := ENNReal) ((μ.restrict s : (a : Set α) → ENNReal) {x} : ENNReal) (0 : ENNReal)
⊢ NoAtoms (μ.restrict s)

Tactic:
refine ⟨fun x => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s_1 : Set α
inst : NoAtoms μ
s : Set α
x : α
obtain :
  ∀ (t : Set α) (hxt : {x} ⊆ t) (ht1 : MeasurableSet t)
    (ht2 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)),
    Eq (α := ENNReal) ((μ.restrict s : (a : Set α) → ENNReal) {x} : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ.restrict s : (a : Set α) → ENNReal) {x} : ENNReal) (0 : ENNReal)

Tactic:
obtain ⟨t, hxt, ht1, ht2⟩ := exists_measurable_superset_of_null (measure_singleton x : μ {x} = 0)

Premises used: MeasureTheory.NoAtoms.measure_singleton, MeasureTheory.exists_measurable_superset_of_null
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s_1 : Set α
inst : NoAtoms μ
s : Set α
x : α
t : Set α
hxt : {x} ⊆ t
ht1 : MeasurableSet t
ht2 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)
apply : Eq (α := ENNReal) ((μ.restrict s : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ.restrict s : (a : Set α) → ENNReal) {x} : ENNReal) (0 : ENNReal)

Tactic:
apply measure_mono_null hxt

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s_1 : Set α
inst : NoAtoms μ
s : Set α
x : α
t : Set α
hxt : {x} ⊆ t
ht1 : MeasurableSet t
ht2 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)
rw : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t ∩ s) : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ.restrict s : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)

Tactic:
rw [Measure.restrict_apply ht1]

Premises used: MeasureTheory.Measure.restrict_apply
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s_1 : Set α
inst : NoAtoms μ
s : Set α
x : α
t : Set α
hxt : {x} ⊆ t
ht1 : MeasurableSet t
ht2 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t ∩ s) : ENNReal) (0 : ENNReal)

Tactic:
apply measure_mono_null inter_subset_left ht2

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono_null