awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
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) < ε
have refine : (μ : (a : Set α) → ℝ≥0∞) ((⋃ i ∈ Finset.range n, t i) ∆ ⋃ (i : ℕ), f i) < ε
Tactic: refine ⟨⋃ i ∈ Finset.range n, t i, hC.biUnion_mem _ (fun i hi ↦ tC _), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
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) ∆ ⋃ (i : ℕ), f i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((⋃ i ∈ Finset.range n, t i ∆ f i) ∪ ⋃ i ∈ Ici n, f i) : ℝ≥0∞)
have 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)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
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
⊢ Membership.mem (γ := Set α) ((⋃ i ∈ Finset.range n, t i ∆ f i) ∪ ⋃ i ∈ Ici n, f i) x
have 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
Tactic: simp only [Finset.mem_range, mem_symmDiff, mem_iUnion, exists_prop, not_exists, not_and,
        mem_Ici, mem_union] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
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
⊢ (μ : (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∞)
have 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∞)
Tactic: apply (measure_union_le _ _).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
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∞) ((μ : (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∞)
have 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∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
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 ∈ 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∞)
have bc : ∀ i ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (t i ∆ f i) ≤ δ i
Tactic: gcongr with i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
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 ∈ 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∞)
have bc : LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, δ i) (∑' (i : ℕ), δ i)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
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
⊢ (μ : (a : Set α) → ℝ≥0∞) ((⋃ i ∈ Finset.range n, t i) ∆ ⋃ (i : ℕ), f i) < ε
have 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∞)
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 ε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) ((⋃ i ∈ Finset.range n, t i) ∆ ⋃ (i : ℕ), f i) < ε
have 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∞)
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 ε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) ((⋃ i ∈ Finset.range n, t i) ∆ ⋃ (i : ℕ), f i) < ε
have 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∞)
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 ε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) ((⋃ i ∈ Finset.range n, t i) ∆ ⋃ (i : ℕ), f i) < ε
have 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∞)
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 ε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) ((⋃ i ∈ Finset.range n, t i) ∆ ⋃ (i : ℕ), f i) < ε
have calc₄ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (∑' (i : ℕ), δ i : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i) : ℝ≥0∞) <
  ε / 2 + ε / 2
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 ε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
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 α),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) t ∧
      (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
have apply : ∃ (D : Set (Set α)),
  D.Countable ∧
    D ⊆ (supClosure : (a : Set (Set α)) → Set (Set α)) C ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply exists_measure_symmDiff_lt_of_generateFrom_isSetRing hC.isSetRing_supClosure ?_ ?_ hs hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
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∞)
⊢ ∃ (t : Set α),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) t ∧
      (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
have apply₁ : mα = generateFrom ((supClosure : (a : Set (Set α)) → Set (Set α)) C)
Tactic: apply exists_measure_symmDiff_lt_of_generateFrom_isSetRing hC.isSetRing_supClosure ?_ ?_ hs hε