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
a : α
this : Nonempty α
hlim : Tendsto f atTop (𝓝 (limUnder atTop f))
obtain :
  ∀ (u : ℕ → α) (u_mono : Monotone u) (hu : Tendsto u atTop atTop),
    (↑hf.vectorMeasure : Set α → E) (Ici a) = limUnder atTop f - Function.leftLim f a
⊢ (↑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 α

Premises used: Filter.exists_seq_monotone_tendsto_atTop_atTop
-- 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 : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
⊢ ⋃ (n : ℕ), Icc a (u n) ≤ Ici a

Tactic:
simp [Icc_subset_Ici_self]

Premises used: Set.Icc_subset_Ici_self
-- 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 : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
apply : Ici a ≤ ⋃ (n : ℕ), Icc a (u n)
⊢ Ici a = ⋃ (n : ℕ), Icc a (u n)

Tactic:
apply le_antisymm ?_ (by simp [Icc_subset_Ici_self])

Premises used: le_antisymm
-- 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 : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
x : α
a₁ : ∀ (hx : a ≤ x), Membership.mem (γ := Set α) (⋃ (n : ℕ), Icc a (u n)) x
⊢ x ∈ Ici a → Membership.mem (γ := Set α) (⋃ (n : ℕ), Icc a (u n)) x

Tactic:
(hx : a ≤ 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
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 : α
hx : a ≤ x
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), Icc a (u n)) x

Tactic:
simpa [hx] using (hu.eventually (Ici_mem_atTop x)).exists

Premises used: Filter.Eventually.exists, Filter.Ici_mem_atTop, Filter.Tendsto.eventually
-- 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 : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
⊢ 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
-- 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_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)
rw :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (⋃ (n : ℕ), Icc a (u n))))
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Ici a)))

Tactic:
rw [this]
-- 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_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)
i j : ℕ
hij : i ≤ j
x : α
hx : Membership.mem (γ := Set α) ((fun (n : ℕ) ↦ Icc a (u n)) i) x
⊢ Membership.mem (γ := Set α) ((fun (n : ℕ) ↦ Icc a (u n)) j) x

Tactic:
grind [Monotone]

Premises used: Monotone
-- 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_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) (⋃ (n : ℕ), Icc a (u n))))

Tactic:
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)

Premises used: measurableSet_Icc, MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iUnion_atTop_nat
-- 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 : ℕ → α
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)))

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)
-- 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 : ℕ → α
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)))
⊢ ∀ (b : α), ∃ (a : ℕ), ∀ b_1 ≥ a, b ≤ u b_1

Tactic:
simp only [tendsto_atTop, eventually_atTop] at hu

Premises used: Filter.tendsto_atTop, Filter.eventually_atTop
-- 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 : ℕ → α
u_mono : Monotone u
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Ici a)))
hu : ∀ (b : α), ∃ (a : ℕ), ∀ b_1 ≥ a, b ≤ u b_1
⊢ ∀ᶠ (n : ℕ) in atTop, a ≤ u n

Tactic:
simp [hu]
-- 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 : ℕ → α
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

Tactic:
have : ∀ᶠ n in atTop, a ≤ u n := by
        simp only [tendsto_atTop, eventually_atTop] at hu
        simp [hu]
-- 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_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
rw rw₁ : Function.rightLim f (u n) - Function.leftLim f a = Function.rightLim f (u n) - Function.leftLim f a
⊢ Function.rightLim f (u n) - Function.leftLim f a = (↑hf.vectorMeasure : Set α → E) (Icc a (u n))

Tactic:
rw [hf.vectorMeasure_Icc hn]

Premises used: BoundedVariationOn.vectorMeasure_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
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
h₁ h₂ :
  ∀ (n : ℕ) (hn : a ≤ u n),
    Function.rightLim f (u n) - Function.leftLim f a = (↑hf.vectorMeasure : Set α → E) (Icc 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))

Tactic:
filter_upwards [this] with n hn using by rw [hf.vectorMeasure_Icc hn]
-- 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 : ℕ → α
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))

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]
-- 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_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))
apply :
  Tendsto (fun (n : ℕ) ↦ Function.rightLim f (u n) - Function.leftLim f a) atTop
    (𝓝 (limUnder atTop f - Function.leftLim f a))
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
    (𝓝 (limUnder atTop f - Function.leftLim f a))

Tactic:
apply Tendsto.congr' this

Premises used: Filter.Tendsto.congr'
-- 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_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))
apply : Tendsto (fun (x : ℕ) ↦ Function.rightLim f (u x)) atTop (𝓝 (limUnder atTop f))
⊢ Tendsto (fun (n : ℕ) ↦ Function.rightLim f (u n) - Function.leftLim f a) atTop
    (𝓝 (limUnder atTop f - Function.leftLim f a))

Tactic:
apply Tendsto.sub ?_ tendsto_const_nhds

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
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 (x : ℕ) ↦ Function.rightLim f (u x)) atTop (𝓝 (limUnder atTop f))

Tactic:
(tendsto_rightLim_atTop_of_tendsto hlim).comp hu

Premises used: Function.rightLim, tendsto_rightLim_atTop_of_tendsto, Filter.Tendsto.comp, Function.leftLim, ite
-- 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_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 (x : ℕ) ↦ Function.rightLim f (u x)) atTop (𝓝 (limUnder atTop f))

Tactic:
exact (tendsto_rightLim_atTop_of_tendsto hlim).comp hu

Premises used: tendsto_rightLim_atTop_of_tendsto, 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
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))

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
-- 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 : ℕ → α
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)))
B :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
    (𝓝 (limUnder atTop f - Function.leftLim f a))
⊢ (↑hf.vectorMeasure : Set α → E) (Ici a) = limUnder atTop f - Function.leftLim f a

Tactic:
tendsto_nhds_unique A B

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
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)))
B :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc a (u n))) atTop
    (𝓝 (limUnder atTop f - Function.leftLim f a))
⊢ (↑hf.vectorMeasure : Set α → E) (Ici a) = limUnder atTop f - Function.leftLim f a

Tactic:
exact tendsto_nhds_unique A B

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
hf : BoundedVariationOn f univ
a : α
⊢ (↑hf.vectorMeasure : Set α → E) (Ici a) = limUnder atTop f - Function.leftLim f a

Tactic:
have := hf.vectorMeasure_Ici 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 : (↑hf.vectorMeasure : Set α → E) (Icc a a ∪ Ioi a) = limUnder atTop f - Function.leftLim f a
⊢ Disjoint (Icc a a) (Ioi 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
hf : BoundedVariationOn f univ
a : α
this : (↑hf.vectorMeasure : Set α → E) (Ici a) = limUnder atTop f - Function.leftLim f a
⊢ 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

Premises used: le_rfl, MeasureTheory.VectorMeasure.of_union, Set.Icc_union_Ioi_eq_Ici, measurableSet_Ioi, BoundedVariationOn.vectorMeasure_Icc, measurableSet_Icc