awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α
this : Nonempty α
⊢ (↑hf.vectorMeasure : Set α → E) (Ici a) = limUnder atTop f - Function.leftLim f a
have hlim : Tendsto f atTop (𝓝 (limUnder atTop f))
Tactic: have hlim : Tendsto f atTop (𝓝 (limUnder atTop f)) := hf.tendsto_atTop_limUnder
-- 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
a : α
this : Nonempty α
hlim : Tendsto f atTop (𝓝 (limUnder atTop f))
⊢ (↑hf.vectorMeasure : Set α → E) (Ici a) = limUnder atTop f - Function.leftLim f a
have obtain : ∀ (u : ℕ → α) (u_mono : Monotone u) (hu : Tendsto u atTop atTop),
  (↑hf.vectorMeasure : Set α → E) (Ici a) = limUnder atTop f - Function.leftLim f a
Tactic: obtain ⟨u, u_mono, hu⟩ : ∃ u, Monotone u ∧ Tendsto u atTop atTop :=
    Filter.exists_seq_monotone_tendsto_atTop_atTop α
-- 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
a : α
this : Nonempty α
hlim : Tendsto f atTop (𝓝 (limUnder atTop f))
u : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
⊢ Ici a = ⋃ (n : ℕ), Icc a (u n)
have apply : Ici a ≤ ⋃ (n : ℕ), Icc a (u n)
Tactic: apply le_antisymm ?_ (by simp [Icc_subset_Ici_self])
-- 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
a : α
this : Nonempty α
hlim : Tendsto f atTop (𝓝 (limUnder atTop f))
u : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
x : α
⊢ x ∈ Ici a → Membership.mem (γ := Set α) (⋃ (n : ℕ), Icc a (u n)) x
have a₁ : ∀ (hx : a ≤ x), Membership.mem (γ := Set α) (⋃ (n : ℕ), Icc a (u n)) x
Tactic: (hx : a ≤ x)
-- 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 : α
this : Nonempty α
hlim : Tendsto f atTop (𝓝 (limUnder atTop f))
u : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Ici a)))
have this₁ : Ici a = ⋃ (n : ℕ), Icc a (u n)
Tactic: have : Ici a = ⋃ n, Icc a (u n) := by
      apply le_antisymm ?_ (by simp [Icc_subset_Ici_self])
      intro x (hx : a ≤ x)
      simpa [hx] using (hu.eventually (Ici_mem_atTop x)).exists
-- 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
a : α
this_1 : Nonempty α
hlim : Tendsto f atTop (𝓝 (limUnder atTop f))
u : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
this : Ici a = ⋃ (n : ℕ), Icc a (u n)
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Ici a)))
have rw : Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
  (𝓝 ((↑hf.vectorMeasure : Set α → E) (⋃ (n : ℕ), Icc a (u n))))
Tactic: rw [this]
-- 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 : α
this : Nonempty α
hlim : Tendsto f atTop (𝓝 (limUnder atTop f))
u : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
⊢ (↑hf.vectorMeasure : Set α → E) (Ici a) = limUnder atTop f - Function.leftLim f a
have A : Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
  (𝓝 ((↑hf.vectorMeasure : Set α → E) (Ici a)))
Tactic: have A : Tendsto (fun n ↦ hf.vectorMeasure (Icc a (u n))) atTop
      (𝓝 (hf.vectorMeasure (Ici a))) := by
    have : Ici a = ⋃ n, Icc a (u n) := by
      apply le_antisymm ?_ (by simp [Icc_subset_Ici_self])
      intro x (hx : a ≤ x)
      simpa [hx] using (hu.eventually (Ici_mem_atTop x)).exists
    rw [this]
    exact hf.vectorMeasure.tendsto_vectorMeasure_iUnion_atTop_nat (s := fun n ↦ Icc a (u n))
      (fun i j hij x hx ↦ by grind [Monotone]) (fun i ↦ measurableSet_Icc)
-- 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 : α
this : Nonempty α
hlim : Tendsto f atTop (𝓝 (limUnder atTop f))
u : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Ici a)))
⊢ ∀ᶠ (n : ℕ) in atTop, a ≤ u n
have hu₁ : ∀ (b : α), ∃ (a : ℕ), ∀ b_1 ≥ a, b ≤ u b_1
Tactic: simp only [tendsto_atTop, eventually_atTop] at hu
Cleared hypotheses: hu
-- 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 : α
this : Nonempty α
hlim : Tendsto f atTop (𝓝 (limUnder atTop f))
u : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Ici a)))
⊢ EventuallyEq.{0, u_2} (β := E) atTop (fun (n : ℕ) ↦ Function.rightLim f (u n) - Function.leftLim f a) fun (n : ℕ) ↦
    (↑hf.vectorMeasure : Set α → E) (Icc a (u n))
have this₁ : ∀ᶠ (n : ℕ) in atTop, a ≤ u n
Tactic: have : ∀ᶠ n in atTop, a ≤ u n := by
        simp only [tendsto_atTop, eventually_atTop] at hu
        simp [hu]
