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 : 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₁ :
  dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n)))
      (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ n ∈ Finset.range (N + 1), f n))) <
    ε / 2
⊢ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n)) -
      ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ n ∈ Finset.range (N + 1), f n)) <
    ε / 2

Tactic:
apply lt_of_le_of_lt (sub_le_dist ..)

Premises used: lt_of_le_of_lt, Real.sub_le_dist
-- 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₁ :
  dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n)))
      (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), ⋃ (_ : n ≤ N), f n))) <
    ε / 2
⊢ dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n)))
      (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ n ∈ Finset.range (N + 1), f n))) <
    ε / 2

Tactic:
simp only [Finset.mem_range, Nat.lt_add_one_iff]

Premises used: Nat.lt_add_one_iff, Finset.mem_range
-- 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)
⊢ dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n)))
      (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), ⋃ (_ : n ≤ N), f n))) <
    ε / 2

Tactic:
(dist_comm (α := ℝ) .. ▸ hN N (le_refl N))

Premises used: le_refl, Eq.rec, dist_comm
-- 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)
⊢ dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n)))
      (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), ⋃ (_ : n ≤ N), f n))) <
    ε / 2

Tactic:
exact (dist_comm (α := ℝ) .. ▸ hN N (le_refl N))
-- 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)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ n ∈ Finset.range (N + 1), f n) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n) : ℝ≥0∞)

Tactic:
measure_mono <| iUnion_subset <|
                      fun i ↦ iUnion_subset fun _ ↦ subset_iUnion f i

Premises used: Set.iUnion_subset, Set.subset_iUnion, MeasureTheory.measure_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)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ n ∈ Finset.range (N + 1), f n) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n) : ℝ≥0∞)

Tactic:
exact measure_mono <| iUnion_subset <|
                      fun i ↦ iUnion_subset fun _ ↦ subset_iUnion f i

Premises used: Set.iUnion_subset, Set.subset_iUnion, MeasureTheory.measure_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)
⊢ Subset.{u_1} (α := Set X) (⋃ n ∈ Finset.range (N + 1), f n) (⋃ (n : ℕ), f n)

Tactic:
iUnion_subset <| fun i ↦ iUnion_subset (fun _ ↦ subset_iUnion f i)

Premises used: Set.iUnion_subset, Set.subset_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)
⊢ Subset.{u_1} (α := Set X) (⋃ n ∈ Finset.range (N + 1), f n) (⋃ (n : ℕ), f n)

Tactic:
exact iUnion_subset <| fun i ↦ iUnion_subset (fun _ ↦ subset_iUnion f i)

Premises used: Set.iUnion_subset, Set.subset_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)
⊢ NullMeasurableSet (⋃ n ∈ Finset.range (N + 1), f n) μ

Tactic:
MeasurableSet.biUnion (countable_coe_iff.1 inferInstance)
                      (fun n _ ↦ (hf n).1.nullMeasurableSet)

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.NullMeasurableSet, inferInstance, Set.countable_coe_iff, And.left, Iff.mp, MeasureTheory.NullMeasurableSpace, MeasurableSet.biUnion
-- 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)
⊢ NullMeasurableSet (⋃ n ∈ Finset.range (N + 1), f n) μ

Tactic:
exact MeasurableSet.biUnion (countable_coe_iff.1 inferInstance)
                      (fun n _ ↦ (hf n).1.nullMeasurableSet)

Premises used: MeasurableSet.nullMeasurableSet, inferInstance, Set.countable_coe_iff, And.left, Iff.mp, MeasurableSet.biUnion
-- 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 ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) ≤
    μ.real (⋃ n ∈ Finset.range (N + 1), f n ∆ g n)

Tactic:
toReal_mono (measure_ne_top _ _) (measure_mono biSup_symmDiff_biSup_le)

Premises used: biSup_symmDiff_biSup_le, MeasureTheory.Measure.real, MeasureTheory.measure_ne_top, 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)
simp_rw :
  ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ n ∈ Finset.range (N + 1), f n ∆ g n)) ≤
    ENNReal.toReal (∑ a ∈ Finset.range (N + 1), (μ : (a : Set X) → ℝ≥0∞) (f a ∆ g a))
⊢ μ.real (⋃ n ∈ Finset.range (N + 1), f n ∆ g n) ≤ ∑ n ∈ Finset.range (N + 1), μ.real (f n ∆ g n)

Tactic:
simp_rw [measureReal_def, ← toReal_sum (fun _ _ ↦ measure_ne_top _ _)]

Premises used: MeasureTheory.measure_ne_top, MeasureTheory.measureReal_def, ENNReal.toReal_sum
-- 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 ∈ Finset.range (N + 1), f n ∆ g n)) ≤
    ENNReal.toReal (∑ a ∈ Finset.range (N + 1), (μ : (a : Set X) → ℝ≥0∞) (f a ∆ g a))

Tactic:
toReal_mono (ne_of_lt <| sum_lt_top.2 fun _ _ ↦ measure_lt_top μ _)
                            (measure_biUnion_finset_le _ _)

Premises used: Iff.mpr, MeasureTheory.measure_lt_top, ENNReal.sum_lt_top, MeasureTheory.measure_biUnion_finset_le, ne_of_lt, ENNReal.toReal_mono, symmDiff
-- 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 ∈ Finset.range (N + 1), f n ∆ g n)) ≤
    ENNReal.toReal (∑ a ∈ Finset.range (N + 1), (μ : (a : Set X) → ℝ≥0∞) (f a ∆ g a))

Tactic:
exact toReal_mono (ne_of_lt <| sum_lt_top.2 fun _ _ ↦ measure_lt_top μ _)
                            (measure_biUnion_finset_le _ _)

Premises used: Iff.mpr, MeasureTheory.measure_lt_top, ENNReal.sum_lt_top, MeasureTheory.measure_biUnion_finset_le, ne_of_lt, 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)
⊢ 0 ∈ Finset.range (N + 1)

Tactic:
simp
-- 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)
simp : HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * (ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)) ≤ ε / 2
⊢ ∑ n ∈ Finset.range (N + 1), ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) ≤ ε / 2

Tactic:
simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul,
                            Nat.cast_add, Nat.cast_one]

Premises used: Finset.card_range, Nat.cast_add, nsmul_eq_mul, Nat.cast_one, Finset.sum_const
-- 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 : ε / 2 * (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * (1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)) ≤ ε / 2
⊢ HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * (ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)) ≤ ε / 2

Tactic:
rw [div_mul_eq_div_mul_one_div, ← mul_assoc, mul_comm ((N : ℝ) + 1),
                            mul_assoc]

Premises used: mul_assoc, Nat.cast, HAdd.hAdd, mul_comm, div_mul_eq_div_mul_one_div, 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)
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
⊢ 0 ≤ ε / 2

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))))
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)
⊢ ε / 2 * (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * (1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)) ≤ ε / 2

Tactic:
exact mul_le_of_le_one_right (by linarith [ε_pos]) <|
                            le_of_eq <| mul_one_div_cancel <| Nat.cast_add_one_ne_zero _

Premises used: mul_le_of_le_one_right, mul_one_div_cancel, Nat.cast_add_one_ne_zero, le_of_eq