awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s t : Set X
t_mem : t ∈ 𝒜
ht : MeasurableSet t
⊢ MeasurableSet t ∧ ∀ (ε : ℝ), 0 < ε → ∃ t_1 ∈ 𝒜, μ.real (t ∆ t_1) < ε

Tactic:
exact ⟨hgen ▸ measurableSet_generateFrom t_mem, fun ε ε_pos ↦ ⟨t, t_mem, by simpa⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ε : ℝ
ε_pos : 0 < ε
⊢ μ.real (∅ ∆ ∅) < ε

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
⊢ MeasurableSet.{u_1} (α := X) ∅ ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (∅ ∆ t) < ε

Tactic:
exact ⟨MeasurableSet.empty, fun ε ε_pos ↦ ⟨∅, h𝒜.empty_mem, by simpa⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s t : Set X
ht_1 : MeasurableSet t
ht : MeasurableSet t ∧ ∀ (ε : ℝ), 0 < ε → ∃ t_1 ∈ 𝒜, μ.real (t ∆ t_1) < ε
⊢ MeasurableSet tᶜ ∧ ∀ (ε : ℝ), 0 < ε → ∃ t_1 ∈ 𝒜, μ.real (tᶜ ∆ t_1) < ε

Tactic:
⟨ht.1.compl, fun ε ε_pos ↦ ?_⟩

Premises used: MeasurableSet.compl, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s t : Set X
ht_1 : MeasurableSet t
ht : MeasurableSet t ∧ ∀ (ε : ℝ), 0 < ε → ∃ t_1 ∈ 𝒜, μ.real (t ∆ t_1) < ε
compl : ∀ (ε : ℝ) (ε_pos : 0 < ε), ∃ t_1 ∈ 𝒜, μ.real (tᶜ ∆ t_1) < ε
⊢ MeasurableSet tᶜ ∧ ∀ (ε : ℝ), 0 < ε → ∃ t_1 ∈ 𝒜, μ.real (tᶜ ∆ t_1) < ε

Tactic:
refine ⟨ht.1.compl, fun ε ε_pos ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s t : Set X
ht_1 : MeasurableSet t
ht : MeasurableSet t ∧ ∀ (ε : ℝ), 0 < ε → ∃ t_1 ∈ 𝒜, μ.real (t ∆ t_1) < ε
ε : ℝ
ε_pos : 0 < ε
compl : ∀ (u : Set X) (u_mem : u ∈ 𝒜) (hμtcu : μ.real (t ∆ u) < ε), ∃ t_1 ∈ 𝒜, μ.real (tᶜ ∆ t_1) < ε
⊢ ∃ t_1 ∈ 𝒜, μ.real (tᶜ ∆ t_1) < ε

Tactic:
obtain ⟨u, u_mem, hμtcu⟩ := ht.2 ε ε_pos

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s t : Set X
ht_1 : MeasurableSet t
ht : MeasurableSet t ∧ ∀ (ε : ℝ), 0 < ε → ∃ t_1 ∈ 𝒜, μ.real (t ∆ t_1) < ε
ε : ℝ
ε_pos : 0 < ε
u : Set X
u_mem : u ∈ 𝒜
hμtcu : μ.real (t ∆ u) < ε
rwa rwa₁ rwa₂ rwa₃ : μ.real (t ∆ u) < ε
⊢ μ.real (tᶜ ∆ uᶜ) < ε

Tactic:
rwa [compl_symmDiff_compl]

Premises used: compl_symmDiff_compl
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s t : Set X
ht_1 : MeasurableSet t
ht : MeasurableSet t ∧ ∀ (ε : ℝ), 0 < ε → ∃ t_1 ∈ 𝒜, μ.real (t ∆ t_1) < ε
ε : ℝ
ε_pos : 0 < ε
u : Set X
u_mem : u ∈ 𝒜
hμtcu : μ.real (t ∆ u) < ε
⊢ ∃ t_1 ∈ 𝒜, μ.real (tᶜ ∆ t_1) < ε

Tactic:
exact ⟨uᶜ, h𝒜.compl_mem u_mem, by rwa [compl_symmDiff_compl]⟩
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
⊢ MeasurableSet.{u_1} (α := X) (⋃ (i : ℕ), f i) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real ((⋃ (i : ℕ), f i) ∆ t) < ε

Tactic:
⟨MeasurableSet.iUnion (fun n ↦ (hf n).1), fun ε ε_pos ↦ ?_⟩

