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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
L1 :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop (𝓝 ((↑hf.vectorMeasure : Set α → E) {a}))
simp_rw :
  Tendsto (fun (n : ℕ) ↦ Function.rightLim f a - Function.rightLim f (u n)) atTop
    (𝓝 (Function.rightLim f a - Function.leftLim f a))
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop
    (𝓝 (Function.rightLim f a - Function.leftLim f a))

Tactic:
simp_rw [hf.vectorMeasure_Ioc (u_lt_a _).le]

Premises used: LT.lt.le, BoundedVariationOn.vectorMeasure_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 : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
L1 :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop (𝓝 ((↑hf.vectorMeasure : Set α → E) {a}))
apply : Tendsto (fun (x : ℕ) ↦ Function.rightLim f (u x)) atTop (𝓝 (Function.leftLim f a))
⊢ Tendsto (fun (n : ℕ) ↦ Function.rightLim f a - Function.rightLim f (u n)) atTop
    (𝓝 (Function.rightLim f a - Function.leftLim f a))

Tactic:
apply tendsto_const_nhds.sub

Premises used: tendsto_const_nhds, Filter.Tendsto.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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
L1 :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop (𝓝 ((↑hf.vectorMeasure : Set α → E) {a}))
⊢ Tendsto u atTop (𝓝[<] a)

Tactic:
have : Tendsto u atTop (𝓝[<] a) := tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
      u_lim (Eventually.of_forall u_lt_a)
-- 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 : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
L1 :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop (𝓝 ((↑hf.vectorMeasure : Set α → E) {a}))
this : Tendsto u atTop (𝓝[<] a)
⊢ Tendsto (Function.rightLim f ∘ u) atTop (𝓝 (Function.leftLim (Function.rightLim f) a))

Tactic:
(hf.rightLim.tendsto_leftLim a).comp this

Premises used: BoundedVariationOn.tendsto_leftLim, BoundedVariationOn.rightLim, Filter.Tendsto.comp
-- 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 : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
L1 :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop (𝓝 ((↑hf.vectorMeasure : Set α → E) {a}))
this : Tendsto u atTop (𝓝[<] a)
h : Function.leftLim f a = Function.leftLim (Function.rightLim f) a
⊢ Tendsto (fun (x : ℕ) ↦ Function.rightLim f (u x)) atTop (𝓝 (Function.leftLim f a))

Tactic:
convert! (hf.rightLim.tendsto_leftLim a).comp this using 2

Premises used: BoundedVariationOn.tendsto_leftLim, BoundedVariationOn.rightLim, Filter.Tendsto.comp
-- 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 : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
L1 :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop (𝓝 ((↑hf.vectorMeasure : Set α → E) {a}))
this : Tendsto u atTop (𝓝[<] a)
rw : a ∈ Iic a
⊢ (𝓝[<] a).NeBot

