awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ IsFiniteMeasure (m0 := hα) hf.measureAux
have pos : ∀ (h : Nonempty α), IsFiniteMeasure (m0 := hα) hf.measureAux
Tactic: by_cases h : Nonempty α
-- 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
pos : ∀ (h : Nonempty α), IsFiniteMeasure (m0 := hα) hf.measureAux
⊢ IsFiniteMeasure (m0 := hα) hf.measureAux
have neg : ∀ (h : ¬Nonempty α), IsFiniteMeasure (m0 := hα) hf.measureAux
Tactic: by_cases h : Nonempty α
-- 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
h : ¬Nonempty α
⊢ IsFiniteMeasure (m0 := hα) hf.measureAux
have neg : IsFiniteMeasure.{u_1} (α := α) (m0 := hα) 0
Tactic: simp only [BoundedVariationOn.measureAux, h, ↓reduceDIte]
-- 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
h : Nonempty α
⊢ IsFiniteMeasure (m0 := hα) hf.measureAux
have pos : IsFiniteMeasure (m0 := hα) (StieltjesFunction.measure (hf.stieltjesFunctionRightLim sorry.some))
Tactic: simp only [BoundedVariationOn.measureAux, h, ↓reduceDIte]
-- 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
h : Nonempty α
⊢ IsFiniteMeasure (m0 := hα) (StieltjesFunction.measure (hf.stieltjesFunctionRightLim ⋯.some))
have apply : ∀ (x : α), |(↑(hf.stieltjesFunctionRightLim sorry.some) : α → ℝ) x| ≤ (eVariationOn (Function.rightLim f) univ).toReal
Tactic: apply StieltjesFunction.isFiniteMeasure_of_forall_abs_le
    (C := (eVariationOn f.rightLim univ).toReal) _ (fun x ↦ ?_)
-- 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
hf : BoundedVariationOn f univ
⊢ ∃ (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
have 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
Tactic: rcases isEmpty_or_nonempty α with h'α | h'α
-- 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
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
⊢ ∃ (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
have 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
Tactic: rcases isEmpty_or_nonempty α with h'α | h'α
-- 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
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
⊢ enorm.{u_2} (E := E) ((m : (a : Set α) → E) (Ioc u v) : E) ≤
    ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) (Ioc u v)
have rw : ‖Function.rightLim f v - Function.rightLim f u‖ₑ ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) (Ioc u v)
Tactic: rw [AddContent.onIoc_apply huv]
-- 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
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
⊢ ‖Function.rightLim f v - Function.rightLim f u‖ₑ ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) (Ioc u v)
have simp : ‖Function.rightLim f v - Function.rightLim f u‖ₑ ≤
  ENNReal.ofReal
    (variationOnFromTo (Function.rightLim f) univ sorry.some v - variationOnFromTo (Function.rightLim f) univ sorry.some u)
Tactic: simp only [BoundedVariationOn.measureAux, h'α, ↓reduceDIte, StieltjesFunction.measure_Ioc,
      BoundedVariationOn.stieltjesFunctionRightLim_apply]
-- 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
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
⊢ ‖Function.rightLim f v - Function.rightLim f u‖ₑ ≤
    ENNReal.ofReal
      (variationOnFromTo (Function.rightLim f) univ ⋯.some v - variationOnFromTo (Function.rightLim f) univ ⋯.some u)
have rw : ‖Function.rightLim f v - Function.rightLim f u‖ₑ ≤
  ENNReal.ofReal
    (variationOnFromTo (Function.rightLim f) univ h'α.some u + variationOnFromTo (Function.rightLim f) univ u v -
      variationOnFromTo (Function.rightLim f) univ sorry.some u)
