awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
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
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
⊢ MeasurableSet s
have rcases : ∀ (P : Finpartition s) (PC : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C), MeasurableSet 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
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 s
have rw : MeasurableSet.{u_1} (α := α) (⋃ x ∈ P.parts (a := s), id x)
Tactic: rw [← P.sup_parts, Finset.sup_set_eq_biUnion]
-- 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
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
⊢ ∃ (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 B : ∀ (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))
-- 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
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),
    (∀ s ∈ C, (↑m' : Set α → E) s = (m : (a : Set α) → E) s) ∧
      ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
have 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
Tactic: rcases VectorMeasure.exists_extension_of_isSetRing_of_le_measure_of_dense
    hC.isSetRing_supClosure B A h'C with ⟨m', hm', m'bound⟩
-- 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
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
have refine : ∀ (s : Set α) (hs : s ∈ C), (↑m' : Set α → E) s = (m : (a : Set α) → E) s
Tactic: refine ⟨m', fun s hs ↦ ?_, m'bound⟩
-- 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
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
⊢ (↑m' : Set α → E) s = (m : (a : Set α) → E) s
have rw : Eq.{u_2 + 1} (α := E) ((m₀ : (a : Set α) → E) s : E) ((m : (a : Set α) → E) s : E)
Tactic: rw [hm' _ (subset_supClosure 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
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∞)
⊢ ∃ (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 apply : ∀ s ∈ C, MeasurableSet s
Tactic: apply VectorMeasure.exists_extension_of_isSetSemiring_of_le_measure_of_dense hC ?_ hm ?_
-- 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
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
⊢ ∃ (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 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) < ε
Tactic: apply VectorMeasure.exists_extension_of_isSetSemiring_of_le_measure_of_dense hC ?_ hm ?_
-- 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
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
have rw : MeasurableSet s
Tactic: rw [h'C]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
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
have rw : MeasurableSet s
Tactic: rw [h'C]
-- 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
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : hα = generateFrom C
⊢ ∃ (m' : VectorMeasure α E),
    (∀ s ∈ C, (↑m' : Set α → E) s = (m : (a : Set α) → E) s) ∧
      ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
have M : ∀ (s : Set α) (hs : s ∈ C), MeasurableSet s
Tactic: have M (s) (hs : s ∈ C) : MeasurableSet s := by
    rw [h'C]; exact measurableSet_generateFrom 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
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : hα = generateFrom C
M : ∀ (s : Set α) (hs : s ∈ C), MeasurableSet 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 rcases : ∀ (D : Set (Set α)) (DC : D ⊆ C) (D_count : D.Countable) (hD : ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D),
  ∃ (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 Measure.exists_ae_subset_biUnion_countable μ M with ⟨D, DC, D_count, hD⟩
-- 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
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : hα = generateFrom C
M : ∀ (s : Set α) (hs : s ∈ C), MeasurableSet s
D : Set (Set α)
DC : D ⊆ C
D_count : D.Countable
hD : ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D
⊢ ∃ (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 MD : MeasurableSet (⋃₀ D)
Tactic: have MD : MeasurableSet (⋃₀ D) := MeasurableSet.sUnion D_count (fun t ht ↦ M _ (DC ht))
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : 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
M : ∀ (s : Set α) (hs : s ∈ C), MeasurableSet s
D : Set (Set α)
DC : D ⊆ C
D_count : D.Countable
hD : ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D
MD : MeasurableSet (⋃₀ D)
μ' : Measure α := μ.restrict (⋃₀ D)
⊢ ∃ (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 apply : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom_of_cover hC
      (fun s hs ↦ ?_) h'C ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
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
M : ∀ (s : Set α) (hs : s ∈ C), MeasurableSet s
D : Set (Set α)
DC : D ⊆ C
D_count : D.Countable
hD : ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D
MD : MeasurableSet (⋃₀ D)
μ' : Measure α := μ.restrict (⋃₀ D)
apply : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (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 apply₁ : ∀ (s : Set α) (hs : s ∈ C), enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ' : (a : Set α) → ℝ≥0∞) s
Tactic: apply exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom_of_cover hC
      (fun s hs ↦ ?_) h'C ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
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
M : ∀ (s : Set α) (hs : s ∈ C), MeasurableSet s
D : Set (Set α)
DC : D ⊆ C
D_count : D.Countable
hD : ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D
MD : MeasurableSet (⋃₀ D)
μ' : Measure α := μ.restrict (⋃₀ D)
s : Set α
hs : s ∈ C
⊢ enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ' : (a : Set α) → ℝ≥0∞) s
have apply : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: apply (hm s hs).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
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : hα = generateFrom C
M : ∀ (s : Set α) (hs : s ∈ C), MeasurableSet s
D : Set (Set α)
DC : D ⊆ C
D_count : D.Countable
hD : ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D
MD : MeasurableSet (⋃₀ D)
μ' : Measure α := μ.restrict (⋃₀ D)
s : Set α
hs : s ∈ C
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have simp : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ ⋃₀ D) : ℝ≥0∞)
Tactic: simp only [Measure.restrict_apply' MD, μ']
-- 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
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : hα = generateFrom C
M : ∀ (s : Set α) (hs : s ∈ C), MeasurableSet s
D : Set (Set α)
DC : D ⊆ C
D_count : D.Countable
hD : ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D
MD : MeasurableSet (⋃₀ D)
μ' : Measure α := μ.restrict (⋃₀ D)
s : Set α
hs : s ∈ C
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ ⋃₀ D) : ℝ≥0∞)
have H : s ≤ᶠ[ae μ] s ∩ ⋃₀ D
Tactic: apply measure_mono_ae
-- 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
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : hα = generateFrom C
M : ∀ (s : Set α) (hs : s ∈ C), MeasurableSet s
D : Set (Set α)
DC : D ⊆ C
D_count : D.Countable
hD : ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D
MD : MeasurableSet (⋃₀ D)
μ' : Measure α := μ.restrict (⋃₀ D)
s : Set α
hs : s ∈ C
⊢ s ≤ᶠ[ae μ] s ∩ ⋃₀ D
have H : s ∩ s ≤ᶠ[ae μ] s ∩ ⋃₀ D
Tactic: nth_rewrite 1 [← Set.inter_self 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 : 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
M : ∀ (s : Set α) (hs : s ∈ C), MeasurableSet s
D : Set (Set α)
DC : D ⊆ C
D_count : D.Countable
hD : ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D
MD : MeasurableSet (⋃₀ D)
μ' : Measure α := μ.restrict (⋃₀ D)
⊢ ∃ (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 obtain : ∀ (m' : VectorMeasure α E) (h : ∀ s ∈ C, (↑m' : Set α → E) s = (m : (a : Set α) → E) s)
  (h' : ∀ (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: obtain ⟨m', h, h'⟩ : ∃ m' : VectorMeasure α E, (∀ s ∈ C, m' s = m s) ∧ ∀ s, ‖m' s‖ₑ ≤ μ' s := by
    apply exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom_of_cover hC
      (fun s hs ↦ ?_) h'C ?_
    · exact ⟨D, D_count, DC, by simp [μ', Measure.restrict_apply' MD]⟩
    · apply (hm s hs).trans
      simp only [Measure.restrict_apply' MD, μ']
      apply measure_mono_ae
      nth_rewrite 1 [← Set.inter_self s]
      exact ae_le_set_inter Filter.EventuallyLE.rfl (hD s hs)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
x₀ : α
⊢ Monotone (β := ℝ) fun (x : α) ↦ variationOnFromTo (Function.rightLim f) univ x₀ x
have rw : MonotoneOn (β := ℝ) (fun (x : α) ↦ variationOnFromTo (Function.rightLim f) univ x₀ x) univ
Tactic: rw [← monotoneOn_univ]