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
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
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
⊢ ∃ (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⟩

Premises used: MeasureTheory.Measure.exists_ae_subset_biUnion_countable
-- 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
M : ∀ (s : Set α) (hs : s ∈ C), MeasurableSet s
D : Set (Set α)
DC : D ⊆ C
D_count : D.Countable
hD : ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D
⊢ MeasurableSet (⋃₀ D)

Tactic:
have MD : MeasurableSet (⋃₀ D) := MeasurableSet.sUnion D_count (fun t ht ↦ M _ (DC 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
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∞)
apply₁ : ∀ (s : Set α) (hs : s ∈ C), 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

Tactic:
apply exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom_of_cover hC
      (fun s hs ↦ ?_) h'C ?_

Premises used: _private.0.MeasureTheory.VectorMeasure.exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom_of_cover
-- 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
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)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [μ', Measure.restrict_apply' MD]

Premises used: MeasureTheory.Measure.restrict_apply'
-- 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
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)
⊢ ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact ⟨D, D_count, DC, by simp [μ', Measure.restrict_apply' MD]⟩
-- 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
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
apply : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ' : (a : Set α) → ℝ≥0∞) s

Tactic:
apply (hm s hs).trans

Premises used: 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
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
simp : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ ⋃₀ D) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [Measure.restrict_apply' MD, μ']

Premises used: MeasureTheory.Measure.restrict_apply'
-- 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
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
H : s ≤ᶠ[ae μ] s ∩ ⋃₀ D
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ ⋃₀ D) : ℝ≥0∞)

Tactic:
apply measure_mono_ae

Premises used: MeasureTheory.measure_mono_ae
-- 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
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
H : s ∩ s ≤ᶠ[ae μ] s ∩ ⋃₀ D
⊢ s ≤ᶠ[ae μ] s ∩ ⋃₀ D

Tactic:
nth_rewrite 1 [← Set.inter_self s]

Premises used: Set.inter_self
-- 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
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 ∩ s ≤ᶠ[ae μ] s ∩ ⋃₀ D

Tactic:
ae_le_set_inter Filter.EventuallyLE.rfl (hD s hs)

Premises used: MeasureTheory.ae_le_set_inter, Filter.EventuallyLE.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 : 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 ∩ s ≤ᶠ[ae μ] s ∩ ⋃₀ D

Tactic:
exact ae_le_set_inter Filter.EventuallyLE.rfl (hD s hs)

Premises used: MeasureTheory.ae_le_set_inter, Filter.EventuallyLE.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 : 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)
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
⊢ ∃ (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)

Premises used: MeasureTheory.VectorMeasure
-- 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
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
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:
⟨m', h, fun s ↦ (h' s).trans (Measure.restrict_apply_le (⋃₀ D) s)⟩

Premises used: Set.sUnion, MeasureTheory.Measure.restrict_apply_le, And.intro, Exists.intro, 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
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
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:
exact ⟨m', h, fun s ↦ (h' s).trans (Measure.restrict_apply_le (⋃₀ D) s)⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
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₀ : α
rw : MonotoneOn (β := ℝ) (fun (x : α) ↦ variationOnFromTo (Function.rightLim f) univ x₀ x) univ
⊢ Monotone (β := ℝ) fun (x : α) ↦ variationOnFromTo (Function.rightLim f) univ x₀ x

Tactic:
rw [← monotoneOn_univ]

Premises used: monotoneOn_univ
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
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₀ : α
⊢ MonotoneOn (β := ℝ) (fun (x : α) ↦ variationOnFromTo (Function.rightLim f) univ x₀ x) univ

Tactic:
variationOnFromTo.monotoneOn hf.rightLim.locallyBoundedVariationOn (mem_univ _)

Premises used: BoundedVariationOn.locallyBoundedVariationOn, BoundedVariationOn.rightLim, variationOnFromTo.monotoneOn, Set.mem_univ
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
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₀ : α
⊢ MonotoneOn (β := ℝ) (fun (x : α) ↦ variationOnFromTo (Function.rightLim f) univ x₀ x) univ

Tactic:
exact variationOnFromTo.monotoneOn hf.rightLim.locallyBoundedVariationOn (mem_univ _)

Premises used: BoundedVariationOn.locallyBoundedVariationOn, BoundedVariationOn.rightLim, variationOnFromTo.monotoneOn, Set.mem_univ
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
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
pos : ∀ (h : Nonempty α), IsFiniteMeasure (m0 := hα) hf.measureAux
neg : ∀ (h : ¬Nonempty α), IsFiniteMeasure (m0 := hα) hf.measureAux
⊢ IsFiniteMeasure (m0 := hα) hf.measureAux

Tactic:
by_cases h : Nonempty α

Premises used: Nonempty
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
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
h : ¬Nonempty α
neg : IsFiniteMeasure.{u_1} (α := α) (m0 := hα) 0
⊢ IsFiniteMeasure (m0 := hα) hf.measureAux

