awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
a : α
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
⊢ (↑(VectorMeasure.dirac (⋯.choose (p := fun (x : α) ↦ IsBot x))
            (Function.rightLim f (⋯.choose (p := fun (x : α) ↦ IsBot x)) - f (⋯.choose (p := fun (x : α) ↦ IsBot x)))) :
        Set α → E)
      {a} =
    Function.rightLim f a - Function.leftLim f a
have pos : Function.rightLim f (sorry.choose (p := fun (x : α) ↦ IsBot x)) - f (sorry.choose (p := fun (x : α) ↦ IsBot x)) =
  Function.rightLim f a - Function.leftLim f a
Tactic: rw [VectorMeasure.dirac_apply_of_mem (MeasurableSet.singleton 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
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
pos :
  Function.rightLim f (⋯.choose (p := fun (x : α) ↦ IsBot x)) - f (⋯.choose (p := fun (x : α) ↦ IsBot x)) =
    Function.rightLim f a - Function.leftLim f a
⊢ (↑(VectorMeasure.dirac (⋯.choose (p := fun (x : α) ↦ IsBot x))
            (Function.rightLim f (⋯.choose (p := fun (x : α) ↦ IsBot x)) - f (⋯.choose (p := fun (x : α) ↦ IsBot x)))) :
        Set α → E)
      {a} =
    Function.rightLim f a - Function.leftLim f a
have pos₁ : Membership.mem (γ := Set α) {a} (sorry.choose (p := fun (x : α) ↦ IsBot x))
Tactic: rw [VectorMeasure.dirac_apply_of_mem (MeasurableSet.singleton 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
ha : ¬IsBot a
⊢ (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
have neg : ∀ (b : α) (hb : b < a), (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
Tactic: obtain ⟨b, hb⟩ : ∃ b, b < a := by simpa only [IsBot, not_forall, not_le] using 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
b : α
hb : b < a
⊢ (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
have neg : ∀ (u : ℕ → α) (u_mono : StrictMono u) (u_lt_a : ∀ (n : ℕ), u n ∈ Ioo b a) (u_lim : Tendsto u atTop (𝓝 a)),
  (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
Tactic: obtain ⟨u, u_mono, u_lt_a, u_lim⟩ :
      ∃ u : ℕ → α, StrictMono u ∧ (∀ n : ℕ, u n ∈ Ioo b a) ∧ Tendsto u atTop (𝓝 a) :=
    exists_seq_strictMono_tendsto' hb
-- 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
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n ∈ Ioo b a
u_lim : Tendsto u atTop (𝓝 a)
⊢ (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
have u_lt_a₁ : ∀ (n : ℕ), u n < a
Tactic: replace u_lt_a n : u n < a := (u_lt_a n).2
Cleared hypotheses: u_lt_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
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
⊢ Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
have refine : ∀ (x : α) (hx : Membership.mem (γ := Set α) (⋂ (n : ℕ), Ioc (u n) a) x), Membership.mem (γ := Set α) {a} x
Tactic: refine Subset.antisymm (fun x hx => by simp [mem_singleton_iff.1 hx, u_lt_a]) fun x hx => ?_
-- 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
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
x : α
hx : Membership.mem (γ := Set α) (⋂ (n : ℕ), Ioc (u n) a) x
⊢ Membership.mem (γ := Set α) {a} x
have hx₁ : ∀ (i : ℕ), u i < x ∧ x ≤ a
Tactic: replace hx : ∀ (i : ℕ), u i < x ∧ x ≤ a := by simpa using hx
Cleared hypotheses: hx
-- 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
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
x : α
hx : ∀ (i : ℕ), u i < x ∧ x ≤ a
⊢ Membership.mem (γ := Set α) {a} x
have this : a ≤ x
Tactic: have : a ≤ x := le_of_tendsto' u_lim fun n => (hx n).1.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 : α
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
⊢ (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
have A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
Tactic: have A : {a} = ⋂ n, Ioc (u n) a := by
    refine Subset.antisymm (fun x hx => by simp [mem_singleton_iff.1 hx, u_lt_a]) fun x hx => ?_
    replace hx : ∀ (i : ℕ), u i < x ∧ x ≤ a := by simpa using hx
    have : a ≤ x := le_of_tendsto' u_lim fun n => (hx n).1.le
    simp [le_antisymm this (hx 0).2]
-- 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
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)
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop (𝓝 ((↑hf.vectorMeasure : Set α → E) {a}))
have rw : Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop
  (𝓝 ((↑hf.vectorMeasure : Set α → E) (⋂ (n : ℕ), Ioc (u n) a)))
Tactic: rw [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
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)
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (⋂ (n : ℕ), Ioc (u n) a)))
have apply : Antitone.{0, u_1} (β := Set α) fun (n : ℕ) ↦ Ioc (u n) a
Tactic: apply VectorMeasure.tendsto_vectorMeasure_iInter_atTop_nat ?_ (fun n ↦ measurableSet_Ioc)
-- 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
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)
⊢ (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
have L1 : Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop (𝓝 ((↑hf.vectorMeasure : Set α → E) {a}))
Tactic: have L1 : Tendsto (fun n ↦ hf.vectorMeasure (Ioc (u n) a)) atTop (𝓝 (hf.vectorMeasure {a})) := by
    rw [A]
    apply VectorMeasure.tendsto_vectorMeasure_iInter_atTop_nat ?_ (fun n ↦ measurableSet_Ioc)
    exact fun m n hmn ↦ Ioc_subset_Ioc_left (u_mono.monotone hmn)
-- 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
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))
have simp_rw : Tendsto (fun (n : ℕ) ↦ Function.rightLim f a - Function.rightLim f (u n)) atTop
  (𝓝 (Function.rightLim f a - Function.leftLim f a))
Tactic: simp_rw [hf.vectorMeasure_Ioc (u_lt_a _).le]
-- 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
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 : ℕ) ↦ Function.rightLim f a - Function.rightLim f (u n)) atTop
    (𝓝 (Function.rightLim f a - Function.leftLim f a))
have apply : Tendsto (fun (x : ℕ) ↦ Function.rightLim f (u x)) atTop (𝓝 (Function.leftLim f a))
Tactic: apply tendsto_const_nhds.sub
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
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 (x : ℕ) ↦ Function.rightLim f (u x)) atTop (𝓝 (Function.leftLim f a))
have this : 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)
-- 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
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 (fun (x : ℕ) ↦ Function.rightLim f (u x)) atTop (𝓝 (Function.leftLim f a))
have h : Function.leftLim f a = Function.leftLim (Function.rightLim f) a
Tactic: convert! (hf.rightLim.tendsto_leftLim a).comp this using 2
-- 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
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
have rw : a ∈ Iic a
Tactic: rw [← mem_closure_iff_nhdsWithin_neBot, closure_Iio' ⟨b, hb⟩]
-- 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
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)
⊢ Function.leftLim f a = Function.leftLim (Function.rightLim f) a
have this₁ : (𝓝[<] a).NeBot
Tactic: have : (𝓝[<] a).NeBot := by
      rw [← mem_closure_iff_nhdsWithin_neBot, closure_Iio' ⟨b, hb⟩]
      exact self_mem_Iic
-- 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
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}))
⊢ (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
have L2 : 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
-- 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) (Icc a b) = Function.rightLim f b - Function.leftLim f a
have 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
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]
-- 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) (Ioo a b) = Function.leftLim f b - Function.rightLim f a
have this : (↑hf.vectorMeasure : Set α → E) (Ioc a b) = Function.rightLim f b - Function.rightLim f a
Tactic: have := hf.vectorMeasure_Ioc h.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
this : (↑hf.vectorMeasure : Set α → E) (Ioc a b) = Function.rightLim f b - Function.rightLim f a
⊢ (↑hf.vectorMeasure : Set α → E) (Ioo a b) = Function.leftLim f b - Function.rightLim f a
have this₁ : (↑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
Cleared hypotheses: this
-- 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) (Ico a b) = Function.leftLim f b - Function.leftLim f a
have inl : ∀ (h : a ≤ a), (↑hf.vectorMeasure : Set α → E) (Ico a a) = Function.leftLim f a - Function.leftLim f a
Tactic: rcases h.eq_or_lt with rfl | h'
Cleared hypotheses: 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
inl : ∀ (h : a ≤ a), (↑hf.vectorMeasure : Set α → E) (Ico a a) = Function.leftLim f a - Function.leftLim f a
⊢ (↑hf.vectorMeasure : Set α → E) (Ico a b) = Function.leftLim f b - Function.leftLim f a
have inr : ∀ (h' : a < b), (↑hf.vectorMeasure : Set α → E) (Ico a b) = Function.leftLim f b - Function.leftLim f a
Tactic: rcases h.eq_or_lt with rfl | 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
h' : a < b
⊢ (↑hf.vectorMeasure : Set α → E) (Ico a b) = Function.leftLim f b - Function.leftLim f a
have 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
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']
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
⊢ (↑hf.vectorMeasure : Set α → E) (Ici a) = limUnder atTop f - Function.leftLim f a
have this : Nonempty α
Tactic: have : Nonempty α := ⟨a⟩