awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
this : IsClosed.{u_1} (X := MeasuredSets μ) {s : MeasuredSets μ | ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)}
s : MeasuredSets μ
hs : s ∈ C'
⊢ m₁ s = (m : (a : Set α) → E) (↑s : Set α)

Tactic:
C'_dense.extend_eq lip.continuous ⟨s, hs⟩

Premises used: Subtype.mk, LipschitzWith.continuous, Dense.extend_eq
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
this : IsClosed.{u_1} (X := MeasuredSets μ) {s : MeasuredSets μ | ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)}
s : MeasuredSets μ
hs : s ∈ C'
⊢ m₁ s = (m : (a : Set α) → E) (↑s : Set α)

Tactic:
exact C'_dense.extend_eq lip.continuous ⟨s, hs⟩

Premises used: Subtype.mk, LipschitzWith.continuous, Dense.extend_eq
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
this : IsClosed.{u_1} (X := MeasuredSets μ) {s : MeasuredSets μ | ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)}
⊢ Dense.{u_1} (X := MeasuredSets μ) {s : MeasuredSets μ | ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)}

Tactic:
have : Dense {s | ‖m₁ s‖ₑ ≤ μ s} := by
      apply C'_dense.mono
      intro s hs
      simp only [Set.mem_setOf_eq]
      convert! hm s (C'C s hs)
      exact C'_dense.extend_eq lip.continuous ⟨s, hs⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
this_1 : IsClosed.{u_1} (X := MeasuredSets μ) {s : MeasuredSets μ | ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)}
this : Dense.{u_1} (X := MeasuredSets μ) {s : MeasuredSets μ | ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)}
⊢ ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)

Tactic:
simpa only [Dense, IsClosed.closure_eq, Set.mem_setOf_eq] using this

Premises used: IsClosed.closure_eq, Dense, Set.mem_setOf_eq
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
⊢ ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)

Tactic:
have hBound : ∀ s, ‖m₁ s‖ₑ ≤ μ s := by
    have : IsClosed {s | ‖m₁ s‖ₑ ≤ μ s} :=
      isClosed_le m₁_lip.continuous.enorm MeasuredSets.continuous_measure
    have : Dense {s | ‖m₁ s‖ₑ ≤ μ s} := by
      apply C'_dense.mono
      intro s hs
      simp only [Set.mem_setOf_eq]
      convert! hm s (C'C s hs)
      exact C'_dense.extend_eq lip.continuous ⟨s, hs⟩
    simpa only [Dense, IsClosed.closure_eq, Set.mem_setOf_eq] using this
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)
s t : MeasuredSets μ
h : Disjoint (↑s : Set α) (↑t : Set α)
this :
  ∀ ε > 0, ‖m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) - m₁ s - m₁ t‖ₑ < ε
rw : ‖m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) - m₁ s - m₁ t‖ₑ = 0
⊢ m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) = m₁ s + m₁ t

Tactic:
rw [← sub_eq_zero, ← enorm_eq_zero, sub_add_eq_sub_sub]

Premises used: sub_eq_zero, sub_add_eq_sub_sub, enorm_eq_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)
s t : MeasuredSets μ
h : Disjoint (↑s : Set α) (↑t : Set α)
this :
  ∀ ε > 0, ‖m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) - m₁ s - m₁ t‖ₑ < ε
⊢ ‖m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) - m₁ s - m₁ t‖ₑ = 0

Tactic:
eq_bot_iff.2 (le_of_forall_gt this)

Premises used: Iff.mpr, eq_bot_iff, le_of_forall_gt
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)
s t : MeasuredSets μ
h : Disjoint (↑s : Set α) (↑t : Set α)
this :
  ∀ ε > 0, ‖m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) - m₁ s - m₁ t‖ₑ < ε
⊢ ‖m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) - m₁ s - m₁ t‖ₑ = 0

Tactic:
exact eq_bot_iff.2 (le_of_forall_gt this)

Premises used: Iff.mpr, eq_bot_iff, le_of_forall_gt
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)
s t : MeasuredSets μ
h : Disjoint (↑s : Set α) (↑t : Set α)
suffices :
  ∀ ε > 0, ‖m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) - m₁ s - m₁ t‖ₑ < ε
⊢ m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) = m₁ s + m₁ t

