awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε_1 : ℝ≥0∞
hε : 0 < ε_1
f : ℕ → Set α
f_disj : Pairwise (Function.onFun Disjoint f)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ),
    (fun (s : Set α) (hs : MeasurableSet s) ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
      (f i) ⋯
ε : ℝ≥0∞
εpos : 0 < ε
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε / 2
t : (i : ℕ) → Set α
tC : ∀ (i : ℕ), t i ∈ C
ht : ∀ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t i ∆ f i) < δ i
this : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i)) atTop (𝓝 0)
n : ℕ
hn : (μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i) < ε / 2
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (∑' (i : ℕ), δ i : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i) : ℝ≥0∞) <
    ε / 2 + ε / 2

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε_1 : ℝ≥0∞
hε : 0 < ε_1
f : ℕ → Set α
f_disj : Pairwise (Function.onFun Disjoint f)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ),
    (fun (s : Set α) (hs : MeasurableSet s) ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
      (f i) ⋯
ε : ℝ≥0∞
εpos : 0 < ε
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε / 2
t : (i : ℕ) → Set α
tC : ∀ (i : ℕ), t i ∈ C
ht : ∀ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t i ∆ f i) < δ i
this : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i)) atTop (𝓝 0)
n : ℕ
hn : (μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i) < ε / 2
⊢ ε / 2 + ε / 2 = ε

Tactic:
ENNReal.add_halves ε

Premises used: ENNReal.add_halves
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε_1 : ℝ≥0∞
hε : 0 < ε_1
f : ℕ → Set α
f_disj : Pairwise (Function.onFun Disjoint f)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ),
    (fun (s : Set α) (hs : MeasurableSet s) ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
      (f i) ⋯
ε : ℝ≥0∞
εpos : 0 < ε
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε / 2
t : (i : ℕ) → Set α
tC : ∀ (i : ℕ), t i ∈ C
ht : ∀ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t i ∆ f i) < δ i
this : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i)) atTop (𝓝 0)
n : ℕ
hn : (μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i) < ε / 2
calc :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⋃ i ∈ Finset.range n, t i) ∆ ⋃ (i : ℕ), f i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((⋃ i ∈ Finset.range n, t i ∆ f i) ∪ ⋃ i ∈ Ici n, f i) : ℝ≥0∞)
calc₁ :
  (μ : (a : Set α) → ℝ≥0∞) ((⋃ i ∈ Finset.range n, t i ∆ f i) ∪ ⋃ i ∈ Ici n, f i) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (∑ i ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (t i ∆ f i) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i) : ℝ≥0∞)
