awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
simp :
  ‖Function.rightLim f v - Function.rightLim f u‖ₑ ≤
    ENNReal.ofReal
      (variationOnFromTo (Function.rightLim f) univ ⋯.some v - variationOnFromTo (Function.rightLim f) univ ⋯.some u)
⊢ ‖Function.rightLim f v - Function.rightLim f u‖ₑ ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) (Ioc u v)

Tactic:
simp only [BoundedVariationOn.measureAux, h'α, ↓reduceDIte, StieltjesFunction.measure_Ioc,
      BoundedVariationOn.stieltjesFunctionRightLim_apply]

Premises used: _private.0.BoundedVariationOn.measureAux, reduceDIte, BoundedVariationOn.stieltjesFunctionRightLim_apply, StieltjesFunction.measure_Ioc
-- 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‖ₑ ≤
    ENNReal.ofReal
      (variationOnFromTo (Function.rightLim f) univ h'α.some u + variationOnFromTo (Function.rightLim f) univ u v -
        variationOnFromTo (Function.rightLim f) univ ⋯.some u)
⊢ ‖Function.rightLim f v - Function.rightLim f u‖ₑ ≤
    ENNReal.ofReal
      (variationOnFromTo (Function.rightLim f) univ ⋯.some v - variationOnFromTo (Function.rightLim f) univ ⋯.some u)

Tactic:
rw [← variationOnFromTo.add hf.rightLim.locallyBoundedVariationOn
      (mem_univ h'α.some) (mem_univ u) (mem_univ v)]

Premises used: Nonempty.some, BoundedVariationOn.locallyBoundedVariationOn, variationOnFromTo.add, BoundedVariationOn.rightLim, 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
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
simp :
  ‖Function.rightLim f v - Function.rightLim f u‖ₑ ≤
    ENNReal.ofReal (eVariationOn (Function.rightLim f) (Icc u v)).toReal
⊢ ‖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)

Tactic:
simp only [add_sub_cancel_left, variationOnFromTo, huv, ↓reduceIte, univ_inter]

Premises used: add_sub_cancel_left, Set.univ_inter, variationOnFromTo, reduceIte
-- 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‖ₑ ≤ eVariationOn (Function.rightLim f) (Icc u v)
rw₁ : 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

Tactic:
rw [ENNReal.ofReal_toReal]

Premises used: ENNReal.ofReal_toReal
-- 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
⊢ eVariationOn (Function.rightLim f) (Icc u v) ≠ ∞

Tactic:
((eVariationOn.mono _ (subset_univ _)).trans_lt hf.rightLim.lt_top).ne

Premises used: Set.subset_univ, Ne.lt_top, eVariationOn.mono, BoundedVariationOn.rightLim, LE.le.trans_lt, LT.lt.ne
-- 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
⊢ eVariationOn (Function.rightLim f) (Icc u v) ≠ ∞

Tactic:
exact ((eVariationOn.mono _ (subset_univ _)).trans_lt hf.rightLim.lt_top).ne

Premises used: Set.subset_univ, Ne.lt_top, eVariationOn.mono, BoundedVariationOn.rightLim, LE.le.trans_lt, LT.lt.ne
-- 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 : edist (Function.rightLim f v) (Function.rightLim f u) ≤ eVariationOn (Function.rightLim f) (Icc u v)
⊢ ‖Function.rightLim f v - Function.rightLim f u‖ₑ ≤ eVariationOn (Function.rightLim f) (Icc u v)

Tactic:
rw [← edist_eq_enorm_sub]

Premises used: edist_eq_enorm_sub
-- 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
⊢ v ∈ Icc u v

Tactic:
grind
-- 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
⊢ u ∈ Icc u v

Tactic:
grind
-- 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
⊢ edist (Function.rightLim f v) (Function.rightLim f u) ≤ eVariationOn (Function.rightLim f) (Icc u v)

Tactic:
exact eVariationOn.edist_le _ (by grind) (by grind)

Premises used: eVariationOn.edist_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
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)
⊢ ∀ (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)
-- 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)
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
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}
⊢ hα = generateFrom {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v}

Tactic:
borelize α
-- 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 α
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 α | ∃ (l : α) (u : α), l ≤ u ∧ Ioc l u = S}

Tactic:
borel_eq_generateFrom_Ioc_le α

Premises used: borel_eq_generateFrom_Ioc_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 α
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 α
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}
⊢ borel α = generateFrom {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v}

Tactic:
convert! borel_eq_generateFrom_Ioc_le α using 2

Premises used: borel_eq_generateFrom_Ioc_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 α
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 α
⊢ 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:
grind only
-- 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)
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}

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

Premises used: MeasureTheory.VectorMeasure.exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom, MeasureTheory.IsSetSemiring.Ioc
-- 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)
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

Tactic:
⟨m', fun u v huv ↦ ?_, ?_, h'm'⟩

Premises used: And.intro, Exists.intro
-- 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)
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
inr₁ : (↑m' : Set α → E) botSet = 0
⊢ ∃ (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:
refine ⟨m', fun u v huv ↦ ?_, ?_, h'm'⟩
-- 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)
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
inr : (m : (a : Set α) → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u
inr₁ : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v} (Ioc u v)
⊢ (↑m' : Set α → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u

Tactic:
rw [hm']
-- 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)
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 : (a : Set α) → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u

Tactic:
AddContent.onIoc_apply huv

Premises used: MeasureTheory.AddContent.onIoc_apply