Tactic:
simp only [BoundedVariationOn.measureAux, h, ↓reduceDIte]

Premises used: _private.0.BoundedVariationOn.measureAux, reduceDIte
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
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
h : ¬Nonempty α
⊢ IsFiniteMeasure.{u_1} (α := α) (m0 := hα) 0

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
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
h : Nonempty α
pos : IsFiniteMeasure (m0 := hα) (StieltjesFunction.measure (hf.stieltjesFunctionRightLim ⋯.some))
⊢ IsFiniteMeasure (m0 := hα) hf.measureAux

Tactic:
simp only [BoundedVariationOn.measureAux, h, ↓reduceDIte]

Premises used: _private.0.BoundedVariationOn.measureAux, reduceDIte
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
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
h : Nonempty α
apply :
  ∀ (x : α), |(↑(hf.stieltjesFunctionRightLim ⋯.some) : α → ℝ) x| ≤ (eVariationOn (Function.rightLim f) univ).toReal
⊢ IsFiniteMeasure (m0 := hα) (StieltjesFunction.measure (hf.stieltjesFunctionRightLim ⋯.some))

Tactic:
apply StieltjesFunction.isFiniteMeasure_of_forall_abs_le
    (C := (eVariationOn f.rightLim univ).toReal) _ (fun x ↦ ?_)

Premises used: StieltjesFunction.isFiniteMeasure_of_forall_abs_le
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
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
h : Nonempty α
x : α
⊢ |(↑(hf.stieltjesFunctionRightLim ⋯.some) : α → ℝ) x| ≤ (eVariationOn (Function.rightLim f) univ).toReal

Tactic:
variationOnFromTo.abs_le_eVariationOn hf.rightLim

Premises used: BoundedVariationOn.rightLim, variationOnFromTo.abs_le_eVariationOn, variationOnFromTo, ite
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
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
h : Nonempty α
x : α
⊢ |(↑(hf.stieltjesFunctionRightLim ⋯.some) : α → ℝ) x| ≤ (eVariationOn (Function.rightLim f) univ).toReal

Tactic:
exact variationOnFromTo.abs_le_eVariationOn hf.rightLim

Premises used: BoundedVariationOn.rightLim, variationOnFromTo.abs_le_eVariationOn
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
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
hf : BoundedVariationOn f univ
inl :
  ∀ (h'α : IsEmpty α),
    ∃ (m : VectorMeasure α E),
      (∀ (u v : α), u ≤ v → (↑m : Set α → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u) ∧
        (↑m : Set α → E) botSet = 0 ∧
          ∀ (s : Set α), ‖(↑m : Set α → E) s‖ₑ ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s
inr :
  ∀ (h'α : Nonempty α),
    ∃ (m : VectorMeasure α E),
      (∀ (u v : α), u ≤ v → (↑m : Set α → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u) ∧
        (↑m : Set α → E) botSet = 0 ∧
          ∀ (s : Set α), ‖(↑m : Set α → E) s‖ₑ ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s
⊢ ∃ (m : VectorMeasure α E),
    (∀ (u v : α), u ≤ v → (↑m : Set α → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u) ∧
      (↑m : Set α → E) botSet = 0 ∧
        ∀ (s : Set α), ‖(↑m : Set α → E) s‖ₑ ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s

Tactic:
rcases isEmpty_or_nonempty α with h'α | h'α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
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
hf : BoundedVariationOn f univ
h'α : IsEmpty α
⊢ (∀ (u v : α), u ≤ v → (↑0 : Set α → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u) ∧
    Eq.{u_2 + 1} (α := E) ((↑0 : Set α → E) botSet) 0 ∧
      ∀ (s : Set α), enorm.{u_2} (E := E) ((↑0 : Set α → E) s) ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
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
hf : BoundedVariationOn f univ
h'α : IsEmpty α
⊢ ∃ (m : VectorMeasure α E),
    (∀ (u v : α), u ≤ v → (↑m : Set α → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u) ∧
      (↑m : Set α → E) botSet = 0 ∧
        ∀ (s : Set α), ‖(↑m : Set α → E) s‖ₑ ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s

Tactic:
exact ⟨0, by simp⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
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
hf : BoundedVariationOn f univ
h'α : Nonempty α
m : AddContent.{u_1, u_2} (α := α) E {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v} :=
  AddContent.onIoc (Function.rightLim f)
u v : α
huv : u ≤ v
rw : ‖Function.rightLim f v - Function.rightLim f u‖ₑ ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) (Ioc u v)
⊢ enorm.{u_2} (E := E) ((m : (a : Set α) → E) (Ioc u v) : E) ≤
    ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) (Ioc u v)

Tactic:
rw [AddContent.onIoc_apply huv]

Premises used: MeasureTheory.AddContent.onIoc_apply