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 α
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
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hst : Disjoint s t
⊢ m' (s ∪ t) = m' s + m' t
have h'm : m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) (s ∪ t) sorry) =
  m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s sorry) +
    m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) t sorry)
Tactic: simp only [hs, ht, MeasurableSet.union, ↓reduceDIte, 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 α
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' ⋯ ⋯ ⋯
⊢ ∃ (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 refine_1 : ∀ (s : Set α) (hs : s ∈ C), (↑m'' : Set α → E) s = (m : (a : Set α) → E) s
Tactic: refine ⟨m'', fun s hs ↦ ?_, fun s ↦ ?_⟩
-- 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 α)
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' ⋯ ⋯ ⋯
refine_1 : ∀ (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
have refine_2 : ∀ (s : Set α), ‖(↑m'' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
Tactic: refine ⟨m'', fun s hs ↦ ?_, fun s ↦ ?_⟩
-- 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 α)
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'' : Set α → E) s = (m : (a : Set α) → E) s
have refine_1 : m' s = (m : (a : Set α) → E) s
Tactic: change m' s = m s
-- 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 α)
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' s = (m : (a : Set α) → E) s
have refine_1 : m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s sorry) = (m : (a : Set α) → E) s
Tactic: simp only [hCmeas s hs, ↓reduceDIte, 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 α
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 α
⊢ ‖(↑m'' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
have refine_2 : ‖m' s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
Tactic: change ‖m' s‖ₑ ≤ μ s
-- 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 α)
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 α
⊢ ‖m' s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
have pos : ∀ (hs : MeasurableSet s), ‖m' s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
Tactic: by_cases hs : MeasurableSet s
-- 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 α)
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
⊢ ‖m' s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
have neg : ∀ (hs : ¬MeasurableSet s), ‖m' s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
Tactic: by_cases hs : MeasurableSet s
-- 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 α)
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
have pos : ‖m₁ (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s sorry)‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
Tactic: simp only [hs, ↓reduceDIte, m']
-- 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 : 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' : VectorMeasure α E),
    (∀ s ∈ C, (↑m' : Set α → E) s = (m : (a : Set α) → E) s) ∧
      ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
have hm₀ : 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₀
-- 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 : 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
have hs₁ : ∃ (P : Finpartition s), (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
Tactic: rw [hC.mem_supClosure_iff] at hs
Cleared hypotheses: 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 : 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
⊢ enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
have 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
Tactic: rcases hs with ⟨P, PC⟩
Cleared hypotheses: 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 : 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
⊢ enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
have nth_rewrite : enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) (P.parts (a := s).sup id)
Tactic: nth_rewrite 2 [← P.sup_parts]
-- 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 : 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
⊢ enorm.{u_2} (E := E) ((m₀ : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) (P.parts (a := s).sup id)
have 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)
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))]
-- 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 : 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
⊢ 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)
have 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))
Tactic: apply (enorm_sum_le _ _).trans
-- 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 : 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
⊢ 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))
have 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)
Tactic: gcongr with t ht
-- 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 : 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
⊢ ∃ (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 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
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)