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
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
⊢ (↑m' : Set α → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u
have inr₁ : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v} (Ioc u v)
Tactic: rw [hm']
-- 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' : Set α → E) botSet = 0
have inr : ‖(↑m' : Set α → E) botSet‖ₑ = 0
Tactic: apply enorm_eq_zero.1
-- 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' : Set α → E) botSet‖ₑ = 0
have inr : ‖(↑m' : Set α → E) botSet‖ₑ ≤ ⊥
Tactic: apply le_bot_iff.1
-- 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
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
⊢ (↑hf.vectorMeasure : Set α → E) (Ioc a b) = Function.rightLim f b - Function.rightLim f a
have A : (↑(Exists.choose (p := fun (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)
          sorry) :
      Set α → E)
    (Ioc a b) =
  Function.rightLim f b - Function.rightLim f a
Tactic: have A : hf.exists_vectorMeasure_le_measureAux.choose (Ioc a b) =
      f.rightLim b - f.rightLim a :=
    hf.exists_vectorMeasure_le_measureAux.choose_spec.1 a b 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
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
A :
  (↑(Exists.choose (p := fun (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)
            ⋯) :
        Set α → E)
      (Ioc a b) =
    Function.rightLim f b - Function.rightLim f a
⊢ Eq.{u_2 + 1} (α := E)
    ((↑(if hx : ∃ (x : α), IsBot x then
            VectorMeasure.dirac (hx.choose (p := IsBot))
              (Function.rightLim f (hx.choose (p := IsBot)) - f (hx.choose (p := IsBot)))
          else 0) :
        Set α → E)
      (Ioc a b))
    0
have pos : ∀ (hx : ∃ (x : α), IsBot x),
  Eq.{u_2 + 1} (α := E)
    ((↑(if hx : ∃ (x : α), IsBot x then
            VectorMeasure.dirac (hx.choose (p := IsBot))
              (Function.rightLim f (hx.choose (p := IsBot)) - f (hx.choose (p := IsBot)))
          else 0) :
        Set α → E)
      (Ioc a b))
    0
Tactic: by_cases hx : ∃ (x : α), IsBot 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
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
A :
  (↑(Exists.choose (p := fun (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)
            ⋯) :
        Set α → E)
      (Ioc a b) =
    Function.rightLim f b - Function.rightLim f a
pos :
  ∀ (hx : ∃ (x : α), IsBot x),
    Eq.{u_2 + 1} (α := E)
      ((↑(if hx : ∃ (x : α), IsBot x then
              VectorMeasure.dirac (hx.choose (p := IsBot))
                (Function.rightLim f (hx.choose (p := IsBot)) - f (hx.choose (p := IsBot)))
            else 0) :
          Set α → E)
        (Ioc a b))
      0
⊢ Eq.{u_2 + 1} (α := E)
    ((↑(if hx : ∃ (x : α), IsBot x then
            VectorMeasure.dirac (hx.choose (p := IsBot))
              (Function.rightLim f (hx.choose (p := IsBot)) - f (hx.choose (p := IsBot)))
          else 0) :
        Set α → E)
      (Ioc a b))
    0
have neg : ∀ (hx : ¬∃ (x : α), IsBot x),
  Eq.{u_2 + 1} (α := E)
    ((↑(if hx : ∃ (x : α), IsBot x then
            VectorMeasure.dirac (hx.choose (p := IsBot))
              (Function.rightLim f (hx.choose (p := IsBot)) - f (hx.choose (p := IsBot)))
          else 0) :
        Set α → E)
      (Ioc a b))
    0
Tactic: by_cases hx : ∃ (x : α), IsBot 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
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
A :
  (↑(Exists.choose (p := fun (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)
            ⋯) :
        Set α → E)
      (Ioc a b) =
    Function.rightLim f b - Function.rightLim f a
hx : ∃ (x : α), IsBot x
⊢ Eq.{u_2 + 1} (α := E)
    ((↑(if hx : ∃ (x : α), IsBot x then
            VectorMeasure.dirac (hx.choose (p := IsBot))
              (Function.rightLim f (hx.choose (p := IsBot)) - f (hx.choose (p := IsBot)))
          else 0) :
        Set α → E)
      (Ioc a b))
    0
have pos : (↑(VectorMeasure.dirac (sorry.choose (p := IsBot))
          (Function.rightLim f (sorry.choose (p := IsBot)) - f (sorry.choose (p := IsBot)))) :
      Set α → E)
    (Ioc a b) =
  0
Tactic: simp only [hx, ↓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 : a ≤ b
A :
  (↑(Exists.choose (p := fun (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)
            ⋯) :
        Set α → E)
      (Ioc a b) =
    Function.rightLim f b - Function.rightLim f a
hx : ∃ (x : α), IsBot x
⊢ (↑(VectorMeasure.dirac (⋯.choose (p := IsBot))
            (Function.rightLim f (⋯.choose (p := IsBot)) - f (⋯.choose (p := IsBot)))) :
        Set α → E)
      (Ioc a b) =
    0
have pos : sorry.choose (p := IsBot) ∉ Ioc a b
Tactic: rw [VectorMeasure.dirac_apply_of_notMem]
-- 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 : a ≤ b
A :
  (↑(Exists.choose (p := fun (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)
            ⋯) :
        Set α → E)
      (Ioc a b) =
    Function.rightLim f b - Function.rightLim f a
hx : ∃ (x : α), IsBot x
⊢ ⋯.choose (p := IsBot) ∉ Ioc a b
have pos : sorry.choose (p := IsBot) ≤ a ∨ b < sorry.choose (p := IsBot)
Tactic: simp only [mem_Ioc, not_and_or, not_lt, not_le]
-- 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
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
A :
  (↑(Exists.choose (p := fun (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)
            ⋯) :
        Set α → E)
      (Ioc a b) =
    Function.rightLim f b - Function.rightLim f a
⊢ (↑hf.vectorMeasure : Set α → E) (Ioc a b) = Function.rightLim f b - Function.rightLim f a
have B : Eq.{u_2 + 1} (α := E)
  ((↑(if hx : ∃ (x : α), IsBot x then
          VectorMeasure.dirac (hx.choose (p := IsBot))
            (Function.rightLim f (hx.choose (p := IsBot)) - f (hx.choose (p := IsBot)))
        else 0) :
      Set α → E)
    (Ioc a b))
  0
Tactic: have B : (if hx : ∃ (x : α), IsBot x then VectorMeasure.dirac hx.choose
      (f.rightLim hx.choose - f hx.choose) else 0) (Ioc a b) = 0 := by
    by_cases hx : ∃ (x : α), IsBot x
    · simp only [hx, ↓reduceDIte]
      rw [VectorMeasure.dirac_apply_of_notMem]
      simp only [mem_Ioc, not_and_or, not_lt, not_le]
      exact Or.inl (hx.choose_spec _)
    · simp [hx]
-- 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 : a ≤ b
⊢ (↑hf.vectorMeasure : Set α → E) (Ioc a b) = Function.rightLim f b - Function.rightLim f a
have have : ∀
  (A :
    (↑(Exists.choose (p := fun (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)
              sorry) :
          Set α → E)
        (Ioc a b) =
      Function.rightLim f b - Function.rightLim f a),
  (↑hf.vectorMeasure : Set α → E) (Ioc a b) = Function.rightLim f b - Function.rightLim f a
Tactic: classical
  have A : hf.exists_vectorMeasure_le_measureAux.choose (Ioc a b) =
      f.rightLim b - f.rightLim a :=
    hf.exists_vectorMeasure_le_measureAux.choose_spec.1 a b h
  have B : (if hx : ∃ (x : α), IsBot x then VectorMeasure.dirac hx.choose
      (f.rightLim hx.choose - f hx.choose) else 0) (Ioc a b) = 0 := by
    by_cases hx : ∃ (x : α), IsBot x
    · simp only [hx, ↓reduceDIte]
      rw [VectorMeasure.dirac_apply_of_notMem]
      simp only [mem_Ioc, not_and_or, not_lt, not_le]
      exact Or.inl (hx.choose_spec _)
    · simp [hx]
  simp [vectorMeasure, A, B]
-- 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 : a ≤ b
have have₁ have₂ :
  ∀
    (A :
      (↑(Exists.choose (p := fun (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)
                ⋯) :
            Set α → E)
          (Ioc a b) =
        Function.rightLim f b - Function.rightLim f a),
    (↑hf.vectorMeasure : Set α → E) (Ioc a b) = Function.rightLim f b - Function.rightLim f a
⊢ (↑hf.vectorMeasure : Set α → E) (Ioc a b) = Function.rightLim f b - Function.rightLim f a
have have₃ : ∀
  (A :
    (↑(Exists.choose (p := fun (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)
              sorry) :
          Set α → E)
        (Ioc a b) =
      Function.rightLim f b - Function.rightLim f a)
  (B :
    Eq.{u_2 + 1} (α := E)
      ((↑(if hx : ∃ (x : α), IsBot x then
              VectorMeasure.dirac (hx.choose (p := IsBot))
                (Function.rightLim f (hx.choose (p := IsBot)) - f (hx.choose (p := IsBot)))
            else 0) :
          Set α → E)
        (Ioc a b))
      0),
  (↑hf.vectorMeasure : Set α → E) (Ioc a b) = Function.rightLim f b - Function.rightLim f a
Tactic: classical
  have A : hf.exists_vectorMeasure_le_measureAux.choose (Ioc a b) =
      f.rightLim b - f.rightLim a :=
    hf.exists_vectorMeasure_le_measureAux.choose_spec.1 a b h
  have B : (if hx : ∃ (x : α), IsBot x then VectorMeasure.dirac hx.choose
      (f.rightLim hx.choose - f hx.choose) else 0) (Ioc a b) = 0 := by
    by_cases hx : ∃ (x : α), IsBot x
    · simp only [hx, ↓reduceDIte]
      rw [VectorMeasure.dirac_apply_of_notMem]
      simp only [mem_Ioc, not_and_or, not_lt, not_le]
      exact Or.inl (hx.choose_spec _)
    · simp [hx]
  simp [vectorMeasure, A, B]
-- 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 : α
hf : BoundedVariationOn f univ
⊢ (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
have pos : ∀ (ha : IsBot a), (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
Tactic: by_cases ha : IsBot 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 α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
a : α
hf : BoundedVariationOn f univ
pos : ∀ (ha : IsBot a), (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
⊢ (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
have neg : ∀ (ha : ¬IsBot a), (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
Tactic: by_cases ha : IsBot a
-- 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
a : α
hf : BoundedVariationOn f univ
ha : IsBot a
⊢ (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
have h : ∃ (x : α), IsBot x
Tactic: have h : ∃ x, IsBot x := ⟨a, ha⟩
-- 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
a : α
hf : BoundedVariationOn f univ
ha : IsBot a
h : ∃ (x : α), IsBot x
⊢ (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
have heqa : h.choose (p := IsBot) = a
Tactic: have heqa : h.choose = a := subsingleton_isBot _ h.choose_spec ha
-- 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 : α
hf : BoundedVariationOn f univ
ha : IsBot a
h : ∃ (x : α), IsBot x
heqa : h.choose (p := IsBot) = a
⊢ (↑(Exists.choose (p := fun (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)
            ⋯) :
        Set α → E)
      {a} =
    0
have rw : (↑(Exists.choose (p := fun (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)
          sorry) :
      Set α → E)
    botSet =
  0
Tactic: rw [← botSet_eq_singleton_of_isBot ha]
-- 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
a : α
hf : BoundedVariationOn f univ
ha : IsBot a
h : ∃ (x : α), IsBot x
heqa : h.choose (p := IsBot) = a
⊢ (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
have A : (↑(Exists.choose (p := fun (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)
          sorry) :
      Set α → E)
    {a} =
  0
Tactic: have A : hf.exists_vectorMeasure_le_measureAux.choose {a} = 0 := by
      rw [← botSet_eq_singleton_of_isBot ha]
      exact hf.exists_vectorMeasure_le_measureAux.choose_spec.2.1
-- 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 : α
hf : BoundedVariationOn f univ
ha : IsBot a
h : ∃ (x : α), IsBot x
heqa : h.choose (p := IsBot) = a
A :
  (↑(Exists.choose (p := fun (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)
            ⋯) :
        Set α → E)
      {a} =
    0
⊢ (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
have pos : (↑(VectorMeasure.dirac (sorry.choose (p := fun (x : α) ↦ IsBot x))
          (Function.rightLim f (sorry.choose (p := fun (x : α) ↦ IsBot x)) - f (sorry.choose (p := fun (x : α) ↦ IsBot x)))) :
      Set α → E)
    {a} =
  Function.rightLim f a - Function.leftLim f a
Tactic: simp only [vectorMeasure, h, ↓reduceDIte, VectorMeasure.coe_add, Pi.add_apply, A,
      zero_add]