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₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)
hAddit :
  ∀ (s t : MeasuredSets μ) (h : Disjoint (↑s : Set α) (↑t : Set α)),
    m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) = m₁ s + m₁ t
m' : (s : Set α) → E :=
  fun (s : Set α) ↦ if hs : MeasurableSet s then m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s hs) else 0
m'' : VectorMeasure α E := of_additive_of_le_measure (μ := μ) m' ⋯ ⋯ ⋯
s : Set α
hs : s ∈ C
⊢ m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s ⋯) = (m : (a : Set α) → E) s

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

Premises used: Subtype.mk, LipschitzWith.continuous, Dense.extend_eq, And.intro, Exists.intro, 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 α)
hAddit :
  ∀ (s t : MeasuredSets μ) (h : Disjoint (↑s : Set α) (↑t : Set α)),
    m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) = m₁ s + m₁ t
m' : (s : Set α) → E :=
  fun (s : Set α) ↦ if hs : MeasurableSet s then m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s hs) else 0
m'' : VectorMeasure α E := of_additive_of_le_measure (μ := μ) m' ⋯ ⋯ ⋯
s : Set α
refine_2 : ‖m' s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
⊢ ‖(↑m'' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
change ‖m' s‖ₑ ≤ μ s

Premises used: DFunLike.coe
-- 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 α)
hAddit :
  ∀ (s t : MeasuredSets μ) (h : Disjoint (↑s : Set α) (↑t : Set α)),
    m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) = m₁ s + m₁ t
m' : (s : Set α) → E :=
  fun (s : Set α) ↦ if hs : MeasurableSet s then m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s hs) else 0
m'' : VectorMeasure α E := of_additive_of_le_measure (μ := μ) m' ⋯ ⋯ ⋯
s : Set α
pos : ∀ (hs : MeasurableSet s), ‖m' s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
neg : ∀ (hs : ¬MeasurableSet s), ‖m' s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
⊢ ‖m' s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
by_cases hs : MeasurableSet s

Premises used: MeasurableSet
-- 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 α)
hAddit :
  ∀ (s t : MeasuredSets μ) (h : Disjoint (↑s : Set α) (↑t : Set α)),
    m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) = m₁ s + m₁ t
m' : (s : Set α) → E :=
  fun (s : Set α) ↦ if hs : MeasurableSet s then m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s hs) else 0
m'' : VectorMeasure α E := of_additive_of_le_measure (μ := μ) m' ⋯ ⋯ ⋯
s : Set α
hs : MeasurableSet s
pos : ‖m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s ⋯)‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
⊢ ‖m' s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
simp only [hs, ↓reduceDIte, m']

Premises used: reduceDIte
-- 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 α)
hAddit :
  ∀ (s t : MeasuredSets μ) (h : Disjoint (↑s : Set α) (↑t : Set α)),
    m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) = m₁ s + m₁ t
m' : (s : Set α) → E :=
  fun (s : Set α) ↦ if hs : MeasurableSet s then m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s hs) else 0
m'' : VectorMeasure α E := of_additive_of_le_measure (μ := μ) m' ⋯ ⋯ ⋯
s : Set α
hs : MeasurableSet s
⊢ ‖m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s ⋯)‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
hBound ⟨s, hs⟩

Premises used: Subtype.mk
-- 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 α)
hAddit :
  ∀ (s t : MeasuredSets μ) (h : Disjoint (↑s : Set α) (↑t : Set α)),
    m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) = m₁ s + m₁ t
m' : (s : Set α) → E :=
  fun (s : Set α) ↦ if hs : MeasurableSet s then m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s hs) else 0
m'' : VectorMeasure α E := of_additive_of_le_measure (μ := μ) m' ⋯ ⋯ ⋯
s : Set α
hs : MeasurableSet s
⊢ ‖m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s ⋯)‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
exact hBound ⟨s, hs⟩

Premises used: Subtype.mk
-- 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 α)
hAddit :
  ∀ (s t : MeasuredSets μ) (h : Disjoint (↑s : Set α) (↑t : Set α)),
    m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) ((↑s : Set α) ∪ (↑t : Set α)) ⋯) = m₁ s + m₁ t
m' : (s : Set α) → E :=
  fun (s : Set α) ↦ if hs : MeasurableSet s then m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s hs) else 0
