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 : IsSetSemiring 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 : Set α),
          Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s ∧
            (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
m₀ : AddContent.{u_1, u_2} (α := α) E ((supClosure : (a : Set (Set α)) → Set (Set α)) C) := m.supClosure (C := C) hC
hm₀ : m₀ = m.supClosure (C := C) hC
A :
  ∀ (s : Set α)
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s),
    enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
s : Set α
hs : ∃ (P : Finpartition s), (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
rcases : ∀ (P : Finpartition s) (PC : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C), MeasurableSet s
⊢ MeasurableSet s

Tactic:
rcases hs with ⟨P, PC⟩
-- 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 : IsSetSemiring 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 : Set α),
          Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s ∧
            (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
m₀ : AddContent.{u_1, u_2} (α := α) E ((supClosure : (a : Set (Set α)) → Set (Set α)) C) := m.supClosure (C := C) hC
hm₀ : m₀ = m.supClosure (C := C) hC
A :
  ∀ (s : Set α)
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s),
    enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
s : Set α
P : Finpartition s
PC : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
rw : MeasurableSet.{u_1} (α := α) (⋃ x ∈ P.parts (a := s), id x)
⊢ MeasurableSet s

Tactic:
rw [← P.sup_parts, Finset.sup_set_eq_biUnion]

Premises used: Finset.sup_set_eq_biUnion, Finpartition.sup_parts
-- 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 : IsSetSemiring 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 : Set α),
          Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s ∧
            (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
m₀ : AddContent.{u_1, u_2} (α := α) E ((supClosure : (a : Set (Set α)) → Set (Set α)) C) := m.supClosure (C := C) hC
hm₀ : m₀ = m.supClosure (C := C) hC
A :
  ∀ (s : Set α)
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s),
    enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
s : Set α
P : Finpartition s
PC : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
⊢ MeasurableSet.{u_1} (α := α) (⋃ x ∈ P.parts (a := s), id x)

Tactic:
Finset.measurableSet_biUnion _ (fun b hb ↦ hCmeas _ (PC hb))

Premises used: id, Finset.measurableSet_biUnion
-- 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 : IsSetSemiring 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 : Set α),
          Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s ∧
            (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
m₀ : AddContent.{u_1, u_2} (α := α) E ((supClosure : (a : Set (Set α)) → Set (Set α)) C) := m.supClosure (C := C) hC
hm₀ : m₀ = m.supClosure (C := C) hC
A :
  ∀ (s : Set α)
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s),
    enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
s : Set α
P : Finpartition s
PC : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
⊢ MeasurableSet.{u_1} (α := α) (⋃ x ∈ P.parts (a := s), id x)

Tactic:
exact Finset.measurableSet_biUnion _ (fun b hb ↦ hCmeas _ (PC hb))

Premises used: Finset.measurableSet_biUnion
-- 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 : IsSetSemiring 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 : Set α),
          Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s ∧
            (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
m₀ : AddContent.{u_1, u_2} (α := α) E ((supClosure : (a : Set (Set α)) → Set (Set α)) C) := m.supClosure (C := C) hC
hm₀ : m₀ = m.supClosure (C := C) hC
A :
  ∀ (s : Set α)
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s),
    enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
⊢ ∀ (s : Set α)
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s),
    MeasurableSet s

Tactic:
have B (s) (hs : s ∈ supClosure C) : MeasurableSet s := by
    rw [hC.mem_supClosure_iff] at hs
    rcases hs with ⟨P, PC⟩
    rw [← P.sup_parts, Finset.sup_set_eq_biUnion]
    exact Finset.measurableSet_biUnion _ (fun b hb ↦ hCmeas _ (PC hb))
-- 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 : IsSetSemiring 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 : Set α),
          Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s ∧
            (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
m₀ : AddContent.{u_1, u_2} (α := α) E ((supClosure : (a : Set (Set α)) → Set (Set α)) C) := m.supClosure (C := C) hC
hm₀ : m₀ = m.supClosure (C := C) hC
A :
  ∀ (s : Set α)
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s),
    enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
B :
  ∀ (s : Set α)
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s),
    MeasurableSet s