-- 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
a : α
this_1 : Nonempty α
hlim : Tendsto f atTop (𝓝 (limUnder atTop f))
u : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Ici a)))
this : ∀ᶠ (n : ℕ) in atTop, a ≤ u n
n : ℕ
hn : a ≤ u n
⊢ Function.rightLim f (u n) - Function.leftLim f a = (↑hf.vectorMeasure : Set α → E) (Icc a (u n))
have rw : Function.rightLim f (u n) - Function.leftLim f a = Function.rightLim f (u n) - Function.leftLim f a
Tactic: rw [hf.vectorMeasure_Icc hn]
-- 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
a : α
this_1 : Nonempty α
hlim : Tendsto f atTop (𝓝 (limUnder atTop f))
u : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Ici a)))
this : ∀ᶠ (n : ℕ) in atTop, a ≤ u n
⊢ EventuallyEq.{0, u_2} (β := E) atTop (fun (n : ℕ) ↦ Function.rightLim f (u n) - Function.leftLim f a) fun (n : ℕ) ↦
    (↑hf.vectorMeasure : Set α → E) (Icc a (u n))
have h : ∀ (a_1 : ℕ),
  Membership.mem (γ := Set ℕ)
    {x : ℕ |
      Membership.mem (γ := Set ℕ) {x : ℕ | (fun (n : ℕ) ↦ a ≤ u n) x} x →
        Membership.mem (γ := Set ℕ)
          {x : ℕ |
            (fun (x : ℕ) ↦
                Eq.{u_2 + 1} (α := E) ((fun (n : ℕ) ↦ Function.rightLim f (u n) - Function.leftLim f a) x)
                  ((fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) x))
              x}
          x}
    a_1
Tactic: filter_upwards [this] with n hn using by rw [hf.vectorMeasure_Icc hn]
-- 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
a : α
this_1 : Nonempty α
hlim : Tendsto f atTop (𝓝 (limUnder atTop f))
u : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Ici a)))
this : ∀ᶠ (n : ℕ) in atTop, a ≤ u n
h :
  ∀ (a_1 : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (n : ℕ) ↦ a ≤ u n) x} x →
          Membership.mem (γ := Set ℕ)
            {x : ℕ |
              (fun (x : ℕ) ↦
                  Eq.{u_2 + 1} (α := E) ((fun (n : ℕ) ↦ Function.rightLim f (u n) - Function.leftLim f a) x)
                    ((fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) x))
                x}
            x}
      a_1
⊢ EventuallyEq.{0, u_2} (β := E) atTop (fun (n : ℕ) ↦ Function.rightLim f (u n) - Function.leftLim f a) fun (n : ℕ) ↦
    (↑hf.vectorMeasure : Set α → E) (Icc a (u n))
have h₁ : ∀ (a_1 : ℕ),
  a ≤ u a_1 → Function.rightLim f (u a_1) - Function.leftLim f a = (↑hf.vectorMeasure : Set α → E) (Icc a (u a_1))
Tactic: filter_upwards [this] with n hn using by rw [hf.vectorMeasure_Icc hn]
-- 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 : α
this : Nonempty α
hlim : Tendsto f atTop (𝓝 (limUnder atTop f))
u : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Ici a)))
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
    (𝓝 (limUnder atTop f - Function.leftLim f a))
have this₁ : EventuallyEq.{0, u_2} (β := E) atTop (fun (n : ℕ) ↦ Function.rightLim f (u n) - Function.leftLim f a) fun (n : ℕ) ↦
  (↑hf.vectorMeasure : Set α → E) (Icc a (u n))
Tactic: have : (fun n ↦ f.rightLim (u n) - f.leftLim a) =ᶠ[atTop]
        (fun n ↦ hf.vectorMeasure (Icc a (u n))) := by
      have : ∀ᶠ n in atTop, a ≤ u n := by
        simp only [tendsto_atTop, eventually_atTop] at hu
        simp [hu]
      filter_upwards [this] with n hn using by rw [hf.vectorMeasure_Icc hn]
-- 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
a : α
this_1 : Nonempty α
hlim : Tendsto f atTop (𝓝 (limUnder atTop f))
u : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Ici a)))
this :
  EventuallyEq.{0, u_2} (β := E) atTop (fun (n : ℕ) ↦ Function.rightLim f (u n) - Function.leftLim f a) fun (n : ℕ) ↦
    (↑hf.vectorMeasure : Set α → E) (Icc a (u n))
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
    (𝓝 (limUnder atTop f - Function.leftLim f a))
have apply : Tendsto (fun (n : ℕ) ↦ Function.rightLim f (u n) - Function.leftLim f a) atTop
  (𝓝 (limUnder atTop f - Function.leftLim f a))
Tactic: apply Tendsto.congr' 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
hf : BoundedVariationOn f univ
a : α
this_1 : Nonempty α
hlim : Tendsto f atTop (𝓝 (limUnder atTop f))
u : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Ici a)))
this :
  EventuallyEq.{0, u_2} (β := E) atTop (fun (n : ℕ) ↦ Function.rightLim f (u n) - Function.leftLim f a) fun (n : ℕ) ↦
    (↑hf.vectorMeasure : Set α → E) (Icc a (u n))