Premises used: And.left, And.intro, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
iUnion : ∀ (ε : ℝ) (ε_pos : 0 < ε), ∃ t ∈ 𝒜, μ.real ((⋃ (i : ℕ), f i) ∆ t) < ε
⊢ MeasurableSet.{u_1} (α := X) (⋃ (i : ℕ), f i) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real ((⋃ (i : ℕ), f i) ∆ t) < ε

Tactic:
refine ⟨MeasurableSet.iUnion (fun n ↦ (hf n).1), fun ε ε_pos ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
⊢ Filter.Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ ((μ : (a : Set X) → ℝ≥0∞) (accumulate f i) : ℝ≥0∞)) Filter.atTop
    (nhds ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)

Tactic:
have := tendsto_measure_iUnion_accumulate (μ := μ) (f := f)
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this :
  Filter.Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ ((μ : (a : Set X) → ℝ≥0∞) (accumulate f i) : ℝ≥0∞)) Filter.atTop
    (nhds ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
⊢ Filter.Tendsto (fun (n : ℕ) ↦ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n))) Filter.atTop
    (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))))

Tactic:
rw [← tendsto_toReal_iff (fun _ ↦ measure_ne_top _ _) (measure_ne_top _ _)] at this

Premises used: MeasureTheory.measure_ne_top, ENNReal.tendsto_toReal_iff
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n))) Filter.atTop
    (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))))
linarith : ε / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : ε / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ε / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₃ : ε / 2 ≤ 0 → 0 - ε + (1 * ε - HMul.hMul (α := ℝ) 2 0) = 0
⊢ ε / 2 > 0

Tactic:
linarith [ε_pos]
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n))) Filter.atTop
    (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))))
iUnion :
  ∀ (N : ℕ)
    (hN :
      ∀ n ≥ N,
        dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n)))
            (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))) <
          ε / 2),
    ∃ t ∈ 𝒜, μ.real ((⋃ (i : ℕ), f i) ∆ t) < ε
⊢ ∃ t ∈ 𝒜, μ.real ((⋃ (i : ℕ), f i) ∆ t) < ε

Tactic:
rcases Metric.tendsto_atTop.1 this (ε / 2) (by linarith [ε_pos]) with ⟨N, hN⟩

Premises used: Metric.tendsto_atTop, HDiv.hDiv, Iff.mp, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n))) Filter.atTop
    (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n)))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))) <
      ε / 2
n : ℕ
linarith :
  2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ≤ 0 →
    HMul.hMul (α := ℝ) 2 (-1) + 2 * HSub.hSub (α := ℝ) 0 (↑N : ℝ) + (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 - 0) = 0
linarith₁ linarith₂ : 2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < 2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n))) Filter.atTop
    (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n)))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))) <
      ε / 2
iUnion :
  ∀ (g : (n : ℕ) → Set X) (g_mem : ∀ (n : ℕ), g n ∈ 𝒜)
    (hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)),
    ∃ t ∈ 𝒜, μ.real ((⋃ (i : ℕ), f i) ∆ t) < ε
⊢ ∃ t ∈ 𝒜, μ.real ((⋃ (i : ℕ), f i) ∆ t) < ε

Tactic:
choose g g_mem hg using fun n ↦ (hf n).2 (ε / (2 * (N + 1))) (div_pos ε_pos (by linarith))

Premises used: HMul.hMul, HDiv.hDiv, Nat.cast, And.right, HAdd.hAdd, div_pos, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n))) Filter.atTop
    (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n)))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))) <
      ε / 2
g : (n : ℕ) → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)
⊢ ∃ t ∈ 𝒜, μ.real ((⋃ (i : ℕ), f i) ∆ t) < ε

Tactic:
⟨⋃ n ∈ Finset.range (N + 1), g n, h𝒜.biUnion_mem _ (fun i _ ↦ g_mem i), ?_⟩

Premises used: MeasureTheory.IsSetAlgebra.biUnion_mem, And.intro, Exists.intro, Set.iUnion
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n))) Filter.atTop
    (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n)))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))) <
      ε / 2
g : (n : ℕ) → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)
iUnion : μ.real ((⋃ (i : ℕ), f i) ∆ ⋃ n ∈ Finset.range (N + 1), g n) < ε
⊢ ∃ t ∈ 𝒜, μ.real ((⋃ (i : ℕ), f i) ∆ t) < ε