rcases :
  ∀ (m' : VectorMeasure α E)
    (hm' :
      ∀ (s : Set α),
        Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s →
          (↑m' : Set α → E) s = (m₀ : (a : Set α) → E) s)
    (m'bound : ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s),
    ∃ (m' : VectorMeasure α E),
      (∀ s ∈ C, (↑m' : Set α → E) s = (m : (a : Set α) → E) s) ∧
        ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
⊢ ∃ (m' : VectorMeasure α E),
    (∀ s ∈ C, (↑m' : Set α → E) s = (m : (a : Set α) → E) s) ∧
      ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
rcases VectorMeasure.exists_extension_of_isSetRing_of_le_measure_of_dense
    hC.isSetRing_supClosure B A h'C with ⟨m', hm', m'bound⟩

Premises used: MeasureTheory.IsSetSemiring.isSetRing_supClosure, MeasureTheory.VectorMeasure.exists_extension_of_isSetRing_of_le_measure_of_dense
-- 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 : IsSetSemiring 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 : Set α),
          Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s ∧
            (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
m₀ : AddContent.{u_1, u_2} (α := α) E ((supClosure : (a : Set (Set α)) → Set (Set α)) C) := m.supClosure (C := C) hC
hm₀ : m₀ = m.supClosure (C := C) hC
A :
  ∀ (s : Set α)
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s),
    enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
B :
  ∀ (s : Set α)
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s),
    MeasurableSet s
m' : VectorMeasure α E
hm' :
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s →
      (↑m' : Set α → E) s = (m₀ : (a : Set α) → E) s
m'bound : ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
⊢ ∃ (m' : VectorMeasure α E),
    (∀ s ∈ C, (↑m' : Set α → E) s = (m : (a : Set α) → E) s) ∧
      ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
⟨m', fun s hs ↦ ?_, m'bound⟩

Premises used: And.intro, Exists.intro
-- 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 : IsSetSemiring 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 : Set α),
          Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s ∧
            (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
m₀ : AddContent.{u_1, u_2} (α := α) E ((supClosure : (a : Set (Set α)) → Set (Set α)) C) := m.supClosure (C := C) hC
hm₀ : m₀ = m.supClosure (C := C) hC
A :
  ∀ (s : Set α)
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s),
    enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
B :
  ∀ (s : Set α)
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s),
    MeasurableSet s
m' : VectorMeasure α E
hm' :
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s →
      (↑m' : Set α → E) s = (m₀ : (a : Set α) → E) s
m'bound : ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
refine : ∀ (s : Set α) (hs : s ∈ C), (↑m' : Set α → E) s = (m : (a : Set α) → E) s
⊢ ∃ (m' : VectorMeasure α E),
    (∀ s ∈ C, (↑m' : Set α → E) s = (m : (a : Set α) → E) s) ∧
      ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
refine ⟨m', fun s hs ↦ ?_, m'bound⟩
-- 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 : IsSetSemiring 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 : Set α),
          Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s ∧
            (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
m₀ : AddContent.{u_1, u_2} (α := α) E ((supClosure : (a : Set (Set α)) → Set (Set α)) C) := m.supClosure (C := C) hC
hm₀ : m₀ = m.supClosure (C := C) hC
A :
  ∀ (s : Set α)
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s),
    enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
B :
  ∀ (s : Set α)
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s),
    MeasurableSet s
m' : VectorMeasure α E
hm' :
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s →
      (↑m' : Set α → E) s = (m₀ : (a : Set α) → E) s
m'bound : ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
s : Set α
hs : s ∈ C
rw : Eq.{u_2 + 1} (α := E) ((m₀ : (a : Set α) → E) s : E) ((m : (a : Set α) → E) s : E)
⊢ (↑m' : Set α → E) s = (m : (a : Set α) → E) s

Tactic:
rw [hm' _ (subset_supClosure hs)]

Premises used: subset_supClosure
-- 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 : IsSetSemiring 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 : Set α),
          Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s ∧
            (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
m₀ : AddContent.{u_1, u_2} (α := α) E ((supClosure : (a : Set (Set α)) → Set (Set α)) C) := m.supClosure (C := C) hC
hm₀ : m₀ = m.supClosure (C := C) hC
A :
  ∀ (s : Set α)
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s),
    enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
B :
  ∀ (s : Set α)
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s),
    MeasurableSet s
m' : VectorMeasure α E
hm' :
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s →
      (↑m' : Set α → E) s = (m₀ : (a : Set α) → E) s
m'bound : ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
s : Set α
hs : s ∈ C
⊢ Eq.{u_2 + 1} (α := E) ((m₀ : (a : Set α) → E) s : E) ((m : (a : Set α) → E) s : E)

Tactic:
AddContent.supClosure_apply_of_mem _ _ hs

Premises used: MeasureTheory.AddContent.supClosure_apply_of_mem
-- 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 : IsSetSemiring 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 : Set α),
          Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s ∧
            (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
m₀ : AddContent.{u_1, u_2} (α := α) E ((supClosure : (a : Set (Set α)) → Set (Set α)) C) := m.supClosure (C := C) hC
hm₀ : m₀ = m.supClosure (C := C) hC
A :
  ∀ (s : Set α)
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s),
    enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
B :
  ∀ (s : Set α)
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s),
    MeasurableSet s
m' : VectorMeasure α E
hm' :
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s →
      (↑m' : Set α → E) s = (m₀ : (a : Set α) → E) s
m'bound : ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
s : Set α
hs : s ∈ C
⊢ Eq.{u_2 + 1} (α := E) ((m₀ : (a : Set α) → E) s : E) ((m : (a : Set α) → E) s : E)

Tactic:
exact AddContent.supClosure_apply_of_mem _ _ hs

Premises used: MeasureTheory.AddContent.supClosure_apply_of_mem
-- 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 : IsSetSemiring C
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : hα = generateFrom C
h''C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
apply : ∀ s ∈ C, MeasurableSet s
apply₁ :
  ∀ (t : Set α) (ε : ℝ≥0∞),
    MeasurableSet t →
      0 < ε →
        ∃ (s : Set α),
          Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s ∧
            (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
⊢ ∃ (m' : VectorMeasure α E),
    (∀ s ∈ C, (↑m' : Set α → E) s = (m : (a : Set α) → E) s) ∧
      ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
apply VectorMeasure.exists_extension_of_isSetSemiring_of_le_measure_of_dense hC ?_ hm ?_

Premises used: MeasureTheory.VectorMeasure.exists_extension_of_isSetSemiring_of_le_measure_of_dense
-- 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 : IsSetSemiring C
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : hα = generateFrom C
h''C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set α
hs : s ∈ C
rw : MeasurableSet s
⊢ MeasurableSet s

Tactic:
rw [h'C]
-- 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 : IsSetSemiring C
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : hα = generateFrom C
h''C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set α
hs : s ∈ C
⊢ MeasurableSet s

Tactic:
measurableSet_generateFrom hs

Premises used: MeasurableSpace.measurableSet_generateFrom
-- 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 : IsSetSemiring C
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : hα = generateFrom C
h''C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set α
hs : s ∈ C
⊢ MeasurableSet s

Tactic:
exact measurableSet_generateFrom hs

Premises used: MeasurableSpace.measurableSet_generateFrom
-- 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 : IsSetSemiring C
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : hα = generateFrom C
h''C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
ε : ℝ≥0∞
ht : MeasurableSet t
εpos : 0 < ε
⊢ ∃ (s : Set α),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s ∧
      (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε

Tactic:
exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring hC h''C h'C ht εpos

Premises used: MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring
-- 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 : IsSetSemiring C
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : hα = generateFrom C
h''C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
ε : ℝ≥0∞
ht : MeasurableSet t
εpos : 0 < ε
⊢ ∃ (s : Set α),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s ∧
      (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε

Tactic:
exact exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring hC h''C h'C ht εpos

Premises used: MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring
-- 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 : IsSetSemiring C
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : hα = generateFrom C
s : Set α
hs : s ∈ C
rw : MeasurableSet s
⊢ MeasurableSet s

Tactic:
rw [h'C]
-- 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 : IsSetSemiring C
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : hα = generateFrom C
s : Set α
hs : s ∈ C
⊢ MeasurableSet s

Tactic:
measurableSet_generateFrom hs

Premises used: MeasurableSpace.measurableSet_generateFrom
-- 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 : IsSetSemiring C
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : hα = generateFrom C
s : Set α
hs : s ∈ C
⊢ MeasurableSet s

Tactic:
exact measurableSet_generateFrom hs

Premises used: MeasurableSpace.measurableSet_generateFrom
-- 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 : IsSetSemiring C
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : hα = generateFrom C
⊢ ∀ (s : Set α) (hs : s ∈ C), MeasurableSet s

Tactic:
have M (s) (hs : s ∈ C) : MeasurableSet s := by
    rw [h'C]; exact measurableSet_generateFrom hs