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
⊢ ∀ (i : ℕ), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ f i) < δ i

Tactic:
have A i : ∃ t ∈ C, μ (t ∆ (f i)) < δ i := hf i _ (δpos i)
-- 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
A : ∀ (i : ℕ), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ f i) < δ i
choose! :
  ∀ (t : (i : ℕ) → Set α) (tC : ∀ (i : ℕ), t i ∈ C) (ht : ∀ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t i ∆ f i) < δ i),
    ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ⋃ (i : ℕ), f i) < ε
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ⋃ (i : ℕ), f i) < ε

Tactic:
choose! t tC ht using A
-- 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
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i)) atTop (𝓝 0)

Tactic:
have : Tendsto (fun n ↦ μ (⋃ i ∈ Ici n, f i)) atTop (𝓝 0) :=
      tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint
        (fun i ↦ (f_meas i).nullMeasurableSet) f_disj
-- 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 : ℕ), (μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i) < ε / 2

Tactic:
((tendsto_order.1 this).2 _ (ENNReal.half_pos εpos.ne')).exists

Premises used: tendsto_order, LT.lt.ne', Filter.Eventually.exists, And.right, ENNReal.half_pos, Iff.mp
-- 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)
obtain :
  ∀ (n : ℕ) (hn : (μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i) < ε / 2),
    ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ⋃ (i : ℕ), f i) < ε
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ⋃ (i : ℕ), f i) < ε

Tactic:
obtain ⟨n, hn⟩ : ∃ n, μ (⋃ i ∈ Ici n, f i) < ε / 2 :=
      ((tendsto_order.1 this).2 _ (ENNReal.half_pos εpos.ne')).exists

Premises used: tendsto_order, LT.lt.ne', Filter.Eventually.exists, And.right, ENNReal.half_pos, Iff.mp
-- 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
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ⋃ (i : ℕ), f i) < ε

Tactic:
⟨⋃ i ∈ Finset.range n, t i, hC.biUnion_mem _ (fun i hi ↦ tC _), ?_⟩

Premises used: And.intro, Exists.intro, MeasureTheory.IsSetRing.biUnion_mem, Set.iUnion
-- 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
refine : (μ : (a : Set α) → ℝ≥0∞) ((⋃ i ∈ Finset.range n, t i) ∆ ⋃ (i : ℕ), f i) < ε
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ⋃ (i : ℕ), f i) < ε

Tactic:
refine ⟨⋃ i ∈ Finset.range n, t i, hC.biUnion_mem _ (fun i hi ↦ 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 : 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
h₁ :
  Subset.{u_1} (α := Set α) ((⋃ i ∈ Finset.range n, t i) ∆ ⋃ (i : ℕ), f i)
    ((⋃ i ∈ Finset.range n, t i ∆ f i) ∪ ⋃ i ∈ Ici n, f i)
⊢ 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∞)

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
x : α
hx : Membership.mem (γ := Set α) ((⋃ i ∈ Finset.range n, t i) ∆ ⋃ (i : ℕ), f i) x
h₁ :
  ∀ (hx : ((∃ i < n, x ∈ t i) ∧ ∀ (x_1 : ℕ), x ∉ f x_1) ∨ (∃ (i : ℕ), x ∈ f i) ∧ ∀ x_1 < n, x ∉ t x_1),
    (∃ i < n, x ∈ t i ∧ x ∉ f i ∨ x ∈ f i ∧ x ∉ t i) ∨ ∃ (i : ℕ), n ≤ i ∧ x ∈ f i
⊢ Membership.mem (γ := Set α) ((⋃ i ∈ Finset.range n, t i ∆ f i) ∪ ⋃ i ∈ Ici n, f i) x

Tactic:
simp only [Finset.mem_range, mem_symmDiff, mem_iUnion, exists_prop, not_exists, not_and,
        mem_Ici, mem_union] at hx ⊢

Premises used: Set.mem_union, Set.mem_symmDiff, Set.mem_iUnion, not_exists, Finset.mem_range, exists_prop, Set.mem_Ici, not_and
-- 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
x : α
hx : ((∃ i < n, x ∈ t i) ∧ ∀ (x_1 : ℕ), x ∉ f x_1) ∨ (∃ (i : ℕ), x ∈ f i) ∧ ∀ x_1 < n, x ∉ t x_1
⊢ (∃ i < n, x ∈ t i ∧ x ∉ f i ∨ x ∈ f i ∧ x ∉ t i) ∨ ∃ (i : ℕ), n ≤ i ∧ x ∈ f i

Tactic:
grind
-- 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
apply :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Finset.range n, t i ∆ f i) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i) : ℝ≥0∞) ≤
    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∞)
⊢ (μ : (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∞)

Tactic:
apply (measure_union_le _ _).trans

Premises used: LE.le.trans, MeasureTheory.measure_union_le
-- 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
bc :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Finset.range n, t i ∆ f i) : ℝ≥0∞)
    (∑ i ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (t i ∆ f i) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Finset.range n, t i ∆ f i) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i) : ℝ≥0∞) ≤
    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∞)

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
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Finset.range n, t i ∆ f i) : ℝ≥0∞)
    (∑ i ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (t i ∆ f i) : ℝ≥0∞)

Tactic:
apply measure_biUnion_finset_le

Premises used: MeasureTheory.measure_biUnion_finset_le
-- 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
bc : ∀ i ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (t i ∆ f i) ≤ δ 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∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (∑ i ∈ Finset.range n, δ i : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i) : ℝ≥0∞)

Tactic:
gcongr with i
-- 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
i : ℕ
h_1 : i ∈ Finset.range n
⊢ (μ : (a : Set α) → ℝ≥0∞) (t i ∆ f i) ≤ δ i

Tactic:
(ht i).le

Premises used: LT.lt.le
-- 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
i : ℕ
h_1 : i ∈ Finset.range n
⊢ (μ : (a : Set α) → ℝ≥0∞) (t i ∆ f i) ≤ δ i

Tactic:
exact (ht i).le

Premises used: LT.lt.le
-- 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
bc : LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, δ i) (∑' (i : ℕ), δ i)
⊢ 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∞)

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
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, δ i) (∑' (i : ℕ), δ i)

Tactic:
ENNReal.sum_le_tsum (Finset.range n)

Premises used: Finset.range, ENNReal.sum_le_tsum
-- 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
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, δ i) (∑' (i : ℕ), δ i)

Tactic:
exact ENNReal.sum_le_tsum (Finset.range n)

Premises used: Finset.range, ENNReal.sum_le_tsum