Tactic: rw [← variationOnFromTo.add hf.rightLim.locallyBoundedVariationOn
      (mem_univ h'α.some) (mem_univ u) (mem_univ v)]
-- 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
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
⊢ ‖Function.rightLim f v - Function.rightLim f u‖ₑ ≤
    ENNReal.ofReal
      (variationOnFromTo (Function.rightLim f) univ h'α.some u + variationOnFromTo (Function.rightLim f) univ u v -
        variationOnFromTo (Function.rightLim f) univ ⋯.some u)
have simp : ‖Function.rightLim f v - Function.rightLim f u‖ₑ ≤ ENNReal.ofReal (eVariationOn (Function.rightLim f) (Icc u v)).toReal
Tactic: simp only [add_sub_cancel_left, variationOnFromTo, huv, ↓reduceIte, univ_inter]
-- 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
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
⊢ ‖Function.rightLim f v - Function.rightLim f u‖ₑ ≤
    ENNReal.ofReal (eVariationOn (Function.rightLim f) (Icc u v)).toReal
have rw : ‖Function.rightLim f v - Function.rightLim f u‖ₑ ≤ eVariationOn (Function.rightLim f) (Icc u v)
Tactic: rw [ENNReal.ofReal_toReal]
-- 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
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‖ₑ ≤ eVariationOn (Function.rightLim f) (Icc u v)
⊢ ‖Function.rightLim f v - Function.rightLim f u‖ₑ ≤
    ENNReal.ofReal (eVariationOn (Function.rightLim f) (Icc u v)).toReal
have rw₁ : eVariationOn (Function.rightLim f) (Icc u v) ≠ ∞
Tactic: rw [ENNReal.ofReal_toReal]
-- 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
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
⊢ ‖Function.rightLim f v - Function.rightLim f u‖ₑ ≤ eVariationOn (Function.rightLim f) (Icc u v)
have rw : edist (Function.rightLim f v) (Function.rightLim f u) ≤ eVariationOn (Function.rightLim f) (Icc u v)
Tactic: rw [← edist_eq_enorm_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (hypothesis)
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)
⊢ ∃ (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
have A : ∀ (s : Set α),
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v} s →
    enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s
Tactic: have A : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, ‖m s‖ₑ ≤ hf.measureAux s := by
    rintro s ⟨u, v, huv, rfl⟩
    rw [AddContent.onIoc_apply huv]
    simp only [BoundedVariationOn.measureAux, h'α, ↓reduceDIte, StieltjesFunction.measure_Ioc,
      BoundedVariationOn.stieltjesFunctionRightLim_apply]
    rw [← variationOnFromTo.add hf.rightLim.locallyBoundedVariationOn
      (mem_univ h'α.some) (mem_univ u) (mem_univ v)]
    simp only [add_sub_cancel_left, variationOnFromTo, huv, ↓reduceIte, univ_inter]
    rw [ENNReal.ofReal_toReal]; swap
    · exact ((eVariationOn.mono _ (subset_univ _)).trans_lt hf.rightLim.lt_top).ne
    rw [← edist_eq_enorm_sub]
    exact eVariationOn.edist_le _ (by grind) (by grind)
-- 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
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)
A :
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v} s →
      enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s
⊢ hα = generateFrom {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v}
have borelize : ∀ [inst_9 : BorelSpace α]
  (A :
    ∀ (s : Set α),
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v} s →
        enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s),
  borel α = generateFrom {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v}
Tactic: borelize α
Cleared hypotheses: hα, inst_6, A
-- 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 α
E : Type u_2
inst_6 : NormedAddCommGroup E
inst_7 : 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)
inst_8 : BorelSpace α
A :
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v} s →
      enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s
this : MeasurableSpace α := borel α
⊢ borel α = generateFrom {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v}
have h : Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v}
  {S : Set α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S}
Tactic: convert! borel_eq_generateFrom_Ioc_le α using 2
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (hypothesis)
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)
A :
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v} s →
      enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ ((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
have B : hα = generateFrom {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v}
Tactic: have B : hα = generateFrom {s | ∃ u v, u ≤ v ∧ s = Ioc u v} := by
    borelize α
    convert! borel_eq_generateFrom_Ioc_le α using 2
    grind only
-- 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
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)
A :
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v} s →
      enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s
B : hα = generateFrom {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v}
⊢ ∃ (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
have inr : ∀ (m' : VectorMeasure α E)
  (hm' :
    ∀ (s : Set α),
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v} s →
        (↑m' : Set α → E) s = (m : (a : Set α) → E) s)
  (h'm' : ∀ (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 VectorMeasure.exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom
    IsSetSemiring.Ioc A B with ⟨m', hm', h'm'⟩
-- 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
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)
A :
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v} s →
      enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s
B : hα = generateFrom {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v}
m' : VectorMeasure α E
hm' :
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v} s →
      (↑m' : Set α → E) s = (m : (a : Set α) → E) s
h'm' : ∀ (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
have inr : ∀ (u v : α) (huv : u ≤ v), (↑m' : Set α → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u
Tactic: refine ⟨m', fun u v huv ↦ ?_, ?_, h'm'⟩
-- 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
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)
A :
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v} s →
      enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s
B : hα = generateFrom {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v}
m' : VectorMeasure α E
hm' :
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v} s →
      (↑m' : Set α → E) s = (m : (a : Set α) → E) s
h'm' : ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s
inr : ∀ (u v : α) (huv : u ≤ v), (↑m' : Set α → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u
⊢ ∃ (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
have inr₁ : (↑m' : Set α → E) botSet = 0
Tactic: refine ⟨m', fun u v huv ↦ ?_, ?_, h'm'⟩
-- 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
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)
A :
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v} s →
      enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s
B : hα = generateFrom {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v}
m' : VectorMeasure α E
hm' :
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v} s →
      (↑m' : Set α → E) s = (m : (a : Set α) → E) s
h'm' : ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s
u v : α
huv : u ≤ v
⊢ (↑m' : Set α → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u
have inr : (m : (a : Set α) → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u
Tactic: rw [hm']