calc₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (∑ i ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (t i ∆ f i) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (∑ i ∈ Finset.range n, δ i : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i) : ℝ≥0∞)
calc₃ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (∑ i ∈ Finset.range n, δ i : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (∑' (i : ℕ), δ i : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i) : ℝ≥0∞)
calc₄ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (∑' (i : ℕ), δ i : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i) : ℝ≥0∞) <
    ε / 2 + ε / 2
⊢ (μ : (a : Set α) → ℝ≥0∞) ((⋃ i ∈ Finset.range n, t i) ∆ ⋃ (i : ℕ), f i) < ε

Tactic:
calc μ ((⋃ i ∈ Finset.range n, t i) ∆ (⋃ i, f i))
    _ ≤ μ ((⋃ i ∈ Finset.range n, (t i) ∆ (f i)) ∪ ⋃ i ∈ Ici n, f i) := by
      gcongr
      intro x hx
      simp only [Finset.mem_range, mem_symmDiff, mem_iUnion, exists_prop, not_exists, not_and,
        mem_Ici, mem_union] at hx ⊢
      grind
    _ ≤ ∑ i ∈ Finset.range n, μ (t i ∆ f i) + μ (⋃ i ∈ Ici n, f i) := by
      apply (measure_union_le _ _).trans
      gcongr
      apply measure_biUnion_finset_le
    _ ≤ ∑ i ∈ Finset.range n, δ i + μ (⋃ i ∈ Ici n, f i) := by
      gcongr with i; exact (ht i).le
    _ ≤ ∑' i, δ i + μ (⋃ i ∈ Ici n, f i) := by
      gcongr; exact ENNReal.sum_le_tsum (Finset.range n)
    _ < ε / 2 + ε / 2 := by gcongr
    _ = ε := ENNReal.add_halves ε

Premises used: Finset.range, ENNReal.add_halves, Union.union, DFunLike.coe, Set.iUnion, symmDiff
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
apply :
  ∃ (D : Set (Set α)),
    D.Countable ∧
      D ⊆ (supClosure : (a : Set (Set α)) → Set (Set α)) C ∧
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
apply₁ : mα = generateFrom ((supClosure : (a : Set (Set α)) → Set (Set α)) C)
⊢ ∃ (t : Set α),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) t ∧
      (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε

Tactic:
apply exists_measure_symmDiff_lt_of_generateFrom_isSetRing hC.isSetRing_supClosure ?_ ?_ hs hε

Premises used: MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetRing, MeasureTheory.IsSetSemiring.isSetRing_supClosure
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
rcases :
  ∀ (D : Set (Set α)) (D_count : D.Countable) (DC : D ⊆ C)
    (hD : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∃ (D : Set (Set α)),
      D.Countable ∧
        D ⊆ (supClosure : (a : Set (Set α)) → Set (Set α)) C ∧
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (D : Set (Set α)),
    D.Countable ∧
      D ⊆ (supClosure : (a : Set (Set α)) → Set (Set α)) C ∧
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rcases h'C with ⟨D, D_count, DC, hD⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
D : Set (Set α)
D_count : D.Countable
DC : D ⊆ C
hD : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (D : Set (Set α)),
    D.Countable ∧
      D ⊆ (supClosure : (a : Set (Set α)) → Set (Set α)) C ∧
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
⟨D, D_count, DC.trans subset_supClosure, hD⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro, subset_supClosure
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
D : Set (Set α)
D_count : D.Countable
DC : D ⊆ C
hD : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (D : Set (Set α)),
    D.Countable ∧
      D ⊆ (supClosure : (a : Set (Set α)) → Set (Set α)) C ∧
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact ⟨D, D_count, DC.trans subset_supClosure, hD⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
rw : generateFrom C = generateFrom ((supClosure : (a : Set (Set α)) → Set (Set α)) C)
⊢ mα = generateFrom ((supClosure : (a : Set (Set α)) → Set (Set α)) C)

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
apply : generateFrom ((supClosure : (a : Set (Set α)) → Set (Set α)) C) ≤ generateFrom C
⊢ generateFrom C = generateFrom ((supClosure : (a : Set (Set α)) → Set (Set α)) C)

Tactic:
apply le_antisymm (generateFrom_mono subset_supClosure)

Premises used: MeasurableSpace.generateFrom_mono, le_antisymm, subset_supClosure
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
apply :
  ∀ (t : Set α)
    (ht : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) t),
    MeasurableSet t
⊢ generateFrom ((supClosure : (a : Set (Set α)) → Set (Set α)) C) ≤ generateFrom C

Tactic:
apply generateFrom_le (fun t ht ↦ ?_)

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
t : Set α
ht : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) t
⊢ MeasurableSet t

Tactic:
apply measurableSet_generateFrom_of_mem_supClosure ht

Premises used: measurableSet_generateFrom_of_mem_supClosure
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
rw : ∀ (x : MeasuredSets μ), ∀ r > 0, (Metric.eball x r ∩ SetLike.coe ⁻¹' C).Nonempty
⊢ Dense (X := MeasuredSets μ) (SetLike.coe ⁻¹' C)

Tactic:
rw [EMetric.dense_iff]

Premises used: EMetric.dense_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
rcases :
  ∀ (t : Set α) (tC : t ∈ C) (ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε),
    (Metric.eball s ε ∩ SetLike.coe ⁻¹' C).Nonempty
⊢ (Metric.eball s ε ∩ SetLike.coe ⁻¹' C).Nonempty

Tactic:
rcases exists_measure_symmDiff_lt_of_generateFrom_isSetRing hC h'C h s.2 εpos with ⟨t, tC, ht⟩

Premises used: MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetRing, Subtype.property
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε
rw : MeasurableSet t
⊢ MeasurableSet t

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε
⊢ MeasurableSet t

Tactic:
measurableSet_generateFrom tC

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε
⊢ MeasurableSet t

Tactic:
exact measurableSet_generateFrom tC

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε
⊢ MeasurableSet t

Tactic:
have t_meas : MeasurableSet t := by rw [h]; exact measurableSet_generateFrom tC
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε
t_meas : MeasurableSet t
⊢ (Metric.eball s ε ∩ SetLike.coe ⁻¹' C).Nonempty

Tactic:
⟨⟨t, t_meas⟩, ?_, tC⟩

Premises used: Subtype.mk, Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε
t_meas : MeasurableSet t
refine : Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) t t_meas ∈ Metric.eball s ε
⊢ (Metric.eball s ε ∩ SetLike.coe ⁻¹' C).Nonempty

Tactic:
refine ⟨⟨t, t_meas⟩, ?_, tC⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε
t_meas : MeasurableSet t
⊢ Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) t t_meas ∈ Metric.eball s ε

Tactic:
simpa [MeasuredSets.edist_def] using ht

Premises used: MeasureTheory.MeasuredSets.edist_def
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
rw :
  ∀ (x : MeasuredSets μ),
    ∀ r > 0, (Metric.eball x r ∩ SetLike.coe ⁻¹' (supClosure : (a : Set (Set α)) → Set (Set α)) C).Nonempty
⊢ Dense (X := MeasuredSets μ) (SetLike.coe ⁻¹' (supClosure : (a : Set (Set α)) → Set (Set α)) C)

Tactic:
rw [EMetric.dense_iff]

Premises used: EMetric.dense_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
rcases :
  ∀ (t : Set α)
    (tC : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) t)
    (ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε),
    (Metric.eball s ε ∩ SetLike.coe ⁻¹' (supClosure : (a : Set (Set α)) → Set (Set α)) C).Nonempty
⊢ (Metric.eball s ε ∩ SetLike.coe ⁻¹' (supClosure : (a : Set (Set α)) → Set (Set α)) C).Nonempty

Tactic:
rcases exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring hC h'C h s.2 εpos
    with ⟨t, tC, ht⟩

Premises used: MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring, Subtype.property
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
t : Set α
tC : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) t
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε
⊢ Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) t ⋯ ∈ Metric.eball s ε

Tactic:
simpa [MeasuredSets.edist_def] using ht

Premises used: MeasureTheory.MeasuredSets.edist_def
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
t : Set α
tC : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) t
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε
refine : MeasurableSet t
⊢ (Metric.eball s ε ∩ SetLike.coe ⁻¹' (supClosure : (a : Set (Set α)) → Set (Set α)) C).Nonempty

Tactic:
refine ⟨⟨t, ?_⟩, by simpa [MeasuredSets.edist_def] using ht, tC⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
t : Set α
tC : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) t
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε
rw : MeasurableSet t
⊢ MeasurableSet t

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
t : Set α
tC : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) t
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε
⊢ MeasurableSet t

Tactic:
measurableSet_generateFrom_of_mem_supClosure tC

Premises used: measurableSet_generateFrom_of_mem_supClosure
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
t : Set α
tC : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) t
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε
⊢ MeasurableSet t

Tactic:
exact measurableSet_generateFrom_of_mem_supClosure tC

Premises used: measurableSet_generateFrom_of_mem_supClosure
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ht : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
hst : univ ⊆ s ∪ t
right : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (toMeasurable μ s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ ⟂ₘ ν

Tactic:
use toMeasurable μ s, measurableSet_toMeasurable _ _, (measure_toMeasurable _).trans hs

Premises used: MeasureTheory.measure_toMeasurable, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.toMeasurable, Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ht : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
hst : univ ⊆ s ∪ t
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (toMeasurable μ s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_mono_null (fun x hx => (hst trivial).resolve_left fun hxs => hx ?_) ht

Premises used: trivial, Or.resolve_left, MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ht : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
hst : univ ⊆ s ∪ t
right : ∀ (x : α) (hx : x ∈ (toMeasurable μ s)ᶜ) (hxs : x ∈ s), x ∈ toMeasurable μ s
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (toMeasurable μ s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine measure_mono_null (fun x hx => (hst trivial).resolve_left fun hxs => hx ?_) ht
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ht : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
hst : univ ⊆ s ∪ t
x : α
hx : x ∈ (toMeasurable μ s)ᶜ
hxs : x ∈ s
⊢ x ∈ toMeasurable μ s

Tactic:
subset_toMeasurable _ _ hxs

Premises used: MeasureTheory.subset_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ht : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
hst : univ ⊆ s ∪ t
x : α
hx : x ∈ (toMeasurable μ s)ᶜ
hxs : x ∈ s
⊢ x ∈ toMeasurable μ s

Tactic:
exact subset_toMeasurable _ _ hxs

Premises used: MeasureTheory.subset_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ MeasurableSet h.nullSet

Tactic:
h.choose_spec.1

Premises used: Exists.choose_spec, MeasureTheory.Measure.MutuallySingular.nullSet, And.left
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) h.nullSet : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
h.choose_spec.2.1

Premises used: Exists.choose_spec, MeasureTheory.Measure.MutuallySingular.nullSet, And.right, And.left