awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i)
have h : ∀ (x : α),
  Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x ↔
    Membership.mem (γ := Set α) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i) x
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
x : α
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x ↔
    Membership.mem (γ := Set α) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i) x
have h : (∃ (i : ℕ), x ∈ f i) ↔ (∃ i < n, x ∈ f i) ∨ ∃ (i : ℕ), n ≤ i ∧ x ∈ f i
Tactic: simp
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (hypothesis)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
⊢ m (⋃ (i : ℕ), f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
have this : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i)
Tactic: have : ⋃ i, f i = (⋃ i ∈ Finset.range n, f i) ∪ (⋃ i ∈ Set.Ici n, f i) := by
        ext; simp; grind
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
this : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i)
⊢ m (⋃ (i : ℕ), f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
have rw : m ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
this : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i)
⊢ m ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
have a : MeasurableSet.{u_1} (α := α) (⋃ i ∈ Finset.range n, f i)
Tactic: apply h'm
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
this : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i)
a : MeasurableSet.{u_1} (α := α) (⋃ i ∈ Finset.range n, f i)
⊢ m ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
have a₁ : MeasurableSet.{u_1} (α := α) (⋃ i ∈ Set.Ici n, f i)
Tactic: apply h'm
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
this : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i)
a : MeasurableSet.{u_1} (α := α) (⋃ i ∈ Finset.range n, f i)
a₁ : MeasurableSet.{u_1} (α := α) (⋃ i ∈ Set.Ici n, f i)
⊢ m ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
have a₂ : Disjoint.{u_1} (α := Set α) (⋃ i ∈ Finset.range n, f i) (⋃ i ∈ Set.Ici n, f i)
Tactic: apply h'm
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
this : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) ((⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i)
⊢ Disjoint.{u_1} (α := Set α) (⋃ i ∈ Finset.range n, f i) (⋃ i ∈ Set.Ici n, f i)
have a : ∀ (i : ℕ) (i_1 : n ≤ i) (i_2 : ℕ) (i_3 : i_2 < n), Disjoint (f i_2) (f i)
Tactic: simp only [Finset.mem_range, Set.mem_Ici, Set.disjoint_iUnion_right,
          Set.disjoint_iUnion_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (hypothesis)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
⊢ Filter.Tendsto (β := ENNReal) (fun (e : ℕ) ↦ ‖m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range e, m (f i)‖ₑ) Filter.atTop
    (nhds 0)
have B : ∀ (n : ℕ), m (⋃ (i : ℕ), f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
Tactic: have B n : m (⋃ i, f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i) := by
      have : ⋃ i, f i = (⋃ i ∈ Finset.range n, f i) ∪ (⋃ i ∈ Set.Ici n, f i) := by
        ext; simp; grind
      rw [this]
      apply h'm
      · exact Finset.measurableSet_biUnion _ (fun i hi ↦ f_meas i)
      · exact MeasurableSet.biUnion (Set.to_countable _) (fun i hi ↦ f_meas i)
      · simp only [Finset.mem_range, Set.mem_Ici, Set.disjoint_iUnion_right,
          Set.disjoint_iUnion_left]
        intro i hi j hj
        exact f_disj (hj.trans_le hi).ne
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
B : ∀ (n : ℕ), m (⋃ (i : ℕ), f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
n : ℕ
⊢ m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i)
have rw : ∑ i ∈ Finset.range n, m (f i) + m (⋃ i ∈ Set.Ici n, f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i)
Tactic: rw [B n, A]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (hypothesis)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
B : ∀ (n : ℕ), m (⋃ (i : ℕ), f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
⊢ Filter.Tendsto (β := ENNReal) (fun (e : ℕ) ↦ ‖m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range e, m (f i)‖ₑ) Filter.atTop
    (nhds 0)
have C : ∀ (n : ℕ), m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i)
Tactic: have C n : m (⋃ i, f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i) := by
      rw [B n, A]; simp
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
B : ∀ (n : ℕ), m (⋃ (i : ℕ), f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
C : ∀ (n : ℕ), m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i)
⊢ Filter.Tendsto (β := ENNReal) (fun (e : ℕ) ↦ ‖m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range e, m (f i)‖ₑ) Filter.atTop
    (nhds 0)
have simp : Filter.Tendsto (β := ENNReal) (fun (e : ℕ) ↦ ‖m (⋃ i ∈ Set.Ici e, f i)‖ₑ) Filter.atTop (nhds 0)
Tactic: simp only [C]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
B : ∀ (n : ℕ), m (⋃ (i : ℕ), f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
C : ∀ (n : ℕ), m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i)
⊢ Filter.Tendsto (β := ENNReal) (fun (e : ℕ) ↦ ‖m (⋃ i ∈ Set.Ici e, f i)‖ₑ) Filter.atTop (nhds 0)
have apply : Filter.Tendsto (β := ENNReal) (fun (n : ℕ) ↦ (μ : (a : Set α) → ENNReal) (⋃ i ∈ Set.Ici n, f i)) Filter.atTop (nhds ⊥)
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
      (h := fun n ↦ μ (⋃ i ∈ Set.Ici n, f i)) ?_ (fun i ↦ bot_le) (fun i ↦ hm _)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (hypothesis)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
⊢ ∃ (m' : VectorMeasure α E),
    (∀ s ∈ C, (↑m' : Set α → E) s = (m : (a : Set α) → E) s) ∧
      ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
have C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
Tactic: have C'C (s : MeasuredSets μ) (hs : s ∈ C') : (s : Set α) ∈ C := by
    rcases hs with ⟨t, ht, rfl⟩; exact ht
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
⊢ Dense C'
have simp : ∀ (x : MeasuredSets μ) (ε : ℝ≥0∞), 0 < ε → ∃ y ∈ C', edist x y < ε
Tactic: simp only [Dense, EMetric.mem_closure_iff, gt_iff_lt]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
x : MeasuredSets μ
ε : ℝ≥0∞
εpos : 0 < ε
⊢ ∃ y ∈ C', edist x y < ε
have rcases : ∀ (s : Set α) (sC : s ∈ C) (hs : (μ : (a : Set α) → ℝ≥0∞) (s ∆ (↑x : Set α)) < ε), ∃ y ∈ C', edist x y < ε
Tactic: rcases h'C x ε x.2 εpos with ⟨s, sC, hs⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
x : MeasuredSets μ
ε : ℝ≥0∞
εpos : 0 < ε
s : Set α
sC : s ∈ C
hs : (μ : (a : Set α) → ℝ≥0∞) (s ∆ (↑x : Set α)) < ε
⊢ ∃ y ∈ C', edist x y < ε
have refine : edist x (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s sorry) < ε
Tactic: refine ⟨⟨s, hCmeas s sC⟩, ⟨s, sC, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
x : MeasuredSets μ
ε : ℝ≥0∞
εpos : 0 < ε
s : Set α
sC : s ∈ C
hs : (μ : (a : Set α) → ℝ≥0∞) (s ∆ (↑x : Set α)) < ε
⊢ edist x (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s ⋯) < ε
have rw : edist (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s sorry) x < ε
Tactic: rw [edist_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (hypothesis)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
⊢ ∃ (m' : VectorMeasure α E),
    (∀ s ∈ C, (↑m' : Set α → E) s = (m : (a : Set α) → E) s) ∧
      ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
have C'_dense : Dense C'
Tactic: have C'_dense : Dense C' := by
    simp only [Dense, EMetric.mem_closure_iff, gt_iff_lt]
    intro x ε εpos
    rcases h'C x ε x.2 εpos with ⟨s, sC, hs⟩
    refine ⟨⟨s, hCmeas s sC⟩, ⟨s, sC, rfl⟩, ?_⟩
    rw [edist_comm]
    exact hs
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (hypothesis)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
C'_dense : Dense C'
m₀ : (↑C' : Type u_1) → E := fun (x : (↑C' : Type u_1)) ↦ (m : (a : Set α) → E) (↑(↑x : MeasuredSets μ) : Set α)
s t : (↑C' : Type u_1)
⊢ edist (m₀ s) (m₀ t) ≤ (↑1 : ℝ≥0∞) * edist s t
have this : edist s t = edist (↑s : MeasuredSets μ) (↑t : MeasuredSets μ)
Tactic: have : edist s t = edist (s : MeasuredSets μ) t := rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
C'_dense : Dense C'
m₀ : (↑C' : Type u_1) → E := fun (x : (↑C' : Type u_1)) ↦ (m : (a : Set α) → E) (↑(↑x : MeasuredSets μ) : Set α)
s t : (↑C' : Type u_1)
this : edist s t = edist (↑s : MeasuredSets μ) (↑t : MeasuredSets μ)
⊢ edist (m₀ s) (m₀ t) ≤ (↑1 : ℝ≥0∞) * edist s t
have simp : ‖HSub.hSub (α := E) (β := E) ((m : (a : Set α) → E) (↑(↑s : MeasuredSets μ) : Set α) : E)
      ((m : (a : Set α) → E) (↑(↑t : MeasuredSets μ) : Set α) : E)‖ₑ ≤
  (μ : (a : Set α) → ℝ≥0∞) ((↑(↑s : MeasuredSets μ) : Set α) ∆ (↑(↑t : MeasuredSets μ) : Set α))
Tactic: simp only [ENNReal.coe_one, one_mul, this, MeasuredSets.edist_def, m₀, edist_eq_enorm_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
C'_dense : Dense C'
m₀ : (↑C' : Type u_1) → E := fun (x : (↑C' : Type u_1)) ↦ (m : (a : Set α) → E) (↑(↑x : MeasuredSets μ) : Set α)
s t : (↑C' : Type u_1)
this : edist s t = edist (↑s : MeasuredSets μ) (↑t : MeasuredSets μ)
⊢ ‖HSub.hSub (α := E) (β := E) ((m : (a : Set α) → E) (↑(↑s : MeasuredSets μ) : Set α) : E)
        ((m : (a : Set α) → E) (↑(↑t : MeasuredSets μ) : Set α) : E)‖ₑ ≤
    (μ : (a : Set α) → ℝ≥0∞) ((↑(↑s : MeasuredSets μ) : Set α) ∆ (↑(↑t : MeasuredSets μ) : Set α))
have rw : ‖HSub.hSub (α := E) (β := E) ((m : (a : Set α) → E) (↑(↑s : MeasuredSets μ) : Set α) : E)
      ((m : (a : Set α) → E) (↑(↑t : MeasuredSets μ) : Set α) : E)‖ₑ ≤
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((↑(↑s : MeasuredSets μ) : Set α) \ (↑(↑t : MeasuredSets μ) : Set α)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((↑(↑t : MeasuredSets μ) : Set α) \ (↑(↑s : MeasuredSets μ) : Set α)) : ℝ≥0∞)
Tactic: rw [measure_symmDiff_eq (by exact s.1.2.nullMeasurableSet) (by exact t.1.2.nullMeasurableSet)]