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)
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:
exact AddContent.onIoc_apply huv

Premises used: MeasureTheory.AddContent.onIoc_apply
-- 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
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v} (Ioc u v)

Tactic:
⟨u, v, huv, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, rfl
-- 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
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Ioc u v} (Ioc u v)

Tactic:
exact ⟨u, v, huv, rfl⟩
-- 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 : ‖(↑m' : Set α → E) botSet‖ₑ = 0
⊢ (↑m' : Set α → E) botSet = 0

Tactic:
apply enorm_eq_zero.1

Premises used: Iff.mp, enorm_eq_zero
-- 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 : ‖(↑m' : Set α → E) botSet‖ₑ ≤ ⊥
⊢ ‖(↑m' : Set α → E) botSet‖ₑ = 0

Tactic:
apply le_bot_iff.1

Premises used: le_bot_iff, Iff.mp
-- 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
⊢ LE.le (α := ℝ≥0∞) (((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) botSet : ℝ≥0∞) (⊥ : ℝ≥0∞)

Tactic:
simp [measureAux, h'α]

Premises used: _private.0.BoundedVariationOn.measureAux
-- 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' : Set α → E) botSet‖ₑ ≤ ⊥

Tactic:
exact (h'm' _).trans (by simp [measureAux, h'α])

Premises used: LE.le.trans
-- 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 : a ≤ b
⊢ (↑(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

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
-- 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 : 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
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
⊢ 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
-- 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 : 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
pos :
  (↑(VectorMeasure.dirac (⋯.choose (p := IsBot))
            (Function.rightLim f (⋯.choose (p := IsBot)) - f (⋯.choose (p := IsBot)))) :
        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

Tactic:
simp only [hx, ↓reduceDIte]

Premises used: 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 : 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
pos : ⋯.choose (p := IsBot) ∉ Ioc a b
⊢ (↑(VectorMeasure.dirac (⋯.choose (p := IsBot))
            (Function.rightLim f (⋯.choose (p := IsBot)) - f (⋯.choose (p := IsBot)))) :
        Set α → E)
      (Ioc a b) =
    0

Tactic:
rw [VectorMeasure.dirac_apply_of_notMem]

Premises used: MeasureTheory.VectorMeasure.dirac_apply_of_notMem
-- 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 : 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
pos : ⋯.choose (p := IsBot) ≤ a ∨ b < ⋯.choose (p := IsBot)
⊢ ⋯.choose (p := IsBot) ∉ Ioc a b

Tactic:
simp only [mem_Ioc, not_and_or, not_lt, not_le]

Premises used: not_le, not_lt, not_and_or, Set.mem_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
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) ≤ a ∨ b < ⋯.choose (p := IsBot)

Tactic:
Or.inl (hx.choose_spec _)

Premises used: Exists.choose_spec, Or.inl
-- 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 : 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) ≤ a ∨ b < ⋯.choose (p := IsBot)

Tactic:
exact Or.inl (hx.choose_spec _)

Premises used: Exists.choose_spec, Or.inl
-- 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 : 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

Tactic:
simp [hx]
-- 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 : 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

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]
-- 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 : 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
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:
simp [vectorMeasure, A, B]

Premises used: BoundedVariationOn.vectorMeasure
-- 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 : 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
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)
    (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
⊢ (↑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]

Premises used: BoundedVariationOn.vectorMeasure