⊢ Tendsto (fun (n : ℕ) ↦ Function.rightLim f (u n) - Function.leftLim f a) atTop
    (𝓝 (limUnder atTop f - Function.leftLim f a))
have apply : Tendsto (fun (x : ℕ) ↦ Function.rightLim f (u x)) atTop (𝓝 (limUnder atTop f))
Tactic: apply Tendsto.sub ?_ tendsto_const_nhds
-- 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 : α
this : Nonempty α
hlim : Tendsto f atTop (𝓝 (limUnder atTop f))
u : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Ici a)))
⊢ (↑hf.vectorMeasure : Set α → E) (Ici a) = limUnder atTop f - Function.leftLim f a
have B : Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
  (𝓝 (limUnder atTop f - Function.leftLim f a))
Tactic: have B : Tendsto (fun n ↦ hf.vectorMeasure (Icc a (u n))) atTop
      (𝓝 (limUnder atTop f - f.leftLim a)) := by
    have : (fun n ↦ f.rightLim (u n) - f.leftLim a) =ᶠ[atTop]
        (fun n ↦ hf.vectorMeasure (Icc a (u n))) := by
      have : ∀ᶠ n in atTop, a ≤ u n := by
        simp only [tendsto_atTop, eventually_atTop] at hu
        simp [hu]
      filter_upwards [this] with n hn using by rw [hf.vectorMeasure_Icc hn]
    apply Tendsto.congr' this
    apply Tendsto.sub ?_ tendsto_const_nhds
    exact (tendsto_rightLim_atTop_of_tendsto hlim).comp hu
-- 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) (Ioi a) = limUnder atTop f - Function.rightLim f a
have this : (↑hf.vectorMeasure : Set α → E) (Ici a) = limUnder atTop f - Function.leftLim f a
Tactic: have := hf.vectorMeasure_Ici 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
hf : BoundedVariationOn f univ
a : α
this : (↑hf.vectorMeasure : Set α → E) (Ici a) = limUnder atTop f - Function.leftLim f a
⊢ (↑hf.vectorMeasure : Set α → E) (Ioi a) = limUnder atTop f - Function.rightLim f a
have this₁ : Function.rightLim f a - Function.leftLim f a + (↑hf.vectorMeasure : Set α → E) (Ioi a) =
  limUnder atTop f - Function.leftLim f a
Tactic: rw [← Icc_union_Ioi_eq_Ici le_rfl, VectorMeasure.of_union (by simp) measurableSet_Icc
    measurableSet_Ioi, hf.vectorMeasure_Icc le_rfl] at this
Cleared hypotheses: this
-- 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) (Iic a) = Function.rightLim f a - limUnder atBot f
have this : Nonempty α
Tactic: have : Nonempty α := ⟨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
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
⊢ (↑hf.vectorMeasure : Set α → E) (Iic a) = Function.rightLim f a - limUnder atBot f
have hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
Tactic: have hlim : Tendsto f atBot (𝓝 (limUnder atBot f)) := hf.tendsto_atBot_limUnder
-- 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
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
⊢ (↑hf.vectorMeasure : Set α → E) (Iic a) = Function.rightLim f a - limUnder atBot f
have obtain : ∀ (u : ℕ → α) (u_anti : Antitone u) (hu : Tendsto u atTop atBot),
  (↑hf.vectorMeasure : Set α → E) (Iic a) = Function.rightLim f a - limUnder atBot f
Tactic: obtain ⟨u, u_anti, hu⟩ : ∃ u, Antitone u ∧ Tendsto u atTop atBot :=
    Filter.exists_seq_antitone_tendsto_atTop_atBot α
-- 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
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
⊢ Iic a = ⋃ (n : ℕ), Icc (u n) a
have apply : Iic a ≤ ⋃ (n : ℕ), Icc (u n) a
Tactic: apply le_antisymm ?_ (by simp [Icc_subset_Iic_self])
-- 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
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
x : α
⊢ x ∈ Iic a → Membership.mem (γ := Set α) (⋃ (n : ℕ), Icc (u n) a) x
have x₁ : ∀ (hx : x ≤ a), Membership.mem (γ := Set α) (⋃ (n : ℕ), Icc (u n) a) x
Tactic: (hx : x ≤ 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
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
have this₁ : Iic a = ⋃ (n : ℕ), Icc (u n) a
Tactic: have : Iic a = ⋃ n, Icc (u n) a := by
      apply le_antisymm ?_ (by simp [Icc_subset_Iic_self])
      intro x (hx : x ≤ a)
      simpa [hx] using (hu.eventually (Iic_mem_atBot x)).exists
-- 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
a : α
this_1 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
this : Iic a = ⋃ (n : ℕ), Icc (u n) a
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
have rw : Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
  (𝓝 ((↑hf.vectorMeasure : Set α → E) (⋃ (n : ℕ), Icc (u n) a)))
Tactic: rw [this]