Tactic:
suffices ∀ ε > 0, ‖m₁ (⟨s ∪ t, s.2.union t.2⟩) - m₁ s - m₁ t‖ₑ < ε by
      rw [← sub_eq_zero, ← enorm_eq_zero, sub_add_eq_sub_sub]
      exact eq_bot_iff.2 (le_of_forall_gt this)
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)
s t : MeasuredSets μ
h : Disjoint (↑s : Set α) (↑t : Set α)
ε : ℝ≥0∞
εpos : ε > 0
⊢ Ne (α := ℝ≥0∞) 8 ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)
s t : MeasuredSets μ
h : Disjoint (↑s : Set α) (↑t : Set α)
ε : ℝ≥0∞
εpos : ε > 0
⊢ Ne (α := ℝ≥0∞) 8 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)
s t : MeasuredSets μ
h : Disjoint (↑s : Set α) (↑t : Set α)
ε : ℝ≥0∞
εpos : ε > 0
obtain :
  ∀ (δ : ℝ≥0∞) (δpos : 0 < δ) (hδ : 8 * δ = ε),
    ‖m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) - m₁ s - m₁ t‖ₑ < ε
⊢ ‖m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) - m₁ s - m₁ t‖ₑ < ε

Tactic:
obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ 8 * δ = ε :=
      ⟨ε / 8, (ENNReal.div_pos εpos.ne' (by simp)), ENNReal.mul_div_cancel (by simp) (by simp)⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)
s t : MeasuredSets μ
h : Disjoint (↑s : Set α) (↑t : Set α)
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
⊢ ∃ s' ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s' ∆ (↑s : Set α)) < δ

Tactic:
h'C _ _ s.2 δpos

Premises used: Subtype.property
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)
s t : MeasuredSets μ
h : Disjoint (↑s : Set α) (↑t : Set α)
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
obtain :
  ∀ (s' : Set α) (s'C : s' ∈ C) (hs' : (μ : (a : Set α) → ℝ≥0∞) (s' ∆ (↑s : Set α)) < δ),
    ‖m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) - m₁ s - m₁ t‖ₑ < ε
⊢ ‖m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) - m₁ s - m₁ t‖ₑ < ε

Tactic:
obtain ⟨s', s'C, hs'⟩ : ∃ s' ∈ C, μ (s' ∆ s) < δ := h'C _ _ s.2 δpos

Premises used: Subtype.property
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)
s t : MeasuredSets μ
h : Disjoint (↑s : Set α) (↑t : Set α)
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : (μ : (a : Set α) → ℝ≥0∞) (s' ∆ (↑s : Set α)) < δ
⊢ ∃ t' ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t' ∆ (↑t : Set α)) < δ

Tactic:
h'C _ _ t.2 δpos

Premises used: Subtype.property
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)
s t : MeasuredSets μ
h : Disjoint (↑s : Set α) (↑t : Set α)
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : (μ : (a : Set α) → ℝ≥0∞) (s' ∆ (↑s : Set α)) < δ
obtain :
  ∀ (t' : Set α) (t'C : t' ∈ C) (ht' : (μ : (a : Set α) → ℝ≥0∞) (t' ∆ (↑t : Set α)) < δ),
    ‖m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) - m₁ s - m₁ t‖ₑ < ε
⊢ ‖m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) - m₁ s - m₁ t‖ₑ < ε

Tactic:
obtain ⟨t', t'C, ht'⟩ : ∃ t' ∈ C, μ (t' ∆ t) < δ := h'C _ _ t.2 δpos

Premises used: Subtype.property
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)
s t : MeasuredSets μ
h : Disjoint (↑s : Set α) (↑t : Set α)
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : (μ : (a : Set α) → ℝ≥0∞) (s' ∆ (↑s : Set α)) < δ
t' : Set α
t'C : t' ∈ C
ht' : (μ : (a : Set α) → ℝ≥0∞) (t' ∆ (↑t : Set α)) < δ
⊢ m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) t' ⋯) = (m : (a : Set α) → E) t'

Tactic:
have : m₁ ⟨t', hCmeas _ t'C⟩ = m t' :=
        C'_dense.extend_eq lip.continuous ⟨⟨t', hCmeas _ t'C⟩, ⟨t', t'C, rfl⟩⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)
s t : MeasuredSets μ
h : Disjoint (↑s : Set α) (↑t : Set α)
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : (μ : (a : Set α) → ℝ≥0∞) (s' ∆ (↑s : Set α)) < δ
t' : Set α
t'C : t' ∈ C
ht' : (μ : (a : Set α) → ℝ≥0∞) (t' ∆ (↑t : Set α)) < δ
this : m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) t' ⋯) = (m : (a : Set α) → E) t'
rw : edist (m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) t' ⋯)) (m₁ t) < δ
⊢ ‖HSub.hSub (α := E) ((m : (a : Set α) → E) t' : E) (m₁ t)‖ₑ < δ

Tactic:
rw [← this, ← edist_eq_enorm_sub]

Premises used: edist_eq_enorm_sub