m'' : VectorMeasure α E := of_additive_of_le_measure (μ := μ) m' ⋯ ⋯ ⋯
s : Set α
hs : ¬MeasurableSet s
⊢ ‖m' s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
simp [m', 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 : 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) < ε
⊢ let m₀ := m.supClosure (C := C) hC;
  m₀ = m.supClosure (C := C) hC

Tactic:
set m₀ : AddContent E (supClosure C) := m.supClosure hC with hm₀

Premises used: supClosure, MeasureTheory.AddContent.supClosure, MeasureTheory.AddContent, DFunLike.coe
-- 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
s : Set α
hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s
⊢ ∃ (P : Finpartition s), (↑(P.parts (a := s)) : Set (Set α)) ⊆ C

Tactic:
rw [hC.mem_supClosure_iff] at hs

Premises used: MeasureTheory.IsSetSemiring.mem_supClosure_iff
-- 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
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),
    enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
⊢ enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) 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
s : Set α
P : Finpartition s
PC : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
nth_rewrite : enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) (P.parts (a := s).sup id)
⊢ enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
nth_rewrite 2 [← P.sup_parts]

Premises used: 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
s : Set α
P : Finpartition s
PC : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
rw :
  enorm.{u_2} (E := E) (∑ s ∈ P.parts (a := s), (m : (a : Set α) → E) s) ≤
    ∑ p ∈ P.parts (a := s), (μ : (a : Set α) → ℝ≥0∞) (id p)
⊢ enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) (P.parts (a := s).sup id)

Tactic:
rw [hm₀, AddContent.supClosure_apply_finpartition hC _ PC, Finset.sup_set_eq_biUnion,
      measure_biUnion_finset P.disjoint (fun b hb ↦ hCmeas _ (PC hb))]

Premises used: Finpartition.disjoint, Finset.sup_set_eq_biUnion, MeasureTheory.AddContent.supClosure_apply_finpartition, id, MeasureTheory.measure_biUnion_finset
-- 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
s : Set α
P : Finpartition s
PC : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
apply :
  LE.le (α := ℝ≥0∞) (∑ i ∈ P.parts (a := s), enorm.{u_2} (E := E) ((m : (a : Set α) → E) i : E))
    (∑ p ∈ P.parts (a := s), (μ : (a : Set α) → ℝ≥0∞) (id p))
⊢ enorm.{u_2} (E := E) (∑ s ∈ P.parts (a := s), (m : (a : Set α) → E) s) ≤
    ∑ p ∈ P.parts (a := s), (μ : (a : Set α) → ℝ≥0∞) (id p)

Tactic:
apply (enorm_sum_le _ _).trans

Premises used: enorm_sum_le, LE.le.trans
-- 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
s : Set α
P : Finpartition s
PC : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
h :
  ∀ (t : Set α) (ht : t ∈ P.parts (a := s)),
    enorm.{u_2} (E := E) ((m : (a : Set α) → E) t : E) ≤ (μ : (a : Set α) → ℝ≥0∞) (id t)
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ P.parts (a := s), enorm.{u_2} (E := E) ((m : (a : Set α) → E) i : E))
    (∑ p ∈ P.parts (a := s), (μ : (a : Set α) → ℝ≥0∞) (id p))

Tactic:
gcongr with t ht
-- 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
s : Set α
P : Finpartition s
PC : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
t : Set α
ht : t ∈ P.parts (a := s)
⊢ enorm.{u_2} (E := E) ((m : (a : Set α) → E) t : E) ≤ (μ : (a : Set α) → ℝ≥0∞) (id t)

Tactic:
hm _ (PC ht)
-- 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
s : Set α
P : Finpartition s
PC : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
t : Set α
ht : t ∈ P.parts (a := s)
⊢ enorm.{u_2} (E := E) ((m : (a : Set α) → E) t : E) ≤ (μ : (a : Set α) → ℝ≥0∞) (id t)

Tactic:
exact hm _ (PC ht)
-- 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
⊢ ∀ (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

Tactic:
have A (s) (hs : s ∈ supClosure C) : ‖m₀ s‖ₑ ≤ μ s := by
    rw [hC.mem_supClosure_iff] at hs
    rcases hs with ⟨P, PC⟩
    nth_rewrite 2 [← P.sup_parts]
    rw [hm₀, AddContent.supClosure_apply_finpartition hC _ PC, Finset.sup_set_eq_biUnion,
      measure_biUnion_finset P.disjoint (fun b hb ↦ hCmeas _ (PC hb))]
    apply (enorm_sum_le _ _).trans
    gcongr with t ht
    exact hm _ (PC ht)
-- 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
⊢ ∃ (P : Finpartition s), (↑(P.parts (a := s)) : Set (Set α)) ⊆ C

Tactic:
rw [hC.mem_supClosure_iff] at hs

Premises used: MeasureTheory.IsSetSemiring.mem_supClosure_iff