Tactic:
refine ⟨⋃ n ∈ Finset.range (N + 1), g n, h𝒜.biUnion_mem _ (fun i _ ↦ g_mem i), ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n))) Filter.atTop
    (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n)))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))) <
      ε / 2
g : (n : ℕ) → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)
⊢ μ.real ((⋃ (n : ℕ), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n) ≤
    ENNReal.toReal
      ((μ : (a : Set X) → ℝ≥0∞)
        (((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n) ∪
          (⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n))

Tactic:
toReal_mono (measure_ne_top _ _)
                  (measure_mono <| symmDiff_of_ge (iUnion_subset <|
                  fun i ↦ iUnion_subset (fun _ ↦ subset_iUnion f i)) ▸ symmDiff_triangle ..)

Premises used: Set.iUnion_subset, symmDiff_of_ge, MeasureTheory.Measure.real, MeasureTheory.measure_ne_top, Eq.rec, symmDiff_triangle, Set.subset_iUnion, MeasureTheory.measure_mono, ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n))) Filter.atTop
    (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n)))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))) <
      ε / 2
g : (n : ℕ) → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)
rw :
  ENNReal.toReal
      ((μ : (a : Set X) → ℝ≥0∞)
        (((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n) ∪
          (⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) ≤
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n) : ℝ≥0∞)).toReal
⊢ ENNReal.toReal
      ((μ : (a : Set X) → ℝ≥0∞)
        (((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n) ∪
          (⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) ≤
    ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n)) +
      ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n))

Tactic:
rw [← toReal_add (measure_ne_top _ _) (measure_ne_top _ _)]

Premises used: ENNReal.toReal_add, MeasureTheory.measure_ne_top
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n))) Filter.atTop
    (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n)))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))) <
      ε / 2
g : (n : ℕ) → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)
⊢ ENNReal.toReal
      ((μ : (a : Set X) → ℝ≥0∞)
        (((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n) ∪
          (⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) ≤
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n) : ℝ≥0∞)).toReal

Tactic:
toReal_mono (add_ne_top.2 ⟨measure_ne_top _ _, measure_ne_top _ _⟩) <|
                  measure_union_le _ _

Premises used: Iff.mpr, MeasureTheory.measure_ne_top, And.intro, ENNReal.add_ne_top, ENNReal.toReal_mono, MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n))) Filter.atTop
    (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n)))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))) <
      ε / 2
g : (n : ℕ) → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)
⊢ ENNReal.toReal
      ((μ : (a : Set X) → ℝ≥0∞)
        (((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n) ∪
          (⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) ≤
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n) : ℝ≥0∞)).toReal

Tactic:
exact toReal_mono (add_ne_top.2 ⟨measure_ne_top _ _, measure_ne_top _ _⟩) <|
                  measure_union_le _ _

Premises used: Iff.mpr, MeasureTheory.measure_ne_top, And.intro, ENNReal.add_ne_top, ENNReal.toReal_mono, MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n))) Filter.atTop
    (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n)))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))) <
      ε / 2
g : (n : ℕ) → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)
rw :
  ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n)) +
      ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) <
    ε / 2 + ε / 2
⊢ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n)) +
      ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) <
    ε

Tactic:
rw [← add_halves ε]

Premises used: add_halves
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n))) Filter.atTop
    (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n)))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))) <
      ε / 2
g : (n : ℕ) → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)
h₁ : ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n)) < ε / 2
h₂ :
  ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) <
    ε / 2
⊢ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n)) +
      ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) <
    ε / 2 + ε / 2

Tactic:
apply _root_.add_lt_add

Premises used: add_lt_add
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n))) Filter.atTop
    (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n)))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))) <
      ε / 2
g : (n : ℕ) → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)
h₁ :
  ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n)) -
      ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ n ∈ Finset.range (N + 1), f n)) <
    ε / 2
h₂ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ n ∈ Finset.range (N + 1), f n) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n) : ℝ≥0∞)
h₃ : Subset.{u_1} (α := Set X) (⋃ n ∈ Finset.range (N + 1), f n) (⋃ (n : ℕ), f n)
h₄ : NullMeasurableSet (⋃ n ∈ Finset.range (N + 1), f n) μ
⊢ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n)) < ε / 2

Tactic:
rw [measure_diff (h_fin := measure_ne_top _ _),
                    toReal_sub_of_le (ha := measure_ne_top _ _)]

Premises used: MeasureTheory.measure_ne_top, ENNReal.toReal_sub_of_le, MeasureTheory.measure_diff