Tactic:
rw [← mem_closure_iff_nhdsWithin_neBot, closure_Iio' ⟨b, hb⟩]

Premises used: closure_Iio', mem_closure_iff_nhdsWithin_neBot, 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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
L1 :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop (𝓝 ((↑hf.vectorMeasure : Set α → E) {a}))
this : Tendsto u atTop (𝓝[<] a)
⊢ a ∈ Iic a

Tactic:
self_mem_Iic

Premises used: Set.self_mem_Iic
-- 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 : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
L1 :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop (𝓝 ((↑hf.vectorMeasure : Set α → E) {a}))
this : Tendsto u atTop (𝓝[<] a)
⊢ a ∈ Iic a

Tactic:
exact self_mem_Iic

Premises used: Set.self_mem_Iic
-- 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 : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
L1 :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop (𝓝 ((↑hf.vectorMeasure : Set α → E) {a}))
this : Tendsto u atTop (𝓝[<] a)
⊢ (𝓝[<] a).NeBot

Tactic:
have : (𝓝[<] a).NeBot := by
      rw [← mem_closure_iff_nhdsWithin_neBot, closure_Iio' ⟨b, hb⟩]
      exact self_mem_Iic
-- 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 : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
L1 :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop (𝓝 ((↑hf.vectorMeasure : Set α → E) {a}))
this_1 : Tendsto u atTop (𝓝[<] a)
this : (𝓝[<] a).NeBot
⊢ Function.leftLim f a = Function.leftLim (Function.rightLim f) a

Tactic:
(leftLim_rightLim (hf.tendsto_leftLim _)).symm

Premises used: BoundedVariationOn.tendsto_leftLim, leftLim_rightLim, Eq.symm
-- 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 : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
L1 :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop (𝓝 ((↑hf.vectorMeasure : Set α → E) {a}))
this_1 : Tendsto u atTop (𝓝[<] a)
this : (𝓝[<] a).NeBot
⊢ Function.leftLim f a = Function.leftLim (Function.rightLim f) a

Tactic:
exact (leftLim_rightLim (hf.tendsto_leftLim _)).symm

Premises used: BoundedVariationOn.tendsto_leftLim, leftLim_rightLim, Eq.symm
-- 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 : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
L1 :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop (𝓝 ((↑hf.vectorMeasure : Set α → E) {a}))
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop
    (𝓝 (Function.rightLim f a - Function.leftLim f a))

Tactic:
have L2 : Tendsto (fun n ↦ hf.vectorMeasure (Ioc (u n) a)) atTop
      (𝓝 (f.rightLim a - f.leftLim a)) := by
    simp_rw [hf.vectorMeasure_Ioc (u_lt_a _).le]
    apply tendsto_const_nhds.sub
    have : Tendsto u atTop (𝓝[<] a) := tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
      u_lim (Eventually.of_forall u_lt_a)
    convert! (hf.rightLim.tendsto_leftLim a).comp this using 2
    have : (𝓝[<] a).NeBot := by
      rw [← mem_closure_iff_nhdsWithin_neBot, closure_Iio' ⟨b, hb⟩]
      exact self_mem_Iic
    exact (leftLim_rightLim (hf.tendsto_leftLim _)).symm
-- 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 : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
L1 :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop (𝓝 ((↑hf.vectorMeasure : Set α → E) {a}))
L2 :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop
    (𝓝 (Function.rightLim f a - Function.leftLim f a))
⊢ (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a

Tactic:
tendsto_nhds_unique L1 L2

Premises used: tendsto_nhds_unique
-- 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 : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
L1 :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop (𝓝 ((↑hf.vectorMeasure : Set α → E) {a}))
L2 :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop
    (𝓝 (Function.rightLim f a - Function.leftLim f a))
⊢ (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a

Tactic:
exact tendsto_nhds_unique L1 L2

Premises used: tendsto_nhds_unique
-- 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
⊢ Disjoint (Icc a a) (Ioc a b)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
rw :
  Function.rightLim f a - Function.leftLim f a + (Function.rightLim f b - Function.rightLim f a) =
    Function.rightLim f b - Function.leftLim f a
⊢ (↑hf.vectorMeasure : Set α → E) (Icc a b) = Function.rightLim f b - Function.leftLim f a

Tactic:
rw [← Icc_union_Ioc_eq_Icc le_rfl h, VectorMeasure.of_union (by simp)
    measurableSet_Icc measurableSet_Ioc, Icc_self, hf.vectorMeasure_singleton,
    hf.vectorMeasure_Ioc h]

Premises used: Set.Icc_self, le_rfl, MeasureTheory.VectorMeasure.of_union, Set.Icc_union_Ioc_eq_Icc, measurableSet_Icc, BoundedVariationOn.vectorMeasure_singleton, measurableSet_Ioc, BoundedVariationOn.vectorMeasure_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
⊢ Function.rightLim f a - Function.leftLim f a + (Function.rightLim f b - Function.rightLim f a) =
    Function.rightLim f b - Function.leftLim f a

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
h : a < b
⊢ (↑hf.vectorMeasure : Set α → E) (Ioc a b) = Function.rightLim f b - Function.rightLim f a

Tactic:
have := hf.vectorMeasure_Ioc h.le
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
h : a < b
this : (↑hf.vectorMeasure : Set α → E) (Ioo a b ∪ Icc b b) = Function.rightLim f b - Function.rightLim f a
⊢ Disjoint (Ioo a b) (Icc b b)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
h : a < b
this : (↑hf.vectorMeasure : Set α → E) (Ioc a b) = Function.rightLim f b - Function.rightLim f a
⊢ (↑hf.vectorMeasure : Set α → E) (Ioo a b) + (Function.rightLim f b - Function.leftLim f b) =
    Function.rightLim f b - Function.rightLim f a

Tactic:
rw [← Ioo_union_Icc_eq_Ioc h le_rfl, VectorMeasure.of_union (by simp) measurableSet_Ioo
    measurableSet_Icc, hf.vectorMeasure_Icc le_rfl] at this

Premises used: le_rfl, Set.Ioo_union_Icc_eq_Ioc, MeasureTheory.VectorMeasure.of_union, BoundedVariationOn.vectorMeasure_Icc, measurableSet_Ioo, measurableSet_Icc
-- 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
this :
  (↑hf.vectorMeasure : Set α → E) (Ioo a b) + (Function.rightLim f b - Function.leftLim f b) =
    Function.rightLim f b - Function.rightLim f a
⊢ (↑hf.vectorMeasure : Set α → E) (Ioo a b) = Function.leftLim f b - Function.rightLim f a

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
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
inl : ∀ (h : a ≤ a), (↑hf.vectorMeasure : Set α → E) (Ico a a) = Function.leftLim f a - Function.leftLim f a
inr : ∀ (h' : a < b), (↑hf.vectorMeasure : Set α → E) (Ico a b) = Function.leftLim f b - Function.leftLim f a
⊢ (↑hf.vectorMeasure : Set α → E) (Ico a b) = Function.leftLim f b - Function.leftLim f a

Tactic:
rcases h.eq_or_lt with rfl | h'

Premises used: LE.le.eq_or_lt, 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
a : α
hf : BoundedVariationOn f univ
h : a ≤ a
⊢ (↑hf.vectorMeasure : Set α → E) (Ico a a) = Function.leftLim f a - Function.leftLim f a

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
h' : a < b
⊢ Disjoint (Icc a a) (Ioo a b)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
h' : a < b
inr :
  Function.rightLim f a - Function.leftLim f a + (Function.leftLim f b - Function.rightLim f a) =
    Function.leftLim f b - Function.leftLim f a
⊢ (↑hf.vectorMeasure : Set α → E) (Ico a b) = Function.leftLim f b - Function.leftLim f a

Tactic:
rw [← Icc_union_Ioo_eq_Ico le_rfl h', VectorMeasure.of_union (by simp) measurableSet_Icc
    measurableSet_Ioo, hf.vectorMeasure_Icc le_rfl, hf.vectorMeasure_Ioo h']

Premises used: le_rfl, MeasureTheory.VectorMeasure.of_union, BoundedVariationOn.vectorMeasure_Icc, measurableSet_Ioo, measurableSet_Icc, BoundedVariationOn.vectorMeasure_Ioo, Set.Icc_union_Ioo_eq_Ico
-- 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
h' : a < b
⊢ Function.rightLim f a - Function.leftLim f a + (Function.leftLim f b - Function.rightLim f a) =
    Function.leftLim f b - Function.leftLim f a

Tactic:
abel
-- 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
a : α
⊢ Nonempty α

Tactic:
have : Nonempty α := ⟨a⟩
-- 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
a : α
this : Nonempty α
⊢ Tendsto f atTop (𝓝 (limUnder atTop f))

Tactic:
have hlim : Tendsto f atTop (𝓝 (limUnder atTop f)) := hf.tendsto_atTop_limUnder
-- 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
a : α
this : Nonempty α
hlim : Tendsto f atTop (𝓝 (limUnder atTop f))
⊢ ∃ (u : ℕ → α), Monotone u ∧ Tendsto u atTop atTop

Tactic:
Filter.exists_seq_monotone_tendsto_atTop_atTop α

Premises used: Filter.exists_seq_monotone_tendsto_atTop_atTop